chore(ToMathlib): note upstreaming status for 8 files

Carleson/ToMathlib/Analysis/MeanInequalitiesPow.lean

@@ -1,7 +1,7 @@
 import Mathlib.Analysis.MeanInequalitiesPow
 import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
 
--- Upstreaming status: looks useful and ready to go
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37547
 
 namespace ENNReal
 

Carleson/ToMathlib/Data/ENNReal.lean

@@ -3,8 +3,10 @@ import Mathlib.Analysis.Normed.Group.Uniform
 import Mathlib.Analysis.Normed.Ring.Basic
 import Mathlib.Order.CompletePartialOrder
 
--- Upstreaming status: lemmas seem useful; proofs may need some polish
+-- Upstreaming status: lemmas seem useful; proofs may need some polish.
 -- At least three or four distinct PRs.
+-- `ofReal_inv_le` and `ofReal_div_le` upstreamed in
+-- https://github.com/leanprover-community/mathlib4/pull/37565
 
 /-! ## `ENNReal` manipulation lemmas -/
 

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

@@ -2,7 +2,7 @@ import Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
 
 open MeasureTheory
 
--- Upstreaming status: rename to `memLp`, then ready for upstreaming.
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37560
 
 lemma ContinuousMap.memLp {α E : Type*} {m0 : MeasurableSpace α} {p : ENNReal} (μ : Measure α)
     [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E]

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

@@ -11,8 +11,7 @@ variable {X : Type*} [TopologicalSpace X] [MeasurableSpace X]
 
 namespace MeasureTheory
 
--- Upstreaming status: seems ready for PRing
--- not actually used in the project, but we want to upstream this and similar lemmas.
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37559
 
 /-- A bounded measurable function with compact support is in L^p. -/
 theorem _root_.HasCompactSupport.memLp_of_enorm_bound {f : X → E} (hf : HasCompactSupport f)

Carleson/ToMathlib/MeasureTheory/Integral/Average.lean

@@ -1,6 +1,6 @@
 import Mathlib.MeasureTheory.Integral.Average
 
--- Upstreaming status: useful and good to go
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37551
 
 open MeasureTheory MeasureTheory.Measure Filter Set
 

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

@@ -3,6 +3,8 @@ import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
 open MeasureTheory
 
 -- Upstreaming status: looks ready for upstreaming; pay attention to the correct file to move to!
+-- `exists_ne_zero_of_setIntegral_ne_zero` and `exists_ne_zero_of_integral_ne_zero` upstreamed in
+-- https://github.com/leanprover-community/mathlib4/pull/37568
 
 -- Put after `setIntegral_re_add_im`
 

Carleson/ToMathlib/MeasureTheory/Integral/IntegrableOn.lean

@@ -5,6 +5,9 @@ open Set Filter TopologicalSpace MeasureTheory Function
 open scoped Topology Interval Filter ENNReal MeasureTheory
 
 -- Upstreaming note: Hypotheses and variables have been matched to corresponding Mathlib file
+-- `IntegrableAtFilter.congr` already in mathlib.
+-- `integrableOn_of_integrableOn_inter_support` already in mathlib as
+-- `MeasureTheory.IntegrableOn.of_inter_support`.
 
 variable {α β ε ε' E F : Type*} [MeasurableSpace α]
 

Carleson/ToMathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -1,6 +1,9 @@
 import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 
--- Upstreaming status: useful and good to go. Easy generalisations of mathlib lemmas.
+-- Upstreaming status: `lintegral_eq_iSup_eapprox_lintegral'` and `lintegral_comp'`
+-- upstreamed in https://github.com/leanprover-community/mathlib4/pull/37558
+-- Remaining lemmas: shift/scaling aliases, `lintegral_set_mono_fn`
+-- (already `setLIntegral_mono'` in mathlib).
 
 open NNReal ENNReal MeasureTheory Set
 

Carleson/ToMathlib/MeasureTheory/Measure/ENNReal.lean

@@ -1,6 +1,7 @@
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
 
--- Upstreaming status: ready to be upstreamed
+-- Upstreaming status: upstreamed as `measurable_iSup_of_lowerSemicontinuous` (generalized) in
+-- https://github.com/leanprover-community/mathlib4/pull/37552
 
 open Set TopologicalSpace ENNReal
 

Carleson/ToMathlib/Order/LiminfLimsup.lean

@@ -1,6 +1,6 @@
 import Mathlib.Order.LiminfLimsup
 
--- Upstreaming status: seems like a useful lemma; no obvious clean-up opportunities
+-- Upstreaming status: upstreamed in https://github.com/leanprover-community/mathlib4/pull/37549
 
 theorem Filter.iSup_liminf_le_liminf_iSup {α β : Type*} {ι : Sort*} [CompleteLattice α]
     {f : Filter β} {u : ι → β → α} :

Carleson/ToMathlib/Topology/Instances/AddCircle/Defs.lean

@@ -2,6 +2,8 @@ import Mathlib.Topology.Instances.AddCircle.Defs
 
 -- Upstreaming status: seems ready to go; lemmas are usually analogues of existing mathlib lemmas
 -- Sometimes, mathlib lemmas need to be renamed along with upstreaming this.
+-- Non-Periodic lemmas upstreamed in
+-- https://github.com/leanprover-community/mathlib4/pull/37570
 
 noncomputable section
 

Carleson/ToMathlib/Topology/Order/Basic.lean

@@ -1,6 +1,7 @@
 import Mathlib.Topology.Order.Basic
 
--- Upstreaming status: perhaps, the hypotheses can be weakened, but otherwise looks ready
+-- Upstreaming status: upstreamed (moved to Mathlib.Topology.Order.DenselyOrdered) in
+-- https://github.com/leanprover-community/mathlib4/pull/37550
 
 theorem nonempty_nhds_inter_Ioi {α : Type*} [LinearOrder α] [DenselyOrdered α]
     [TopologicalSpace α] [OrderTopology α]