Skip to content

Commit 9ac500b

Browse files
pitmonticonepitmonticone
authored
chore(ToMathlib): note upstreaming status for 8 files (#548)
Update the upstreaming status comments for files that have been PRed to mathlib: - `Analysis/MeanInequalitiesPow` leanprover-community/mathlib4#37547 - `Order/LiminfLimsup` leanprover-community/mathlib4#37549 (merged) - `Topology/Order/Basic` leanprover-community/mathlib4#37550 (moved to DenselyOrdered) - `MeasureTheory/Integral/Average` leanprover-community/mathlib4#37551 - `MeasureTheory/Measure/ENNReal` leanprover-community/mathlib4#37552 (generalized to `measurable_iSup_of_lowerSemicontinuous`) - `MeasureTheory/Integral/Lebesgue` leanprover-community/mathlib4#37558 (merged) - `MeasureTheory/Function/LpSpace/Indicator` leanprover-community/mathlib4#37559 - `MeasureTheory/Function/LpSpace/ContinuousFunctions` leanprover-community/mathlib4#37560 - `Data/ENNReal` leanprover-community/mathlib4#37565 (partial) - `MeasureTheory/Integral/Bochner/ContinuousLinearMap` leanprover-community/mathlib4#37568 (partial) - `Topology/Instances/AddCircle/Defs` leanprover-community/mathlib4#37570 (partial) - `Discrete/SumEstimates` leanprover-community/mathlib4#37597 Also notes that `IntegrableAtFilter.congr` and `integrableOn_of_integrableOn_inter_support` already exist in mathlib.
1 parent 743d325 commit 9ac500b

File tree

13 files changed

+26
-10
lines changed

13 files changed

+26
-10
lines changed

‎Carleson/Discrete/SumEstimates.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
11
import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
2+
3+
-- Upstreaming status: upstreamed in
4+
-- https://github.com/leanprover-community/mathlib4/pull/37597
25
import Mathlib.Analysis.SumIntegralComparisons
36

47
open scoped Nat

‎Carleson/ToMathlib/Analysis/MeanInequalitiesPow.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import Mathlib.Analysis.MeanInequalitiesPow
22
import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
33

4-
-- Upstreaming status: looks useful and ready to go
4+
-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37547
55

66
namespace ENNReal
77

‎Carleson/ToMathlib/Data/ENNReal.lean‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,10 @@ import Mathlib.Analysis.Normed.Group.Uniform
33
import Mathlib.Analysis.Normed.Ring.Basic
44
import Mathlib.Order.CompletePartialOrder
55

6-
-- Upstreaming status: lemmas seem useful; proofs may need some polish
6+
-- Upstreaming status: lemmas seem useful; proofs may need some polish.
77
-- At least three or four distinct PRs.
8+
-- `ofReal_inv_le` and `ofReal_div_le` upstreamed in
9+
-- https://github.com/leanprover-community/mathlib4/pull/37565
810

911
/-! ## `ENNReal` manipulation lemmas -/
1012

‎Carleson/ToMathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ import Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
22

33
open MeasureTheory
44

5-
-- Upstreaming status: rename to `memLp`, then ready for upstreaming.
5+
-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37560
66

77
lemma ContinuousMap.memLp {α E : Type*} {m0 : MeasurableSpace α} {p : ENNReal} (μ : Measure α)
88
[NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E]

‎Carleson/ToMathlib/MeasureTheory/Function/LpSpace/Indicator.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,7 @@ variable {X : Type*} [TopologicalSpace X] [MeasurableSpace X]
1111

1212
namespace MeasureTheory
1313

14-
-- Upstreaming status: seems ready for PRing
15-
-- not actually used in the project, but we want to upstream this and similar lemmas.
14+
-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37559
1615

1716
/-- A bounded measurable function with compact support is in L^p. -/
1817
theorem _root_.HasCompactSupport.memLp_of_enorm_bound {f : X → E} (hf : HasCompactSupport f)

‎Carleson/ToMathlib/MeasureTheory/Integral/Average.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
import Mathlib.MeasureTheory.Integral.Average
22

3-
-- Upstreaming status: useful and good to go
3+
-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37551
44

55
open MeasureTheory MeasureTheory.Measure Filter Set
66

‎Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
33
open MeasureTheory
44

55
-- Upstreaming status: looks ready for upstreaming; pay attention to the correct file to move to!
6+
-- `exists_ne_zero_of_setIntegral_ne_zero` and `exists_ne_zero_of_integral_ne_zero` upstreamed in
7+
-- https://github.com/leanprover-community/mathlib4/pull/37568
68

79
-- Put after `setIntegral_re_add_im`
810

‎Carleson/ToMathlib/MeasureTheory/Integral/IntegrableOn.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@ open Set Filter TopologicalSpace MeasureTheory Function
55
open scoped Topology Interval Filter ENNReal MeasureTheory
66

77
-- Upstreaming note: Hypotheses and variables have been matched to corresponding Mathlib file
8+
-- `IntegrableAtFilter.congr` already in mathlib.
9+
-- `integrableOn_of_integrableOn_inter_support` already in mathlib as
10+
-- `MeasureTheory.IntegrableOn.of_inter_support`.
811

912
variable {α β ε ε' E F : Type*} [MeasurableSpace α]
1013

‎Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
22

3-
-- Upstreaming status: useful and good to go. Easy generalisations of mathlib lemmas.
3+
-- Upstreaming status: `lintegral_eq_iSup_eapprox_lintegral'` and `lintegral_comp'`
4+
-- upstreamed in https://github.com/leanprover-community/mathlib4/pull/37558
5+
-- Remaining lemmas: shift/scaling aliases, `lintegral_set_mono_fn`
6+
-- (already `setLIntegral_mono'` in mathlib).
47

58
open NNReal ENNReal MeasureTheory Set
69

‎Carleson/ToMathlib/MeasureTheory/Measure/ENNReal.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
22

3-
-- Upstreaming status: ready to be upstreamed
3+
-- Upstreaming status: upstreamed as `measurable_iSup_of_lowerSemicontinuous` (generalized) in
4+
-- https://github.com/leanprover-community/mathlib4/pull/37552
45

56
open Set TopologicalSpace ENNReal
67

0 commit comments

Comments
 (0)
⚡