Cleanup

Add some \leanok's in chapter 11
Move some lemmas from HardyLittlewood to ToMathlib
Fix some lemma/section numbers.

Carleson/Classical/Approximation.lean

@@ -1,4 +1,4 @@
-/- The arguments in this file replace section 10.2 (Piecewise constant functions) from the paper. -/
+/- The arguments in this file contains section 11.2 (smooth functions) from the paper. -/
 
 import Carleson.MetricCarleson
 import Carleson.Classical.Basic

Carleson/Classical/Basic.lean

@@ -190,7 +190,7 @@ lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_l
         · simp [pow_two_nonneg]
         · linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
 
-/-Slightly weaker version of Lemma 10.11 (lower secant bound) with simplified constant. -/
+/-Slightly weaker version of Lemma 11..1.9 (lower secant bound) with simplified constant. -/
 lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)) (xAbs : η ≤ |x|) :
     η / 2 ≤ Complex.abs (1 - Complex.exp (Complex.I * x)) := by
   by_cases ηpos : η < 0

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -1,4 +1,4 @@
-/- This file contains the proof of Lemma 10.4, from section 10.7-/
+/- This file contains the proof of Lemma 11.1.4, from section 11.7 -/
 
 import Carleson.MetricCarleson
 import Carleson.Classical.Basic
@@ -434,10 +434,10 @@ instance compatibleFunctions_R : CompatibleFunctions ℝ ℝ (2 ^ 4) where
     intro x R R' f
     exact integer_ball_cover.mono_nat (by norm_num)
 
---TODO : What is Lemma 10.34 (frequency ball growth) needed for?
+--TODO : What is Lemma 11.7.10 (frequency ball growth) needed for?
 
 instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
-  /- Lemma 10.36 (real van der Corput) from the paper. -/
+  /- Lemma 11.7.12 (real van der Corput) from the paper. -/
   norm_integral_exp_le := by
     intro x r ϕ K hK _ f g
     by_cases r_pos : 0 ≥ r
@@ -599,7 +599,7 @@ lemma CarlesonOperatorReal_le_CarlesonOperator : T ≤ CarlesonOperator K := by
   ring_nf
 
 
-/- Lemma 10.4 (ENNReal version) -/
+/- Lemma 11.1.4 (ENNReal version) -/
 lemma rcarleson {F G : Set ℝ}
     (hF : MeasurableSet F) (hG : MeasurableSet G)
     (f : ℝ → ℂ) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x)

Carleson/Classical/ControlApproximationEffect.lean

@@ -1,4 +1,4 @@
-/- This file formalizes section 10.8 (The error bound) from the paper. -/
+/- This file formalizes section 11.6 (The error bound) from the paper. -/
 import Carleson.MetricCarleson
 import Carleson.Classical.Helper
 import Carleson.Classical.Basic
@@ -181,7 +181,7 @@ lemma intervalIntegrable_mul_dirichletKernel'_max' {x : ℝ} (hx : x ∈ Set.Icc
 lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
       ∫ (y : ℝ) in x - Real.pi..x + Real.pi,
         g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))
-    = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, 
+    = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1},
         g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
   calc _
     _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 Real.pi}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
@@ -527,7 +527,7 @@ lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤
 --TODO: add doc-strings !
 
 
-/-ENNReal version of a generalized Lemma 10.3 (control approximation effect).-/
+/-ENNReal version of a generalized Lemma 11.1.3 (control approximation effect).-/
 --added subset assumption
 --changed interval to match the interval in the theorem
 lemma control_approximation_effect {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real.pi) {δ : ℝ} (hδ : 0 < δ)

Carleson/Classical/DirichletKernel.lean

@@ -57,7 +57,7 @@ lemma dirichletKernel'_periodic {N : ℕ} : Function.Periodic (dirichletKernel'
 lemma dirichletKernel'_measurable {N : ℕ} : Measurable (dirichletKernel' N) :=
   by apply Measurable.add <;> apply Measurable.div <;> measurability
 
-/-Second part of Lemma 10.10 (Dirichlet kernel) from the paper.-/
+/-Second part of Lemma 11.1.8 (Dirichlet kernel) from the paper.-/
 lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) :
     dirichletKernel N x = dirichletKernel' N x := by
   have : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x
@@ -167,7 +167,7 @@ lemma norm_dirichletKernel'_le {N : ℕ} {x : ℝ} : ‖dirichletKernel' N x‖
     rw [dirichletKernel'_eq_zero h, norm_zero]
     linarith
 
-/-First part of lemma 10.10 (Dirichlet kernel) from the paper.-/
+/-First part of lemma 11.1.8 (Dirichlet kernel) from the paper.-/
 /-TODO (maybe): correct statement so that the integral is taken over the interval [-pi, pi] -/
 lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) :
     partialFourierSum f N x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y)  := by

Carleson/Classical/HilbertKernel.lean

@@ -32,7 +32,7 @@ def K (x y : ℝ) : ℂ := k (x - y)
 @[measurability]
 lemma Hilbert_kernel_measurable : Measurable (Function.uncurry K) := k_measurable.comp measurable_sub
 
-/- Lemma 10.13 (Hilbert kernel bound) -/
+/- Lemma 11.1.11 (Hilbert kernel bound) -/
 lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x - y|) := by
   by_cases h : 0 < |x - y| ∧ |x - y| < 1
   · calc ‖K x y‖
@@ -202,7 +202,7 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧
   · rwa [abs_neg, abs_of_nonneg yy'nonneg.2]
   · rwa [abs_neg, abs_of_nonneg yy'nonneg.1]
 
-/- Lemma 10.14 (Hilbert kernel regularity) -/
+/- Lemma 11.1.12 (Hilbert kernel regularity) -/
 lemma Hilbert_kernel_regularity {x y y' : ℝ} :
     2 * |y - y'| ≤ |x - y| → ‖K x y - K x y'‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)  := by
   rw [K, K]

Carleson/Classical/VanDerCorput.lean

@@ -1,4 +1,4 @@
-/- This file formalizes section 10.6 (The proof of the van der Corput Lemma) from the paper. -/
+/- This file formalizes section 11.4 (The proof of the van der Corput Lemma) from the paper. -/
 import Carleson.Classical.Basic
 
 

Carleson/DiscreteCarleson.lean

@@ -1,7 +1,5 @@
 import Carleson.Forest
 import Carleson.HardyLittlewood
--- import Carleson.Proposition2
--- import Carleson.Proposition3
 
 open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology
 open scoped ENNReal
@@ -325,7 +323,7 @@ lemma first_exception' : volume (G₁ : Set X) ≤ 2 ^ (- 5 : ℤ) * volume G :=
     simp only [Finset.mem_image, mem_toFinset, 𝓑] at hz
     rcases hz with ⟨p, h, rfl⟩
     simpa [u, lintegral_indicator, Measure.restrict_apply, measurableSet_F, r, h] using (hr h).2.le
-  have ineq := measure_biUnion_le_lintegral' (A := defaultA a) 𝓑 K0 hu h2u
+  have ineq := Finset.measure_biUnion_le_lintegral (A := defaultA a) 𝓑 K0 hu h2u
   simp only [u, lintegral_indicator, measurableSet_F, Pi.one_apply, lintegral_const,
     MeasurableSet.univ, Measure.restrict_apply, univ_inter, one_mul] at ineq
   rw [← mul_le_mul_left K0.ne.symm K_ne_top]

Carleson/HardyLittlewood.lean

@@ -30,15 +30,11 @@ M_𝓑 in the blueprint. -/
 abbrev MB (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) :=
   maximalFunction μ 𝓑 c r 1 u x
 
-lemma covering_separable_space (X : Type*) [MetricSpace X] [SeparableSpace X] :
+lemma covering_separable_space (X : Type*) [PseudoMetricSpace X] [SeparableSpace X] :
     ∃ C : Set X, C.Countable ∧ ∀ r > 0, ⋃ c ∈ C, ball c r = univ := by
-  obtain ⟨C, hC, h2C⟩ := exists_countable_dense X
-  use C, hC
-  simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball]
-  intro r hr x
-  simp_rw [Dense, Metric.mem_closure_iff] at h2C
-  exact h2C x r hr
+  simp_rw [← Metric.dense_iff_iUnion_ball, exists_countable_dense]
 
+-- this can be removed next Mathlib bump
 /-- A slight generalization of Mathlib's version, with 5 replaced by τ. Already PR'd -/
 theorem Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall' {α ι} [MetricSpace α]
     (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) (τ : ℝ) (hτ : 3 < τ) :
@@ -80,7 +76,7 @@ theorem Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall' {α ι}
 proof of `first_exception` in DiscreteCarleson.lean. But everything involved there is finite, so
 you can prove this with `ℝ≥0` and deal with casting between `ℝ≥0` and `ℝ≥0∞` there, if that turns
 out to be easier. -/
-theorem measure_biUnion_le_lintegral (h𝓑 : 𝓑.Countable) {l : ℝ≥0∞} (hl : 0 < l)
+theorem Set.Countable.measure_biUnion_le_lintegral (h𝓑 : 𝓑.Countable) {l : ℝ≥0∞} (hl : 0 < l)
     {u : X → ℝ≥0∞} (hu : AEStronglyMeasurable u μ)
     (R : ℝ) (hR : ∀ a ∈ 𝓑, r a ≤ R)
     (h2u : ∀ i ∈ 𝓑, l * μ (ball (c i) (r i)) ≤ ∫⁻ x in ball (c i) (r i), u x ∂μ) :
@@ -96,56 +92,18 @@ theorem measure_biUnion_le_lintegral (h𝓑 : 𝓑.Countable) {l : ℝ≥0∞} (
     _ = A ^ 2 * ∫⁻ x in ⋃ i ∈ B, ball (c i) (r i), u x ∂μ := sorry -- does this exist in Mathlib?
     _ ≤ A ^ 2 * ∫⁻ x, u x ∂μ := sorry
 
-theorem measure_biUnion_le_lintegral' (𝓑 : Finset ι) {l : ℝ≥0∞} (hl : 0 < l)
+protected theorem Finset.measure_biUnion_le_lintegral (𝓑 : Finset ι) {l : ℝ≥0∞} (hl : 0 < l)
     {u : X → ℝ≥0∞} (hu : AEStronglyMeasurable u μ)
     (h2u : ∀ i ∈ 𝓑, l * μ (ball (c i) (r i)) ≤ ∫⁻ x in ball (c i) (r i), u x ∂μ) :
     l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ A ^ 2 * ∫⁻ x, u x ∂μ  :=
   let ⟨c, hc⟩ := (𝓑.image r).exists_le
-  measure_biUnion_le_lintegral 𝓑.countable_toSet hl hu c (by simpa using hc) h2u
-
-attribute [gcongr] Set.indicator_le_indicator mulIndicator_le_mulIndicator_of_subset
-attribute [simp] MeasureTheory.laverage_const
-
-
-namespace MeasureTheory
-variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {s : Set α}
-  {F : Type*} [NormedAddCommGroup F]
-lemma laverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) :
-    ⨍⁻ a, f a ∂μ ≤ ⨍⁻ a, g a ∂μ := by
-  exact lintegral_mono_ae <| h.filter_mono <| Measure.ae_mono' Measure.smul_absolutelyContinuous
-
-lemma setLAverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) :
-    ⨍⁻ a in s, f a ∂μ ≤ ⨍⁻ a in s, g a ∂μ := by
-  refine laverage_mono_ae <| h.filter_mono <| ae_mono Measure.restrict_le_self
-
-lemma setLaverage_const_le {c : ℝ≥0∞} : ⨍⁻ _x in s, c ∂μ ≤ c := by
-  simp_rw [setLaverage_eq, lintegral_const, Measure.restrict_apply MeasurableSet.univ,
-    univ_inter, div_eq_mul_inv, mul_assoc]
-  conv_rhs => rw [← mul_one c]
-  gcongr
-  exact ENNReal.mul_inv_le_one (μ s)
-
-theorem snormEssSup_lt_top_of_ae_ennnorm_bound {f : α → F} {C : ℝ≥0∞} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) :
-    snormEssSup f μ ≤ C :=
-  essSup_le_of_ae_le C hfC
-
-@[simp]
-lemma ENNReal.nnorm_toReal {x : ℝ≥0∞} : ‖x.toReal‖₊ = x.toNNReal := by
-  ext; simp [ENNReal.toReal]
-
-end MeasureTheory
+  𝓑.countable_toSet.measure_biUnion_le_lintegral hl hu c (by simpa using hc) h2u
 
 protected theorem MeasureTheory.AEStronglyMeasurable.maximalFunction {p : ℝ}
     {u : X → E} (hu : AEStronglyMeasurable u μ) (h𝓑 : 𝓑.Countable) :
     AEStronglyMeasurable (maximalFunction μ 𝓑 c r p u) μ := by
   sorry
 
-theorem MeasureTheory.AEStronglyMeasurable.ennreal_toReal
-    {u : X → ℝ≥0∞} (hu : AEStronglyMeasurable u μ) :
-    AEStronglyMeasurable (fun x ↦ (u x).toReal) μ := by
-  refine aestronglyMeasurable_iff_aemeasurable.mpr ?_
-  exact ENNReal.measurable_toReal.comp_aemeasurable hu.aemeasurable
-
 theorem MeasureTheory.AEStronglyMeasurable.maximalFunction_toReal {p : ℝ}
     {u : X → E} (hu : AEStronglyMeasurable u μ) (h𝓑 : 𝓑.Countable) :
     AEStronglyMeasurable (fun x ↦ maximalFunction μ 𝓑 c r p u x |>.toReal) μ :=
@@ -239,7 +197,7 @@ lemma countable_globalMaximalFunction :
     (covering_separable_space X).choose ×ˢ (univ : Set ℤ) |>.Countable :=
   (covering_separable_space X).choose_spec.1.prod countable_univ
 
--- prove if needed. Use `MB_le_snormEssSup`
+-- prove only if needed. Use `MB_le_snormEssSup`
 theorem globalMaximalFunction_lt_top {p : ℝ≥0} (hp₁ : 1 ≤ p)
     {u : X → E} (hu : AEStronglyMeasurable u μ) (hu : IsBounded (range u)) {x : X} :
     globalMaximalFunction μ p u  x < ∞ := by

Carleson/ToMathlib/Misc.lean

@@ -1,5 +1,6 @@
 import Mathlib.Analysis.Convex.PartitionOfUnity
 import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.MeasureTheory.Integral.Average
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 import Mathlib.Topology.MetricSpace.Holder
@@ -14,12 +15,32 @@ import Carleson.ToMathlib.MeasureReal
 
 open Function Set
 open scoped ENNReal
+
+section Metric
+
 attribute [gcongr] Metric.ball_subset_ball
 
+
+lemma Metric.dense_iff_iUnion_ball {X : Type*} [PseudoMetricSpace X] (s : Set X) :
+    Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ := by
+  simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, Metric.mem_closure_iff,
+    forall_comm (α := X)]
+
+theorem PseudoMetricSpace.dist_eq_of_dist_zero {X : Type*} [PseudoMetricSpace X] (x : X) {y y' : X}
+    (hyy' : dist y y' = 0) : dist x y = dist x y' :=
+  dist_comm y x ▸ dist_comm y' x ▸ sub_eq_zero.1 (abs_nonpos_iff.1 (hyy' ▸ abs_dist_sub_le y y' x))
+
+end Metric
+
+section Order
+
 lemma IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i := by
   simp_rw [le_antisymm_iff, h j, true_and]
   refine ⟨(· (h j)), swap (fun _ ↦ h · |>.trans ·)⟩
 
+end Order
+
+section Int
 
 theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < z + 1 := by
   rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right]
@@ -39,6 +60,10 @@ theorem Int.Icc_of_eq_sub_1 {a b : ℤ} (h : a = b - 1) : Finset.Icc a b = {a, b
     · exact Finset.mem_Icc.2 ⟨le_refl t, hab⟩
     · rw [Finset.mem_singleton.1 hb]; exact Finset.mem_Icc.2 ⟨hab, le_refl b⟩
 
+end Int
+
+section ENNReal
+
 lemma tsum_one_eq' {α : Type*} (s : Set α) : ∑' (_:s), (1 : ℝ≥0∞) = s.encard := by
   if hfin : s.Finite then
     have hfin' : Finite s := by exact hfin
@@ -80,10 +105,6 @@ lemma ENNReal.tsum_const_eq' {α : Type*} (s : Set α) (c : ℝ≥0∞) :
   nth_rw 1 [← one_mul c]
   rw [ENNReal.tsum_mul_right,tsum_one_eq']
 
-theorem PseudoMetricSpace.dist_eq_of_dist_zero {X : Type*} [PseudoMetricSpace X] (x : X) {y y' : X}
-    (hyy' : dist y y' = 0) : dist x y = dist x y' :=
-  dist_comm y x ▸ dist_comm y' x ▸ sub_eq_zero.1 (abs_nonpos_iff.1 (hyy' ▸ abs_dist_sub_le y y' x))
-
 /-! ## `ENNReal` manipulation lemmas -/
 
 lemma ENNReal.sum_geometric_two_pow_toNNReal {k : ℕ} (hk : k > 0) :
@@ -110,10 +131,18 @@ lemma ENNReal.sum_geometric_two_pow_neg_two :
   conv_lhs => enter [1, n, 2]; rw [← Nat.cast_two]
   rw [ENNReal.sum_geometric_two_pow_toNNReal zero_lt_two]; norm_num
 
-/-! ## Partitioning an interval -/
+end ENNReal
+
+section Indicator
+attribute [gcongr] Set.indicator_le_indicator mulIndicator_le_mulIndicator_of_subset
+end Indicator
+
 
 namespace MeasureTheory
 
+/-! ## Partitioning an interval -/
+
+
 lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc : 0 ≤ c) :
     ∫⁻ t in Ioc (a * c) (b * c), f t =
     ∑ l ∈ Finset.Ico a b, ∫⁻ t in Ioc (l * c) ((l + 1 : ℕ) * c), f t := by
@@ -132,6 +161,40 @@ lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc
 
 end MeasureTheory
 
+namespace MeasureTheory
+variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {s : Set α}
+  {F : Type*} [NormedAddCommGroup F]
+
+theorem AEStronglyMeasurable.ennreal_toReal {u : α → ℝ≥0∞} (hu : AEStronglyMeasurable u μ) :
+    AEStronglyMeasurable (fun x ↦ (u x).toReal) μ := by
+  refine aestronglyMeasurable_iff_aemeasurable.mpr ?_
+  exact ENNReal.measurable_toReal.comp_aemeasurable hu.aemeasurable
+
+lemma laverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) :
+    ⨍⁻ a, f a ∂μ ≤ ⨍⁻ a, g a ∂μ := by
+  exact lintegral_mono_ae <| h.filter_mono <| Measure.ae_mono' Measure.smul_absolutelyContinuous
+
+lemma setLAverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) :
+    ⨍⁻ a in s, f a ∂μ ≤ ⨍⁻ a in s, g a ∂μ := by
+  refine laverage_mono_ae <| h.filter_mono <| ae_mono Measure.restrict_le_self
+
+lemma setLaverage_const_le {c : ℝ≥0∞} : ⨍⁻ _x in s, c ∂μ ≤ c := by
+  simp_rw [setLaverage_eq, lintegral_const, Measure.restrict_apply MeasurableSet.univ,
+    univ_inter, div_eq_mul_inv, mul_assoc]
+  conv_rhs => rw [← mul_one c]
+  gcongr
+  exact ENNReal.mul_inv_le_one (μ s)
+
+theorem snormEssSup_lt_top_of_ae_ennnorm_bound {f : α → F} {C : ℝ≥0∞} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) :
+    snormEssSup f μ ≤ C :=
+  essSup_le_of_ae_le C hfC
+
+@[simp]
+lemma ENNReal.nnorm_toReal {x : ℝ≥0∞} : ‖x.toReal‖₊ = x.toNNReal := by
+  ext; simp [ENNReal.toReal]
+
+end MeasureTheory
+
 /-! ## `EquivalenceOn` -/
 
 /-- An equivalence relation on the set `s`. -/

Carleson/WeakType.lean

@@ -310,7 +310,6 @@ def HasBoundedStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAdd
   ∀ f : α → E, Memℒp f p μ → snorm f ∞ μ < ∞ → μ (support f) < ∞ →
   AEStronglyMeasurable (T f) ν ∧ snorm (T f) p' ν ≤ c * snorm f p μ
 
-
 lemma HasStrongType.hasWeakType (hp' : 1 ≤ p')
     (h : HasStrongType T p p' μ ν c) : HasWeakType T p p' μ ν c :=
   fun f hf ↦ ⟨(h f hf).1, (wnorm_le_snorm (h f hf).1 hp').trans (h f hf).2⟩