chore: note the upstreaming status of more files and some minor golfs

Author: grunweg

Carleson/Classical/Basic.lean

@@ -63,20 +63,21 @@ lemma partialFourierSupLp_eq_partialFourierSupLp_of_aeeq {T : ℝ} [hT : Fact (0
 
 
 lemma partialFourierSum'_eq_partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) :
-    partialFourierSumLp p N f = MemLp.toLp (partialFourierSum' N f) ((partialFourierSum' N f).MemLp haarAddCircle ℂ)  := by
+    partialFourierSumLp p N f = MemLp.toLp (partialFourierSum' N f) ((partialFourierSum' N f).memLp haarAddCircle ℂ)  := by
   unfold partialFourierSumLp partialFourierSum'
   unfold fourierLp
   simp_rw [ContinuousMap.coe_sum, ContinuousMap.coe_smul]
-  rw [MemLp.toLp_sum _ (by intro n hn; apply MemLp.const_smul (ContinuousMap.MemLp haarAddCircle ℂ (fourier n)))]
-  rw [Finset.univ_eq_attach]
-  rw [← Finset.sum_attach]
+  rw [MemLp.toLp_sum _ (by
+      intro n hn; apply MemLp.const_smul (ContinuousMap.memLp haarAddCircle ℂ (fourier n))),
+    Finset.univ_eq_attach, ← Finset.sum_attach]
   rfl
 
 
 lemma partialFourierSum_aeeq_partialFourierSumLp [hT : Fact (0 < 2 * Real.pi)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : ℝ → ℂ) (h_mem_Lp : MemLp (liftIoc (2 * Real.pi) 0 f) 2 haarAddCircle) :
     liftIoc (2 * Real.pi) 0 (partialFourierSum N f) =ᶠ[ae haarAddCircle] ↑↑(partialFourierSumLp p N (MemLp.toLp (liftIoc (2 * Real.pi) 0 f) h_mem_Lp)) := by
-  rw [partialFourierSupLp_eq_partialFourierSupLp_of_aeeq (Lp.aestronglyMeasurable _) h_mem_Lp.aestronglyMeasurable (MemLp.coeFn_toLp h_mem_Lp)]
-  rw [partialFourierSum'_eq_partialFourierSumLp, partialFourierSum_eq_partialFourierSum']
+  rw [partialFourierSupLp_eq_partialFourierSupLp_of_aeeq (Lp.aestronglyMeasurable _)
+      h_mem_Lp.aestronglyMeasurable (MemLp.coeFn_toLp h_mem_Lp),
+    partialFourierSum'_eq_partialFourierSumLp, partialFourierSum_eq_partialFourierSum']
   symm
   apply MemLp.coeFn_toLp
 
@@ -86,15 +87,15 @@ local notation "S_" => partialFourierSum
 
 @[simp]
 lemma fourierCoeffOn_mul {a b : ℝ} {hab : a < b} {f : ℝ → ℂ} {c : ℂ} {n : ℤ} :
-  fourierCoeffOn hab (fun x ↦ c * f x) n = c * (fourierCoeffOn hab f n):= by
+    fourierCoeffOn hab (fun x ↦ c * f x) n = c * (fourierCoeffOn hab f n):= by
   simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
     fourier_coe_apply', mul_comm, Complex.ofReal_sub, smul_eq_mul, mul_assoc,
     intervalIntegral.integral_const_mul, Complex.real_smul, Complex.ofReal_inv]
   ring
 
 @[simp]
 lemma fourierCoeffOn_neg {a b : ℝ} {hab : a < b} {f : ℝ → ℂ} {n : ℤ} :
-  fourierCoeffOn hab (-f) n = - (fourierCoeffOn hab f n):= by
+    fourierCoeffOn hab (-f) n = - (fourierCoeffOn hab f n):= by
   simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
     fourier_coe_apply', Complex.ofReal_sub, Pi.neg_apply, smul_eq_mul, mul_neg,
     intervalIntegral.integral_neg, smul_neg, Complex.real_smul, Complex.ofReal_inv]
@@ -109,10 +110,8 @@ lemma fourierCoeffOn_add {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
     Complex.ofReal_inv]
   rw [← mul_add, ← intervalIntegral.integral_add]
   · ring_nf
-    apply hf.continuousOn_mul (Continuous.continuousOn _)
-    exact Complex.continuous_conj.comp' (by fun_prop)
-  · apply hg.continuousOn_mul (Continuous.continuousOn _)
-    exact Complex.continuous_conj.comp' (by fun_prop)
+    exact hf.continuousOn_mul (Continuous.continuousOn (by fun_prop))
+  · exact hg.continuousOn_mul (Continuous.continuousOn (by fun_prop))
 
 @[simp]
 lemma fourierCoeffOn_sub {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}

Carleson/ToMathlib/Data/Finset/Lattice/Fold.lean

@@ -3,6 +3,9 @@ import Mathlib.Order.ConditionallyCompleteLattice.Defs
 import Mathlib.Order.ConditionallyCompleteLattice.Indexed
 import Mathlib.Data.Set.Finite.Lattice
 
+-- Upstreaming status: under active development by @ldiedering
+-- Wait for the file to stabilise first.
+
 -- currently unused
 -- proof could probably be simplified if there were more mathlib lemmas about `ciSup` (in `ConditionallyCompleteLinearOrderBot`)
 theorem Finset.sup_eq_iSup' {α : Type*} {β : Type*} [ConditionallyCompleteLinearOrderBot β] (s : Finset α) (f : α → β) :
@@ -29,22 +32,19 @@ theorem Finset.sup_eq_iSup' {α : Type*} {β : Type*} [ConditionallyCompleteLine
       apply BddAbove.insert
       exact Finset.bddAbove (image f s)
     refine le_ciSup_of_le ?_ ha (le_refl (f a))
-    by_cases ha : Nonempty (a ∈ s)
+    by_cases! ha : Nonempty (a ∈ s)
     · rw [Set.range_const]
       exact bddAbove_singleton
-    · rw [not_nonempty_iff] at ha
-      rw [Set.range_eq_empty]
+    · rw [Set.range_eq_empty]
       exact bddAbove_empty
-  · by_cases h : Nonempty α
+  · by_cases! h : Nonempty α
     · apply ciSup_le
       intro a
-      by_cases ha : Nonempty (a ∈ s)
+      by_cases! ha : Nonempty (a ∈ s)
       · apply ciSup_le
         simp only [nonempty_prop] at ha
         apply Finset.le_sup
-      · rw [not_nonempty_iff] at ha
-        rw [ciSup_of_empty]
+      · rw [ciSup_of_empty]
         exact bot_le
-    · rw [not_nonempty_iff] at h
-      rw [ciSup_of_empty]
+    · rw [ciSup_of_empty]
       exact bot_le

Carleson/ToMathlib/MeasureTheory/Function/AEEqFun.lean

@@ -3,13 +3,15 @@ import Carleson.ToMathlib.Misc
 
 open MeasureTheory Finset
 
+-- Upstreaming status: seems ready for upstreaming
+
 theorem AEEqFun.mk_sum {α E ι : Type*} {m0 : MeasurableSpace α}
     {μ : Measure α} [inst : NormedAddCommGroup E] [DecidableEq ι] {s : Finset ι} {f : ι → α → E}
     (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) :
       AEEqFun.mk (∑ i ∈ s, f i) (Finset.aestronglyMeasurable_sum s hf) =
       ∑ i ∈ s.attach, AEEqFun.mk (f ↑i) (hf i (Finset.coe_mem i)) := by
   induction s using Finset.induction_on with
-  | empty => aesop
+  | empty => simp only [sum_empty, attach_empty]; rfl
   | insert i s hi h =>
     simp_rw [sum_insert hi]
     have := fun i hi ↦ hf i (mem_insert_of_mem hi)

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

@@ -2,9 +2,12 @@ import Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
 
 open MeasureTheory
 
-lemma ContinuousMap.MemLp {α : Type*} {E : Type*} {m0 : MeasurableSpace α} {p : ENNReal} (μ : Measure α)
-    [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α]
-    [IsFiniteMeasure μ] (𝕜 : Type*) [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) : MemLp f p μ := by
+-- Upstreaming status: rename to `memLp`, then ready for upstreaming.
+
+lemma ContinuousMap.memLp {α E : Type*} {m0 : MeasurableSpace α} {p : ENNReal} (μ : Measure α)
+    [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E]
+    [CompactSpace α] [IsFiniteMeasure μ] [Fact (1 ≤ p)]
+    (𝕜 : Type*) [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) : MemLp f p μ := by
   have := Lp.mem_Lp_iff_memLp.mp (Subtype.val_prop (ContinuousMap.toLp p μ 𝕜 f))
   rw [ContinuousMap.coe_toLp, memLp_congr_ae (ContinuousMap.coeFn_toAEEqFun _ _)] at this
   exact this

Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean

@@ -2,6 +2,9 @@ import Mathlib.Algebra.Order.Pi
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
 import Mathlib.MeasureTheory.Function.SimpleFunc
 
+-- Upstreaming status: under active development by @ldiedering.
+-- Wait for the file to stabilise first.
+
 noncomputable section
 
 open Set hiding restrict restrict_apply

Carleson/ToMathlib/Order/CompleteLattice/Basic.lean

@@ -1,6 +1,8 @@
 import Mathlib.Order.CompleteLattice.Basic
 import Carleson.ToMathlib.Order.ConditionallyCompleteLattice.Basic
 
+-- Upstreaming status: under active development by @ldiedering
+-- Wait for the file to stabilise first.
 
 --currently unused
 theorem iSup_eq_iSup {α : Type*} {ι ι' : Sort*} [CompleteLattice α] {f : ι → α} {g : ι' → α}

Carleson/ToMathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -1,6 +1,9 @@
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.ConditionallyCompleteLattice.Indexed
 
+-- Upstreaming status: under active development by @ldiedering
+-- Wait for the file to stabilise first.
+
 theorem ciSup_le_ciSup {α : Type*} {ι ι' : Sort*} [Nonempty ι] [ConditionallyCompleteLattice α]
   {f : ι → α} {g : ι' → α} (h₀ : ∀ i, ∃ j, f i ≤ g j) (hg : BddAbove (Set.range g)) :
     ⨆ i, f i ≤ ⨆ j, g j := by
@@ -47,9 +50,8 @@ theorem ciSup_eq_ciSup {α : Type*} {ι ι' : Sort*} [ConditionallyCompleteLinea
     rcases h₀ i with ⟨j, _⟩
     exact hι' ⟨j⟩
   have hι' : ¬ Nonempty ι' := by
-    intro hι'
-    rcases hι' with ⟨j⟩
+    intro ⟨j⟩
     rcases h₁ j with ⟨i, _⟩
     exact hι ⟨i⟩
-  simp at hι hι'
+  push_neg at hι hι'
   rw [iSup_of_empty', iSup_of_empty']