diff --git a/Carleson/ForestOperator/AlmostOrthogonality.lean b/Carleson/ForestOperator/AlmostOrthogonality.lean index c860e7c5..12e66456 100644 --- a/Carleson/ForestOperator/AlmostOrthogonality.lean +++ b/Carleson/ForestOperator/AlmostOrthogonality.lean @@ -337,7 +337,7 @@ lemma adjoint_tree_control (hu : u ∈ t) (hf : BoundedCompactSupport f) : eLpNorm f 2 volume := by gcongr · exact adjoint_tree_estimate hu hf - · exact hasStrongType_MB 𝓑_finite one_lt_two _ (hf.memℒp _) |>.2 + · exact hasStrongType_MB_finite 𝓑_finite one_lt_two _ (hf.memℒp _) |>.2 _ ≤ (C7_4_2 a * (1 : ℝ≥0∞) ^ (2 : ℝ)⁻¹ + CMB (defaultA a) 2 + 1) * eLpNorm f 2 volume := by simp_rw [add_mul] gcongr diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean index 8391f504..eb957dcd 100644 --- a/Carleson/HardyLittlewood.lean +++ b/Carleson/HardyLittlewood.lean @@ -2,16 +2,17 @@ import Carleson.DoublingMeasure import Carleson.RealInterpolation import Mathlib.MeasureTheory.Covering.Vitali -open MeasureTheory Metric Bornology Set TopologicalSpace Vitali Filter -open scoped NNReal ENNReal +open MeasureTheory Metric Bornology Set TopologicalSpace Vitali Filter ENNReal Pointwise +open scoped NNReal noncomputable section /-! This should roughly contain the contents of chapter 9. -/ section Prelude -variable (X : Type*) [PseudoMetricSpace X] [SeparableSpace X] +variable {X : Type*} [PseudoMetricSpace X] [SeparableSpace X] +variable (X) in /-- Lemma 9.0.2 -/ lemma covering_separable_space : ∃ C : Set X, C.Countable ∧ ∀ r > 0, ⋃ c ∈ C, ball c r = univ := by @@ -21,7 +22,6 @@ lemma countable_globalMaximalFunction : (covering_separable_space X).choose ×ˢ (univ : Set ℤ) |>.Countable := (covering_separable_space X).choose_spec.1.prod countable_univ --- [TODO] change the name? lemma exists_ball_subset_ball_two (c : X) {r : ℝ} (hr : 0 < r) : ∃ c' ∈ (covering_separable_space X).choose, ∃ m : ℤ, ball c r ⊆ ball c' (2 ^ m) ∧ 2 ^ m ≤ 2 * r ∧ ball c' (2 ^ m) ⊆ ball c (4 * r) := by @@ -93,16 +93,9 @@ lemma maximalFunction_eq_MB -- We will replace the criterion `P` used in `MeasureTheory.AESublinearOn.maximalFunction` with the -- weaker criterion `LocallyIntegrable` that is closed under addition and scalar multiplication. -variable (μ) in -private def P (f : X → E) : Prop := Memℒp f ∞ μ ∨ Memℒp f 1 μ - -private lemma LocallyIntegrable_of_P [BorelSpace X] [ProperSpace X] [IsFiniteMeasureOnCompacts μ] - {u : X → E} (hu : P μ u) : LocallyIntegrable u μ := by - refine hu.elim (Memℒp.locallyIntegrable · le_top) (Memℒp.locallyIntegrable · le_rfl) - -- The average that appears in the definition of `MB` variable (μ c r) in -private def T (i : ι) (u : X → E) := (⨍⁻ (y : X) in ball (c i) (r i), ‖u y‖₊ ∂μ).toReal +private def T (i : ι) (u : X → E) := ⨍⁻ (y : X) in ball (c i) (r i), ‖u y‖₊ ∂μ -- move lemma MeasureTheory.LocallyIntegrable.integrableOn_of_isBounded [ProperSpace X] @@ -125,26 +118,20 @@ lemma MeasureTheory.LocallyIntegrable.laverage_ball_lt_top private lemma T.add_le [MeasurableSpace E] [BorelSpace E] [BorelSpace X] [ProperSpace X] (i : ι) {f g : X → E} (hf : LocallyIntegrable f μ) (hg : LocallyIntegrable g μ) : - ‖T μ c r i (f + g)‖ ≤ ‖T μ c r i f‖ + ‖T μ c r i g‖ := by - simp only [T, Pi.add_apply, Real.norm_eq_abs, ENNReal.abs_toReal] - rw [← ENNReal.toReal_add hf.laverage_ball_lt_top.ne hg.laverage_ball_lt_top.ne, ENNReal.toReal_le_toReal] - · rw [← laverage_add_left hf.integrableOn_ball.aemeasurable.ennnorm] - exact laverage_mono (fun x ↦ ENNNorm_add_le (f x) (g x)) - · exact (hf.add hg).laverage_ball_lt_top.ne - · exact (ENNReal.add_lt_top.2 ⟨hf.laverage_ball_lt_top, hg.laverage_ball_lt_top⟩).ne - -private lemma T.smul [NormedSpace ℝ E] (i : ι) : ∀ {f : X → E} {d : ℝ}, LocallyIntegrable f μ → - d ≥ 0 → T μ c r i (d • f) = d • T μ c r i f := by - intro f d _ hd - simp_rw [T, Pi.smul_apply, smul_eq_mul] - nth_rewrite 2 [← (ENNReal.toReal_ofReal hd)] - rw [← ENNReal.toReal_mul] - congr - rw [laverage_const_mul ENNReal.ofReal_ne_top] - congr - ext x - simp only [nnnorm_smul, ENNReal.coe_mul, ← Real.toNNReal_eq_nnnorm_of_nonneg hd] - congr + ‖T μ c r i (f + g)‖ₑ ≤ ‖T μ c r i f‖ₑ + ‖T μ c r i g‖ₑ := by + simp only [T, Pi.add_apply, enorm_eq_self] + rw [← laverage_add_left hf.integrableOn_ball.aemeasurable.ennnorm] + exact laverage_mono (fun x ↦ ENNNorm_add_le (f x) (g x)) + +-- move +lemma NNReal.smul_ennreal_eq_mul (x : ℝ≥0) (y : ℝ≥0∞) : x • y = x * y := rfl + +private lemma T.smul [NormedSpace ℝ E] (i : ι) : ∀ {f : X → E} {d : ℝ≥0}, LocallyIntegrable f μ → + T μ c r i (d • f) = d • T μ c r i f := by + intro f d _ + simp_rw [T, Pi.smul_apply, NNReal.smul_def, NNReal.smul_ennreal_eq_mul, + laverage_const_mul ENNReal.coe_ne_top] + simp [nnnorm_smul] -- todo: move -- slightly more general than the Mathlib version @@ -276,7 +263,7 @@ theorem MB_le_eLpNormEssSup {u : X → E} {x : X} : MB μ 𝓑 c r u x ≤ eLpNo fun _x ↦ ⨍⁻ _y in ball (c i) (r i), eLpNormEssSup u μ ∂μ := by simp_rw [MB, maximalFunction, inv_one, ENNReal.rpow_one] gcongr - exact setLAverage_mono_ae <| coe_nnnorm_ae_le_eLpNormEssSup u μ + exact coe_nnnorm_ae_le_eLpNormEssSup u μ _ ≤ ⨆ i ∈ 𝓑, (ball (c i) (r i)).indicator (x := x) fun _x ↦ eLpNormEssSup u μ := by gcongr; apply setLaverage_const_le _ ≤ ⨆ i ∈ 𝓑, eLpNormEssSup u μ := by gcongr; apply indicator_le_self @@ -292,44 +279,16 @@ protected theorem HasStrongType.MB_top [BorelSpace X] (h𝓑 : 𝓑.Countable) : simp_rw [enorm_eq_nnnorm, ENNReal.nnorm_toReal] exact ENNReal.coe_toNNReal_le_self |>.trans MB_le_eLpNormEssSup -protected theorem MeasureTheory.AESublinearOn.maximalFunction - [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] - [IsFiniteMeasureOnCompacts μ] [ProperSpace X] (h𝓑 : 𝓑.Finite) : - AESublinearOn (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal) - (fun f ↦ Memℒp f ∞ μ ∨ Memℒp f 1 μ) 1 μ := by - apply AESublinearOn.antitone LocallyIntegrable_of_P - simp only [MB, maximalFunction, ENNReal.rpow_one, inv_one] - apply AESublinearOn.biSup (P := (LocallyIntegrable · μ)) 𝓑 h𝓑.countable _ _ - LocallyIntegrable.add (fun hf _ ↦ hf.smul _) - · intro i _ - let B := ball (c i) (r i) - have (u : X → E) (x : X) : (B.indicator (fun _ ↦ ⨍⁻ y in B, ‖u y‖₊ ∂μ) x).toReal = - (B.indicator (fun _ ↦ (⨍⁻ y in B, ‖u y‖₊ ∂μ).toReal) x) := by - by_cases hx : x ∈ B <;> simp [hx] - simp_rw [this] - apply (AESublinearOn.const (T μ c r i) (LocallyIntegrable · μ) (T.add_le i) - (fun f d ↦ T.smul i)).indicator - · refine fun f hf ↦ ae_of_all _ (fun x ↦ ?_) - by_cases h𝓑' : 𝓑.Nonempty; swap - · simp [not_nonempty_iff_eq_empty.mp h𝓑'] - have ⟨i, _, hi⟩ := h𝓑.biSup_eq h𝓑' (fun i ↦ (ball (c i) (r i)).indicator - (fun _ ↦ ⨍⁻ y in ball (c i) (r i), ‖f y‖₊ ∂μ) x) - rw [hi] - by_cases hx : x ∈ ball (c i) (r i) - · simpa [hx] using hf.laverage_ball_lt_top.ne - · simp [hx] - /- The proof is roughly between (9.0.12)-(9.0.22). -/ -open ENNReal in -variable (μ) in protected theorem HasWeakType.MB_one [BorelSpace X] (h𝓑 : 𝓑.Countable) {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) : - HasWeakType (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal) 1 1 μ μ (A ^ 2) := by + HasWeakType (MB (E := E) μ 𝓑 c r) 1 1 μ μ (A ^ 2) := by intro f _ - use AEStronglyMeasurable.maximalFunction_toReal h𝓑 + use AEStronglyMeasurable.maximalFunction h𝓑 let Bₗ (ℓ : ℝ≥0∞) := { i ∈ 𝓑 | ∫⁻ y in (ball (c i) (r i)), ‖f y‖₊ ∂μ ≥ ℓ * μ (ball (c i) (r i)) } - simp only [wnorm, one_ne_top, reduceIte, wnorm', one_toReal, inv_one, rpow_one, coe_pow, eLpNorm, - one_ne_zero, eLpNorm', ne_eq, not_false_eq_true, div_self, iSup_le_iff] + simp only [wnorm, one_ne_top, wnorm', one_toReal, inv_one, ENNReal.rpow_one, reduceIte, + ENNReal.coe_pow, eLpNorm, one_ne_zero, eLpNorm', ne_eq, not_false_eq_true, div_self, + iSup_le_iff] intro t by_cases ht : t = 0 · simp [ht] @@ -338,21 +297,75 @@ protected theorem HasWeakType.MB_one [BorelSpace X] (h𝓑 : 𝓑.Countable) (u := fun x ↦ ‖f x‖₊) (R := R) ?_ ?_) · refine mul_left_mono <| μ.mono (fun x hx ↦ mem_iUnion₂.mpr ?_) -- We need a ball in `Bₗ t` containing `x`. Since `MB μ 𝓑 c r f x` is large, such a ball exists - simp only [nnorm_toReal, mem_setOf_eq] at hx - replace hx := lt_of_lt_of_le hx coe_toNNReal_le_self - simp only [MB, maximalFunction, rpow_one, inv_one] at hx + simp only [mem_setOf_eq] at hx + -- replace hx := lt_of_lt_of_le hx coe_toNNReal_le_self + simp only [MB, maximalFunction, ENNReal.rpow_one, inv_one] at hx obtain ⟨i, ht⟩ := lt_iSup_iff.mp hx replace hx : x ∈ ball (c i) (r i) := - by_contradiction <| fun h ↦ not_lt_of_ge (zero_le t) (coe_lt_coe.mp <| by simp [h] at ht) + by_contradiction <| fun h ↦ not_lt_of_ge (zero_le t) (ENNReal.coe_lt_coe.mp <| by simp [h] at ht) refine ⟨i, ?_, hx⟩ -- It remains only to confirm that the chosen ball is actually in `Bₗ t` simp only [ge_iff_le, mem_setOf_eq, Bₗ] have hi : i ∈ 𝓑 := - by_contradiction <| fun h ↦ not_lt_of_ge (zero_le t) (coe_lt_coe.mp <| by simp [h] at ht) + by_contradiction <| fun h ↦ not_lt_of_ge (zero_le t) (ENNReal.coe_lt_coe.mp <| by simp [h] at ht) exact ⟨hi, mul_le_of_le_div <| le_of_lt (by simpa [setLaverage_eq, hi, hx] using ht)⟩ · exact fun i hi ↦ hR i (mem_of_mem_inter_left hi) · exact fun i hi ↦ hi.2.trans (setLIntegral_mono' measurableSet_ball fun x _ ↦ by simp) +protected theorem HasWeakType.MB_one_toReal [BorelSpace X] (h𝓑 : 𝓑.Countable) + {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) : + HasWeakType (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal) 1 1 μ μ (A ^ 2) := + HasWeakType.MB_one h𝓑 hR |>.ennreal_toReal + +include A in +theorem MB_ae_ne_top [BorelSpace X] (h𝓑 : 𝓑.Countable) + {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) + {u : X → E} (hu : Memℒp u 1 μ) : ∀ᵐ x : X ∂μ, MB μ 𝓑 c r u x ≠ ∞ := by + simpa only [enorm_eq_self] using HasWeakType.MB_one h𝓑 hR |>.memWℒp hu |>.ae_ne_top + +-- move +lemma MeasureTheory.Memℒp.eLpNormEssSup_lt_top {α} [MeasurableSpace α] {μ : Measure α} + {u : α → E} (hu : Memℒp u ⊤ μ) : eLpNormEssSup u μ < ⊤ := by + simp_rw [Memℒp, eLpNorm_exponent_top] at hu + exact hu.2 + +include A in +protected theorem MeasureTheory.AESublinearOn.maximalFunction + [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] + [IsFiniteMeasureOnCompacts μ] [ProperSpace X] (h𝓑 : 𝓑.Countable) + {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) : + AESublinearOn (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x) + (fun f ↦ Memℒp f ∞ μ ∨ Memℒp f 1 μ) 1 μ := by + let P := fun g ↦ g ∈ {f : X → E | Memℒp f ∞ μ} + {f | Memℒp f 1 μ} + have hP : ∀ {g}, P g → LocallyIntegrable g μ := by + rintro _ ⟨f, hf, g, hg, rfl⟩ + exact (Memℒp.locallyIntegrable hf le_top).add (Memℒp.locallyIntegrable hg le_rfl) + simp only [MB, maximalFunction, ENNReal.rpow_one, inv_one] + refine AESublinearOn.biSup2 (P := (Memℒp · ⊤ μ)) (Q := (Memℒp · 1 μ)) h𝓑 ?_ ?_ zero_memℒp zero_memℒp Memℒp.add Memℒp.add + ?_ ?_ ?_ + · intro u hu + refine .of_forall fun x ↦ ?_ + rw [← lt_top_iff_ne_top] + calc + _ ≤ ⨆ i ∈ 𝓑, (ball (c i) (r i)).indicator + (fun x ↦ ⨍⁻ (y : X) in ball (c i) (r i), eLpNormEssSup u μ ∂μ) x := by + gcongr; exact ENNReal.ae_le_essSup fun y ↦ ↑‖u y‖₊ + _ ≤ ⨆ i ∈ 𝓑, (ball (c i) (r i)).indicator (fun x ↦ eLpNormEssSup u μ) x := by + gcongr; exact setLaverage_const_le + _ ≤ ⨆ i ∈ 𝓑, eLpNormEssSup u μ := by gcongr; apply indicator_le_self + _ ≤ ⨆ i : ι, eLpNormEssSup u μ := by gcongr; exact iSup_const_le + _ ≤ eLpNormEssSup u μ := iSup_const_le + _ < ⊤ := hu.eLpNormEssSup_lt_top + · intro u hu + have := MB_ae_ne_top (u := u) (μ := μ) (c := c) h𝓑 hR hu + filter_upwards [this] with x hx + simpa [MB, maximalFunction] using hx + · intro f c hf; rw [NNReal.smul_def]; exact hf.const_smul _ + · intro f c hf; rw [NNReal.smul_def]; exact hf.const_smul _ + · intro i _ + refine AESublinearOn.const (T μ c r i) P (fun hf hg ↦ T.add_le i (hP hf) (hP hg)) + (fun f d hf ↦ T.smul i (hP hf)) |>.indicator _ + /-- The constant factor in the statement that `M_𝓑` has strong type. -/ irreducible_def CMB (A p : ℝ≥0) : ℝ≥0 := C_realInterpolation ⊤ 1 ⊤ 1 p 1 (A ^ 2) 1 p⁻¹ @@ -360,7 +373,7 @@ irreducible_def CMB (A p : ℝ≥0) : ℝ≥0 := C_realInterpolation ⊤ 1 ⊤ 1 Use the real interpolation theorem instead of following the blueprint. -/ lemma hasStrongType_MB [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [Nonempty X] [μ.IsOpenPosMeasure] - (h𝓑 : 𝓑.Finite) {p : ℝ≥0} (hp : 1 < p) : + (h𝓑 : 𝓑.Countable) {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) {p : ℝ≥0} (hp : 1 < p) : HasStrongType (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal) p p μ μ (CMB A p) := by have h2p : 0 < p := by positivity @@ -369,9 +382,20 @@ lemma hasStrongType_MB [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [B (T := fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal) (p := p) (q := p) (A := 1) ⟨ENNReal.zero_lt_top, le_rfl⟩ ⟨zero_lt_one, le_rfl⟩ (by norm_num) zero_lt_one (by simp [inv_lt_one_iff₀, hp, h2p] : p⁻¹ ∈ _) zero_lt_one (pow_pos (A_pos μ) 2) (by simp [ENNReal.coe_inv h2p.ne']) (by simp [ENNReal.coe_inv h2p.ne']) - (fun f _ ↦ AEStronglyMeasurable.maximalFunction_toReal h𝓑.countable) - (AESublinearOn.maximalFunction h𝓑).1 (HasStrongType.MB_top h𝓑.countable |>.hasWeakType le_top) - (HasWeakType.MB_one μ h𝓑.countable (h𝓑.exists_image_le r).choose_spec) + (fun f _ ↦ AEStronglyMeasurable.maximalFunction_toReal h𝓑) + _ (HasStrongType.MB_top h𝓑 |>.hasWeakType le_top) + (HasWeakType.MB_one_toReal h𝓑 hR) + apply ((AESublinearOn.maximalFunction h𝓑 hR).toReal _).1 + sorry -- already proven above, we will likely refactor this away + +lemma hasStrongType_MB_finite [BorelSpace X] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] + [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [Nonempty X] [μ.IsOpenPosMeasure] + (h𝓑 : 𝓑.Finite) {p : ℝ≥0} (hp : 1 < p) : + HasStrongType (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal) + p p μ μ (CMB A p) := + hasStrongType_MB h𝓑.countable (Finite.exists_image_le h𝓑 _).choose_spec hp + + /-- The constant factor in the statement that `M_{𝓑, p}` has strong type. -/ irreducible_def C2_0_6 (A p₁ p₂ : ℝ≥0) : ℝ≥0 := CMB A (p₂ / p₁) ^ (p₁⁻¹ : ℝ) @@ -379,11 +403,11 @@ irreducible_def C2_0_6 (A p₁ p₂ : ℝ≥0) : ℝ≥0 := CMB A (p₂ / p₁) /-- Equation (2.0.44). The proof is given between (9.0.34) and (9.0.36). -/ theorem hasStrongType_maximalFunction [BorelSpace X] [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [Nonempty X] [μ.IsOpenPosMeasure] - {p₁ p₂ : ℝ≥0} (h𝓑 : 𝓑.Finite) (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) : + {p₁ p₂ : ℝ≥0} (h𝓑 : 𝓑.Countable) {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) : HasStrongType (fun (u : X → E) (x : X) ↦ maximalFunction μ 𝓑 c r p₁ u x |>.toReal) p₂ p₂ μ μ (C2_0_6 A p₁ p₂) := fun v mlpv ↦ by dsimp only - constructor; · exact AEStronglyMeasurable.maximalFunction_toReal h𝓑.countable + constructor; · exact AEStronglyMeasurable.maximalFunction_toReal h𝓑 have cp₁p : 0 < (p₁ : ℝ) := by positivity have p₁n : p₁ ≠ 0 := by exact_mod_cast cp₁p.ne' conv_lhs => @@ -395,7 +419,7 @@ theorem hasStrongType_maximalFunction calc _ ≤ (CMB A (p₂ / p₁) * eLpNorm (fun y ↦ ‖v y‖ ^ (p₁ : ℝ)) (p₂ / p₁) μ) ^ p₁.toReal⁻¹ := by apply ENNReal.rpow_le_rpow _ (by positivity) - convert (hasStrongType_MB h𝓑 (μ := μ) _ (fun x ↦ ‖v x‖ ^ (p₁ : ℝ)) _).2 + convert (hasStrongType_MB h𝓑 hR (μ := μ) _ (fun x ↦ ‖v x‖ ^ (p₁ : ℝ)) _).2 · exact (ENNReal.coe_div p₁n).symm · rwa [lt_div_iff₀, one_mul]; exact cp₁p · rw [ENNReal.coe_div p₁n]; exact Memℒp.norm_rpow_div mlpv p₁ @@ -416,17 +440,17 @@ variable (μ) in @[nolint unusedArguments] def globalMaximalFunction [μ.IsDoubling A] (p : ℝ) (u : X → E) (x : X) : ℝ≥0∞ := A ^ 2 * maximalFunction μ ((covering_separable_space X).choose ×ˢ (univ : Set ℤ)) - (·.1) (2 ^ ·.2) p u x + (·.1) (fun x ↦ 2 ^ (x.2)) p u x -- prove only if needed. Use `MB_le_eLpNormEssSup` -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 - sorry +-- 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 +-- sorry protected theorem MeasureTheory.AEStronglyMeasurable.globalMaximalFunction [BorelSpace X] {p : ℝ} {u : X → E} : AEStronglyMeasurable (globalMaximalFunction μ p u) μ := - AEStronglyMeasurable.maximalFunction (countable_globalMaximalFunction X) + AEStronglyMeasurable.maximalFunction countable_globalMaximalFunction |>.aemeasurable.const_mul _ |>.aestronglyMeasurable /-- Equation (2.0.45).-/ @@ -436,7 +460,7 @@ theorem laverage_le_globalMaximalFunction [IsFiniteMeasureOnCompacts μ] [μ.IsO rw [globalMaximalFunction, maximalFunction] simp only [gt_iff_lt, mem_prod, mem_univ, and_true, ENNReal.rpow_one, inv_one] have hr : 0 < r := lt_of_le_of_lt dist_nonneg h - obtain ⟨c, hc, m, h_subset, _, h_subset'⟩ := exists_ball_subset_ball_two _ z hr + obtain ⟨c, hc, m, h_subset, _, h_subset'⟩ := exists_ball_subset_ball_two z hr calc _ ≤ (μ (ball z r))⁻¹ * ∫⁻ y in ball c (2 ^ m), ‖u y‖₊ ∂μ := by simp only [laverage, MeasurableSet.univ, Measure.restrict_apply, univ_inter, @@ -466,13 +490,14 @@ theorem hasStrongType_globalMaximalFunction [BorelSpace X] [IsFiniteMeasureOnCom [Nonempty X] [μ.IsOpenPosMeasure] {p₁ p₂ : ℝ≥0} (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) : HasStrongType (fun (u : X → E) (x : X) ↦ globalMaximalFunction μ p₁ u x |>.toReal) p₂ p₂ μ μ (C2_0_6' A p₁ p₂) := by - -- unfold globalMaximalFunction - -- simp_rw [ENNReal.toReal_mul] - -- apply HasStrongType.const_mul -- this needs to be adapted - -- refine hasStrongType_maximalFunction ?_ hp₁ hp₁₂ - /- `hasStrongType_maximalFunction` currently requires the collection of balls `𝓑` - to be finite, but its generalization to countable collections is already planned (see https://leanprover.zulipchat.com/#narrow/channel/442935-Carleson/topic/Hardy-Littlewood.20maximal.20principle.20for.20countable.20many.20balls/near/478069896). - -/ + unfold globalMaximalFunction + simp_rw [ENNReal.toReal_mul, C2_0_6'] + convert HasStrongType.const_mul _ _ + · simp + refine hasStrongType_maximalFunction (R := 1) countable_globalMaximalFunction ?_ hp₁ hp₁₂ + -- We need to get rid of this assumption, or fix the proof elsewhere + rintro ⟨_, i⟩ - + simp [inv_le_comm₀, one_le_pow₀ (one_le_two (α := ℝ))] sorry diff --git a/Carleson/RealInterpolation.lean b/Carleson/RealInterpolation.lean index ba8a3b68..3c39aec6 100644 --- a/Carleson/RealInterpolation.lean +++ b/Carleson/RealInterpolation.lean @@ -1045,7 +1045,6 @@ variable {α α' E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : Measur [MeasurableSpace E] [BorelSpace E] [MeasurableSpace E₃] [BorelSpace E₃] {f : α → E₁} {t : ℝ} - {T : (α → E₁) → (α' → E₂)} /-! ## Results about the particular choice of scale @@ -1200,7 +1199,6 @@ variable {α α' E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : Measur {p p' q p₀ q₀ p₁ q₁: ℝ≥0∞} {c : ℝ≥0} {μ : Measure α} {ν : Measure α'} {f : α → E₁} {t : ℝ} - {T : (α → E₁) → (α' → E₂)} /-! ## Some tools for measure theory computations A collection of small lemmas to help with integral manipulations. @@ -1337,7 +1335,6 @@ variable {α α' E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : Measur {p p' q p₀ q₀ p₁ q₁: ℝ≥0∞} {c : ℝ≥0} {a : ℝ} {μ : Measure α} {ν : Measure α'} {f : α → E₁} {t : ℝ} - {T : (α → E₁) → (α' → E₂)} /-! ## Results about truncations of a function -/ @@ -1795,7 +1792,6 @@ variable {α α' E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : Measur [NormedAddCommGroup E₂] [MeasurableSpace E] [BorelSpace E] {f : α → E₁} {t : ℝ} - {T : (α → E₁) → (α' → E₂)} /-! ## Some results about the integrals of truncations @@ -2026,12 +2022,11 @@ noncomputable section open NNReal ENNReal MeasureTheory Set ComputationsInterpolatedExponents ComputationsChoiceExponent -variable {α α' E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : MeasurableSpace α'} +variable {α α' ε E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {p p' q p₀ q₀ p₁ q₁: ℝ≥0∞} {C₀ C₁ : ℝ≥0} {μ : Measure α} {ν : Measure α'} {a : ℝ} {f : α → E₁} {t : ℝ} - {T : (α → E₁) → (α' → E₂)} /-! ## Minkowski's integral inequality -/ namespace MeasureTheory @@ -2765,12 +2760,15 @@ lemma wnorm_eq_zero_iff {f : α → E₁} {p : ℝ≥0∞} [NormedAddCommGroup E /-! ## Weaktype estimates applied to truncations -/ -lemma eLpNorm_trnc_est {f : α → E₁} {j : Bool} {a : ℝ} [NormedAddCommGroup E₁] : +variable [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] + +lemma eLpNorm_trnc_est {f : α → E₁} {j : Bool} {a : ℝ} : eLpNorm (trnc j f a) p μ ≤ eLpNorm f p μ := eLpNorm_mono fun _x ↦ trnc_le_func +variable [ContinuousENorm ε] {T : (α → E₁) → (α' → ε)} in -- TODO: remove the subindex 0 here lemma weaktype_estimate {C₀ : ℝ≥0} {p : ℝ≥0∞} {q : ℝ≥0∞} {f : α → E₁} - [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (hq : 0 < q) (hq' : q < ⊤) (hf : Memℒp f p μ) + (hq : 0 < q) (hq' : q < ⊤) (hf : Memℒp f p μ) (h₀T : HasWeakType T p q μ ν C₀) {t : ℝ} (ht : t > 0) : distribution (T f) (ENNReal.ofReal t) ν ≤ C₀ ^ q.toReal * eLpNorm f p μ ^ q.toReal * ENNReal.ofReal (t ^ (-q.toReal)) := by @@ -2790,8 +2788,8 @@ lemma weaktype_estimate {C₀ : ℝ≥0} {p : ℝ≥0∞} {q : ℝ≥0∞} {f : Real.rpow_rpow_inv] <;> try positivity rwa [← coe_coe_eq_ofReal] +variable [ContinuousENorm ε] {T : (α → E₁) → (α' → ε)} in lemma weaktype_estimate_top {C : ℝ≥0} {p : ℝ≥0∞} {q : ℝ≥0∞} - [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (hq' : q = ⊤) {f : α → E₁} (hf : Memℒp f p μ) (hT : HasWeakType T p q μ ν C) {t : ℝ} (ht : C * eLpNorm f p μ ≤ ENNReal.ofReal t) : distribution (T f) (ENNReal.ofReal t) ν = 0 := by @@ -2801,12 +2799,16 @@ lemma weaktype_estimate_top {C : ℝ≥0} {p : ℝ≥0∞} {q : ℝ≥0∞} apply nonpos_iff_eq_zero.mp calc _ ≤ distribution (T f) (eLpNormEssSup (T f) ν) ν := distribution_mono_right (le_trans wt_est ht) - _ = _ := meas_eLpNormEssSup_lt + _ = _ := meas_essSup_lt -- meas_eLpNormEssSup_lt + +-- for the remaining lemmas we use too much measure theory that is just for normed spaces +-- try to generalize to ENorm-classes after Mathlib refactor +variable {T : (α → E₁) → (α' → E₂)} /-- If `T` has weaktype `p₀`-`p₁`, `f` is `AEStronglyMeasurable` and the `p`-norm of `f` vanishes, then the `q`-norm of `T f` vanishes. -/ -lemma weaktype_aux₀ {p₀ q₀ p q : ℝ≥0∞} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] +lemma weaktype_aux₀ {p₀ q₀ p q : ℝ≥0∞} (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp : p > 0) (hq : q > 0) {C₀ : ℝ≥0} (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (hf : AEStronglyMeasurable f μ) @@ -2821,8 +2823,9 @@ lemma weaktype_aux₀ {p₀ q₀ p q : ℝ≥0∞} [NormedAddCommGroup E₁] [No have : (T f) =ᵐ[ν] 0 := (wnorm_eq_zero_iff hq₀.ne').mp wnorm_0 exact (eLpNorm_eq_zero_iff (h₀T _ hf₁).1 hq.ne').mpr this +variable [MeasurableSpace E₁] [BorelSpace E₁] + lemma weaktype_estimate_trunc_compl {C₀ : ℝ≥0} {p p₀: ℝ≥0∞} {f : α → E₁} - [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp₀ : 0 < p₀) {q₀ : ℝ≥0∞} (hp : p ≠ ⊤) (hq₀ : 0 < q₀) (hq₀' : q₀ < ⊤) (hp₀p : p₀ < p) (hf : Memℒp f p μ) (h₀T : HasWeakType T p₀ q₀ μ ν C₀) {t : ℝ} (ht : t > 0) {a : ℝ} (ha : a > 0) : @@ -2832,7 +2835,6 @@ lemma weaktype_estimate_trunc_compl {C₀ : ℝ≥0} {p p₀: ℝ≥0∞} {f : exact trunc_compl_Lp_Lq_lower hp ⟨hp₀, hp₀p⟩ ha hf lemma weaktype_estimate_trunc {C₁ : ℝ≥0} {p p₁ q₁: ℝ≥0∞} {f : α → E₁} - [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp : 0 < p) (hq₁ : 0 < q₁) (hq₁' : q₁ < ⊤) (hp₁p : p < p₁) (hf : Memℒp f p μ) @@ -2842,7 +2844,6 @@ lemma weaktype_estimate_trunc {C₁ : ℝ≥0} {p p₁ q₁: ℝ≥0∞} {f : α weaktype_estimate hq₁ hq₁' (trunc_Lp_Lq_higher (p := p) ⟨hp, hp₁p⟩ hf) h₁T ht lemma weaktype_estimate_trunc_top_top {a : ℝ} {C₁ : ℝ≥0} - [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hC₁ : C₁ > 0) {p p₁ q₁ : ℝ≥0∞} (hp : 0 < p) (hp₁ : p₁ = ⊤) (hq₁ : q₁ = ⊤) (hp₁p : p < p₁) {f : α → E₁} (hf : Memℒp f p μ) (h₁T : HasWeakType T p₁ q₁ μ ν C₁) {t : ℝ} (ht : t > 0) (ha : a = t / C₁) : @@ -2871,7 +2872,6 @@ lemma weaktype_estimate_trunc_top_top {a : ℝ} {C₁ : ℝ≥0} _ = 0 := distribution_snormEssSup lemma weaktype_estimate_trunc_compl_top {C₀ : ℝ≥0} (hC₀ : C₀ > 0) {p p₀ q₀ : ℝ≥0∞} - [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp₀ : 0 < p₀) (hq₀ : q₀ = ⊤) (hp₀p : p₀ < p) (hp : p ≠ ⊤) {f : α → E₁} (hf : Memℒp f p μ) (h₀T : HasWeakType T p₀ q₀ μ ν C₀) {t : ℝ} (ht : t > 0) {a : ℝ} {d : ℝ} -- (hd : d > 0) (ha : a = (t / d) ^ (p₀.toReal / (p₀.toReal - p.toReal))) @@ -2934,9 +2934,8 @@ lemma weaktype_estimate_trunc_compl_top {C₀ : ℝ≥0} (hC₀ : C₀ > 0) {p p distribution_mono_right snorm_est _ = _ := meas_eLpNormEssSup_lt -lemma weaktype_estimate_trunc_top {C₁ : ℝ≥0} (hC₁ : C₁ > 0) {p p₁ q₁ : ℝ≥0∞} [MeasurableSpace E₁] - [NormedAddCommGroup E₁] - [BorelSpace E₁] [NormedAddCommGroup E₂] (hp : 0 < p) +lemma weaktype_estimate_trunc_top {C₁ : ℝ≥0} (hC₁ : C₁ > 0) {p p₁ q₁ : ℝ≥0∞} + (hp : 0 < p) (hp₁ : p₁ < ⊤) (hq₁ : q₁ = ⊤) (hp₁p : p < p₁) {f : α → E₁} (hf : Memℒp f p μ) (h₁T : HasWeakType T p₁ q₁ μ ν C₁) {t : ℝ} (ht : t > 0) {a : ℝ} {d : ℝ} -- (hd : d > 0) (ha : a = (t / d) ^ (p₁.toReal / (p₁.toReal - p.toReal))) @@ -3007,9 +3006,9 @@ end noncomputable section -open NNReal ENNReal MeasureTheory Set +open NNReal ENNReal MeasureTheory Set Pointwise -variable {α α' E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : MeasurableSpace α'} +variable {α α' ε E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {p p' q p₀ q₀ p₁ q₁: ℝ≥0∞} {C₀ C₁ : ℝ≥0} {μ : Measure α} {ν : Measure α'} {a : ℝ}-- truncation parameter @@ -3024,142 +3023,197 @@ namespace MeasureTheory -- ## Definitions-/ -def Subadditive (T : (α → E₁) → α' → E₂) : Prop := - ∃ A > 0, ∀ (f g : α → E₁) (x : α'), ‖T (f + g) x‖ ≤ A * (‖T f x‖ + ‖T g x‖) +def Subadditive [ENorm ε] (T : (α → E₁) → α' → ε) : Prop := + ∃ A ≠ ⊤, ∀ (f g : α → E₁) (x : α'), ‖T (f + g) x‖ₑ ≤ A * (‖T f x‖ₑ + ‖T g x‖ₑ) --- TODO: put `A` in ℝ≥0∞? -def Subadditive_trunc (T : (α → E₁) → α' → E₂) (A : ℝ) (f : α → E₁) (ν : Measure α') : Prop := +def Subadditive_trunc [ENorm ε] (T : (α → E₁) → α' → ε) (A : ℝ≥0∞) (f : α → E₁) (ν : Measure α') : + Prop := ∀ a : ℝ, a > 0 → ∀ᵐ y ∂ν, - ‖T (trunc f a + trunc_compl f a) y‖ ≤ A * (‖T (trunc f a) y‖ + ‖T (trunc_compl f a) y‖) + ‖T (trunc f a + trunc_compl f a) y‖ₑ ≤ A * (‖T (trunc f a) y‖ₑ + ‖T (trunc_compl f a) y‖ₑ) -/-- The operator is subadditive on functions satisfying `P` with constant `A`. -/ -def AESubAdditiveOn (T : (α → E₁) → α' → E₂) (P : (α → E₁) → Prop) (A : ℝ) (ν : Measure α') : Prop := - ∀ (f g : α → E₁), P f → P g → ∀ᵐ x ∂ν, ‖T (f + g) x‖ ≤ A * (‖T f x‖ + ‖T g x‖) +/-- The operator is subadditive on functions satisfying `P` with constant `A` +(this is almost vacuous if `A = ⊤`). -/ +def AESubadditiveOn [ENorm ε] (T : (α → E₁) → α' → ε) (P : (α → E₁) → Prop) (A : ℝ≥0∞) + (ν : Measure α') : Prop := + ∀ (f g : α → E₁), P f → P g → ∀ᵐ x ∂ν, ‖T (f + g) x‖ₑ ≤ A * (‖T f x‖ₑ + ‖T g x‖ₑ) -namespace AESubAdditiveOn +namespace AESubadditiveOn -variable {ν : Measure α'} +variable [ENormedAddMonoid ε] {ν : Measure α'} -lemma antitone {T : (α → E₁) → α' → E₂} {P P' : (α → E₁) → Prop} - (h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ} (sa : AESubAdditiveOn T P' A ν) : AESubAdditiveOn T P A ν := +lemma antitone {T : (α → E₁) → α' → ε} {P P' : (α → E₁) → Prop} + (h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ≥0∞} (sa : AESubadditiveOn T P' A ν) : + AESubadditiveOn T P A ν := fun f g hf hg ↦ sa f g (h hf) (h hg) -lemma neg (P : (α → E₁) → Prop) {A : ℝ} (hA : A < 0) (h : AESubAdditiveOn T P A ν) - (f : α → E₁) (hf : P f) : T f =ᵐ[ν] 0 := by - filter_upwards [h f f hf hf] with x hx using norm_le_zero_iff.mp - (by nlinarith [norm_nonneg (T (f + f) x), hx]) - lemma zero {P : (α → E₁) → Prop} (hP : ∀ {f g : α → E₁}, P f → P g → P (f + g)) - (A : ℝ) (h : ∀ u, P u → T u =ᵐ[ν] 0) : AESubAdditiveOn T P A ν := by + (A : ℝ≥0∞) (h : ∀ u, P u → T u =ᵐ[ν] 0) : AESubadditiveOn T P A ν := by intro f g hf hg filter_upwards [h f hf, h g hg, h (f + g) (hP hf hg)] with x hx1 hx2 hx3 simp [hx1, hx2, hx3] -lemma biSup {ι : Type*} (𝓑 : Set ι) (h𝓑 : 𝓑.Countable) {T : ι → (α → E₁) → α' → ℝ≥0∞} +lemma forall_le {ι : Type*} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) {T : ι → (α → E₁) → α' → ε} + {P : (α → E₁) → Prop} {A : ℝ≥0∞} + (h : ∀ i ∈ 𝓑, AESubadditiveOn (T i) P A ν) + {f g : α → E₁} (hf : P f) (hg : P g) : + ∀ᵐ x ∂ν, ∀ i ∈ 𝓑, ‖T i (f + g) x‖ₑ ≤ A * (‖T i f x‖ₑ + ‖T i g x‖ₑ) := + eventually_countable_ball h𝓑 |>.mpr fun i hi ↦ h i hi f g hf hg + +lemma biSup {ι : Type*} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) {T : ι → (α → E₁) → α' → ℝ≥0∞} {P : (α → E₁) → Prop} (hT : ∀ (u : α → E₁), P u → ∀ᵐ x ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ∞) (hP : ∀ {f g : α → E₁}, P f → P g → P (f + g)) - (A : ℝ) (h : ∀ i ∈ 𝓑, AESubAdditiveOn (fun u x ↦ (T i u x).toReal) P A ν) : - AESubAdditiveOn (fun u x ↦ (⨆ i ∈ 𝓑, T i u x).toReal) P A ν := by + {A : ℝ≥0∞} (h : ∀ i ∈ 𝓑, AESubadditiveOn (T i) P A ν) : + AESubadditiveOn (fun u x ↦ ⨆ i ∈ 𝓑, T i u x) P A ν := by have hT' : ∀ i ∈ 𝓑, ∀ (u : α → E₁), P u → ∀ᵐ x ∂ν, T i u x ≠ ∞ := by intro i hi f hf filter_upwards [hT f hf] with x hx rw [ne_eq, eq_top_iff] at hx ⊢ exact fun h ↦ hx <| h.trans (le_biSup (fun i ↦ T i f x) hi) - rcases lt_or_le A 0 with A0 | A0 - · refine AESubAdditiveOn.zero hP A (fun f hf ↦ ?_) - have h (i : ι) (hi : i ∈ 𝓑) := (h i hi).neg _ A0 - simp_rw [Set.forall_in_swap, imp.swap, ← imp_forall_iff] at h hT' - filter_upwards [(ae_ball_iff h𝓑).mpr (h f hf), (ae_ball_iff h𝓑).mpr (hT' f hf)] with x hx hx' - simp only [Pi.zero_apply, toReal_eq_zero_iff, ENNReal.iSup_eq_zero] - refine Or.inl fun i hi ↦ ?_ - have := (ENNReal.toReal_eq_zero_iff _).mp (hx i hi) - tauto + -- rcases lt_or_le A 0 with A0 | A0 + -- · refine AESubadditiveOn.zero hP A (fun f hf ↦ ?_) + -- have h (i : ι) (hi : i ∈ 𝓑) := (h i hi).neg _ A0 + -- simp_rw [Set.forall_in_swap, imp.swap, ← imp_forall_iff] at h hT' + -- filter_upwards [(ae_ball_iff h𝓑).mpr (h f hf), (ae_ball_iff h𝓑).mpr (hT' f hf)] with x hx hx' + -- simp only [Pi.zero_apply, toReal_eq_zero_iff, ENNReal.iSup_eq_zero] + -- refine Or.inl fun i hi ↦ ?_ + -- have := (ENNReal.toReal_eq_zero_iff _).mp (hx i hi) + -- tauto intro f g hf hg - simp_rw [AESubAdditiveOn, Set.forall_in_swap, imp.swap, ← imp_forall_iff] at h hT' + simp_rw [AESubadditiveOn, Set.forall_in_swap, imp.swap, ← imp_forall_iff] at h hT' specialize h f hf g hg - simp only [Real.norm_eq_abs, abs_toReal] at h ⊢ + simp_rw [enorm_eq_self] at h ⊢ filter_upwards [hT f hf, hT g hg, (ae_ball_iff h𝓑).mpr h, (ae_ball_iff h𝓑).mpr (hT' f hf), (ae_ball_iff h𝓑).mpr (hT' g hg), (ae_ball_iff h𝓑).mpr (hT' (f + g) (hP hf hg))] with x hTfx hTgx hx hT'fx hT'gx hT'fgx - rw [← toReal_add hTfx hTgx, ← toReal_ofReal A0, ← toReal_mul] - apply toReal_mono <| mul_ne_top ofReal_ne_top (add_ne_top.mpr ⟨hTfx, hTgx⟩) - simp only [iSup_le_iff] + -- rw [← toReal_add hTfx hTgx, ← toReal_ofReal A0, ← toReal_mul] + -- apply toReal_mono <| mul_ne_top ofReal_ne_top (add_ne_top.mpr ⟨hTfx, hTgx⟩) + simp_rw [iSup_le_iff] intro i hi specialize hx i hi - rw [← toReal_add (hT'fx i hi) (hT'gx i hi), ← toReal_ofReal A0, ← toReal_mul, - toReal_le_toReal (hT'fgx i hi) <| mul_ne_top ofReal_ne_top <| - add_ne_top.mpr ⟨hT'fx i hi, hT'gx i hi⟩] at hx + -- rw [← toReal_add (hT'fx i hi) (hT'gx i hi), ← toReal_ofReal A0, ← toReal_mul, + -- toReal_le_toReal (hT'fgx i hi) <| mul_ne_top ofReal_ne_top <| + -- add_ne_top.mpr ⟨hT'fx i hi, hT'gx i hi⟩] at hx apply hx.trans gcongr <;> apply le_biSup _ hi -lemma indicator {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ} - (sa : AESubAdditiveOn T P A ν) (S : Set α') : - AESubAdditiveOn (fun u x ↦ (S.indicator (fun y ↦ T u y) x)) P A ν := by +lemma indicator {T : (α → E₁) → α' → ε} {P : (α → E₁) → Prop} {A : ℝ≥0∞} + (sa : AESubadditiveOn T P A ν) (S : Set α') : + AESubadditiveOn (fun u x ↦ (S.indicator (fun y ↦ T u y) x)) P A ν := by intro f g hf hg filter_upwards [sa f g hf hg] with x hx by_cases h : x ∈ S <;> simp [hx, h] -- If `T` is constant in the second argument (but not necessarily the first) and satisfies --- a subadditivity criterion, then `AESubAdditiveOn T P 1` -lemma const (T : (α → E₁) → E₂) (P : (α → E₁) → Prop) - (h_add : ∀ {f g}, P f → P g → ‖T (f + g)‖ ≤ ‖T f‖ + ‖T g‖) : - AESubAdditiveOn (fun u (_ : α') ↦ T u) P 1 ν := +-- a subadditivity criterion, then `AESubadditiveOn T P 1` +lemma const (T : (α → E₁) → ε) (P : (α → E₁) → Prop) + (h_add : ∀ {f g}, P f → P g → ‖T (f + g)‖ₑ ≤ ‖T f‖ₑ + ‖T g‖ₑ) : + AESubadditiveOn (fun u (_ : α') ↦ T u) P 1 ν := fun f g hf hg ↦ ae_of_all _ fun _ ↦ (by simpa using h_add hf hg) -end AESubAdditiveOn +end AESubadditiveOn -variable [NormedSpace ℝ E₁] [NormedSpace ℝ E₂] +variable [NormedSpace ℝ E₁] [NormedSpace ℝ E₂] [ENormedSpace ε] /-- The operator is sublinear on functions satisfying `P` with constant `A`. -/ -def AESublinearOn (T : (α → E₁) → α' → E₂) (P : (α → E₁) → Prop) (A : ℝ) (ν : Measure α') : Prop := - AESubAdditiveOn T P A ν ∧ ∀ (f : α → E₁) (c : ℝ), P f → c ≥ 0 → T (c • f) =ᵐ[ν] c • T f +def AESublinearOn (T : (α → E₁) → α' → ε) (P : (α → E₁) → Prop) (A : ℝ≥0∞) (ν : Measure α') : + Prop := + AESubadditiveOn T P A ν ∧ ∀ (f : α → E₁) (c : ℝ≥0), P f → T (c • f) =ᵐ[ν] c • T f namespace AESublinearOn variable {ν : Measure α'} -lemma antitone {T : (α → E₁) → α' → E₂} {P P' : (α → E₁) → Prop} - (h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ} (sl : AESublinearOn T P' A ν) : AESublinearOn T P A ν := - ⟨sl.1.antitone (fun hu ↦ h hu), fun u c hu hc ↦ sl.2 u c (h hu) hc⟩ +lemma antitone {T : (α → E₁) → α' → ε} {P P' : (α → E₁) → Prop} + (h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ≥0∞} (sl : AESublinearOn T P' A ν) : + AESublinearOn T P A ν := + ⟨sl.1.antitone (fun hu ↦ h hu), fun u c hu ↦ sl.2 u c (h hu)⟩ -lemma biSup {ι : Type*} (𝓑 : Set ι) (h𝓑 : 𝓑.Countable) (T : ι → (α → E₁) → α' → ℝ≥0∞) +lemma biSup {ι : Type*} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) {T : ι → (α → E₁) → α' → ℝ≥0∞} {P : (α → E₁) → Prop} (hT : ∀ (u : α → E₁), P u → ∀ᵐ x ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ∞) (h_add : ∀ {f g : α → E₁}, P f → P g → P (f + g)) - (h_smul : ∀ {f : α → E₁} {c : ℝ}, P f → c ≥ 0 → P (c • f)) - {A : ℝ} (h : ∀ i ∈ 𝓑, AESublinearOn (fun u x ↦ (T i u x).toReal) P A ν) : - AESublinearOn (fun u x ↦ (⨆ i ∈ 𝓑, T i u x).toReal) P A ν := by + (h_smul : ∀ {f : α → E₁} {c : ℝ≥0}, P f → P (c • f)) + {A : ℝ≥0∞} (h : ∀ i ∈ 𝓑, AESublinearOn (T i) P A ν) : + AESublinearOn (fun u x ↦ ⨆ i ∈ 𝓑, T i u x) P A ν := by have hT' : ∀ i ∈ 𝓑, ∀ (u : α → E₁), P u → ∀ᵐ x ∂ν, T i u x ≠ ∞ := by intro i hi f hf filter_upwards [hT f hf] with x hx rw [ne_eq, eq_top_iff] at hx ⊢ exact fun h ↦ hx <| h.trans (le_biSup (fun i ↦ T i f x) hi) - refine ⟨AESubAdditiveOn.biSup 𝓑 h𝓑 hT h_add A (fun i hi ↦ (h i hi).1), fun f c hf hc ↦ ?_⟩ + refine ⟨AESubadditiveOn.biSup h𝓑 hT h_add (fun i hi ↦ (h i hi).1), fun f c hf ↦ ?_⟩ simp_rw [Set.forall_in_swap, imp.swap, ← imp_forall_iff] at hT' - filter_upwards [(ae_ball_iff h𝓑).mpr (fun i hi ↦ (h i hi).2 f c hf hc), - (ae_ball_iff h𝓑).mpr (hT' f hf), (ae_ball_iff h𝓑).mpr (hT' (c • f) (h_smul hf hc))] with x hx hT'fx hT'cfx - rw [Pi.smul_apply, ← ENNReal.toReal_ofReal hc, smul_eq_mul] - simp only [← toReal_mul, ENNReal.mul_iSup] - congr 1 + filter_upwards [(ae_ball_iff h𝓑).mpr (fun i hi ↦ (h i hi).2 f c hf), + (ae_ball_iff h𝓑).mpr (hT' f hf), (ae_ball_iff h𝓑).mpr (hT' (c • f) (h_smul hf))] with x hx hT'fx hT'cfx + simp_rw [Pi.smul_apply, ENNReal.smul_iSup] refine biSup_congr (fun i hi ↦ ?_) specialize hx i hi - simp only [Pi.smul_apply, smul_eq_mul, ← toReal_ofReal_mul c (T i f x) hc] at hx - simp_rw [ENNReal.toReal_eq_toReal (hT'cfx i hi) (mul_ne_top ofReal_ne_top (hT'fx i hi))] at hx - rwa [toReal_ofReal hc] - -lemma indicator {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ} (S : Set α') + simpa only [Pi.smul_apply, smul_eq_mul] using hx + +lemma biSup2 {ι : Type*} {𝓑 : Set ι} (h𝓑 : 𝓑.Countable) {T : ι → (α → E₁) → α' → ℝ≥0∞} + {P : (α → E₁) → Prop} {Q : (α → E₁) → Prop} + (hPT : ∀ (u : α → E₁), P u → ∀ᵐ x ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ∞) + (hQT : ∀ (u : α → E₁), Q u → ∀ᵐ x ∂ν, ⨆ i ∈ 𝓑, T i u x ≠ ∞) + (P0 : P 0) + (Q0 : Q 0) + (haP : ∀ {f g : α → E₁}, P f → P g → P (f + g)) + (haQ : ∀ {f g : α → E₁}, Q f → Q g → Q (f + g)) + (hsP : ∀ {f : α → E₁} {c : ℝ≥0}, P f → P (c • f)) + (hsQ : ∀ {f : α → E₁} {c : ℝ≥0}, Q f → Q (c • f)) + {A : ℝ≥0} -- todo, here and elsewhere: probably better to have {A : ℝ≥0∞} (hA : A ≠ ⊤) + (hAP : ∀ i ∈ 𝓑, + AESublinearOn (T i) (fun g ↦ g ∈ {f | P f} + {f | Q f}) A ν) : + AESublinearOn (fun u x ↦ ⨆ i ∈ 𝓑, T i u x) (fun f ↦ P f ∨ Q f) A ν := by + set R := fun g ↦ g ∈ {f | P f} + {f | Q f} + have hPR : ∀ {f}, P f → R f := fun hu ↦ ⟨_, hu, 0, Q0, by simp⟩ + have hQR : ∀ {f}, Q f → R f := fun hu ↦ ⟨0, P0, _, hu, by simp⟩ + apply AESublinearOn.antitone (P' := R) (fun hu ↦ hu.elim hPR hQR) + refine AESublinearOn.biSup (P := R) h𝓑 ?_ ?_ ?_ hAP + · rintro _ ⟨f, hf, g, hg, rfl⟩ + filter_upwards [hPT f hf, hQT g hg, + AESubadditiveOn.forall_le h𝓑 (fun i hi ↦ hAP i hi |>.1) (hPR hf) (hQR hg)] with x hfx hgx hTx + simp_rw [← lt_top_iff_ne_top] at hfx hgx ⊢ + simp_rw [enorm_eq_self] at hTx + calc + _ ≤ ⨆ i ∈ 𝓑, A * (T i f x + T i g x) := by gcongr; exact hTx _ ‹_› + _ ≤ A * ((⨆ i ∈ 𝓑, T i f x) + (⨆ i ∈ 𝓑, T i g x)) := by + simp_rw [← ENNReal.mul_iSup] + gcongr + -- todo: make lemma + simp_rw [iSup_le_iff] + intro i hi + gcongr <;> apply le_biSup _ hi + _ < ⊤ := mul_lt_top coe_lt_top <| add_lt_top.mpr ⟨hfx, hgx⟩ + · rintro _ _ ⟨f₁, hf₁, g₁, hg₁, rfl⟩ ⟨f₂, hf₂, g₂, hg₂, rfl⟩ + exact ⟨f₁ + f₂, haP hf₁ hf₂, g₁ + g₂, haQ hg₁ hg₂, by abel_nf⟩ + · rintro _ c ⟨f, hf, g, hg, rfl⟩ + exact ⟨c • f, hsP hf, c • g, hsQ hg, by module⟩ + +lemma indicator {T : (α → E₁) → α' → ε} {P : (α → E₁) → Prop} {A : ℝ≥0∞} (S : Set α') (sl : AESublinearOn T P A ν) : AESublinearOn (fun u x ↦ (S.indicator (fun y ↦ T u y) x)) P A ν := by - refine ⟨AESubAdditiveOn.indicator sl.1 S, fun f c hf hc ↦ ?_⟩ - filter_upwards [sl.2 f c hf hc] with x hx + refine ⟨AESubadditiveOn.indicator sl.1 S, fun f c hf ↦ ?_⟩ + filter_upwards [sl.2 f c hf] with x hx by_cases h : x ∈ S <;> simp [h, hx] -- If `T` is constant in the second argument (but not necessarily the first) and satisfies -- certain requirements, then `AESublinearOn T P 1` -lemma const (T : (α → E₁) → E₂) (P : (α → E₁) → Prop) - (h_add : ∀ {f g}, P f → P g → ‖T (f + g)‖ ≤ ‖T f‖ + ‖T g‖) - (h_smul : ∀ f {c : ℝ}, P f → c ≥ 0 → T (c • f) = c • T f) : +lemma const (T : (α → E₁) → ε) (P : (α → E₁) → Prop) + (h_add : ∀ {f g}, P f → P g → ‖T (f + g)‖ₑ ≤ ‖T f‖ₑ + ‖T g‖ₑ) + (h_smul : ∀ f {c : ℝ≥0}, P f → T (c • f) = c • T f) : AESublinearOn (fun u (_ : α') ↦ T u) P 1 ν := by - refine ⟨AESubAdditiveOn.const T P h_add, fun f c hf hc ↦ ae_of_all _ fun _ ↦ ?_⟩ - simpa using h_smul f hf hc + refine ⟨AESubadditiveOn.const T P h_add, fun f c hf ↦ ae_of_all _ fun _ ↦ ?_⟩ + simpa using h_smul f hf + +-- glue that we can probably remove +lemma toReal {T : (α → E₁) → α' → ℝ≥0∞} + {P : (α → E₁) → Prop} + {A : ℝ≥0∞} (h : AESublinearOn T P A ν) + (hP : ∀ (u : α → E₁), P u → ∀ᵐ x ∂ν, T u x ≠ ∞) : + AESublinearOn (T · · |>.toReal) P A ν := by + refine ⟨fun f g hf hg ↦ ?_, fun f c hf ↦ ?_⟩ + · filter_upwards [h.1 f g hf hg, hP f hf, hP g hg] with x hx hfx hgx + simp only [enorm_eq_self, ne_eq, hfx, not_false_eq_true, enorm_toReal, hgx] at hx ⊢ + exact enorm_toReal_le.trans hx + · filter_upwards [h.2 f c hf, hP f hf] with x hx hfx + simp_rw [hx, Pi.smul_apply, toReal_smul] end AESublinearOn @@ -3194,24 +3248,25 @@ def PreservesAEStrongMeasurability (T : (α → E₁) → α' → E₂) (p : ℝ≥0∞) : Prop := ∀ ⦃f : α → E₁⦄, Memℒp f p μ → AEStronglyMeasurable (T f) ν -lemma estimate_distribution_Subadditive_trunc {f : α → E₁} {t : ℝ} +lemma estimate_distribution_Subadditive_trunc {f : α → E₁} {t : ℝ≥0} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] - (ht : t > 0) {a : ℝ} (ha : a > 0) {A : ℝ} (hA : A ≥ 0) (h : Subadditive_trunc T A f ν) : - distribution (T f) (ENNReal.ofReal (2 * A * t)) ν ≤ - distribution (T (trunc f a)) (ENNReal.ofReal t) ν + - distribution (T (f - trunc f a)) (ENNReal.ofReal t) ν := by + {a : ℝ} (ha : a > 0) {A : ℝ≥0∞} (h : Subadditive_trunc T A f ν) : + distribution (T f) (2 * A * t) ν ≤ + distribution (T (trunc f a)) t ν + + distribution (T (f - trunc f a)) t ν := by nth_rw 2 [mul_comm] - rw [mul_assoc, two_mul, ENNReal.ofReal_mul, ofReal_add] <;> try positivity - apply distribution_add_le' hA + rw [mul_assoc, two_mul] + apply distribution_add_le' nth_rw 1 [trunc_buildup (f := f) (t := a)] exact h a ha lemma rewrite_norm_func {q : ℝ} {g : α' → E} - [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] (hq : 0 < q) {A : ℝ} (hA : A > 0) + [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] (hq : 0 < q) {A : ℝ≥0} (hA : A > 0) (hg : AEMeasurable g ν) : - ∫⁻ x, ‖g x‖₊ ^q ∂ν = - ENNReal.ofReal ((2 * A)^q * q) * ∫⁻ s in Ioi (0 : ℝ), + ∫⁻ x, ‖g x‖₊ ^ q ∂ν = + ENNReal.ofReal ((2 * A) ^ q * q) * ∫⁻ s in Ioi (0 : ℝ), distribution g ((ENNReal.ofReal (2 * A * s))) ν * (ENNReal.ofReal (s^(q - 1))) := by + have : (A : ℝ) > 0 := hA simp only [← enorm_eq_nnnorm] rw [lintegral_norm_pow_eq_distribution hg (by linarith)] nth_rewrite 1 [← lintegral_scale_constant_halfspace' (a := (2*A)) (by linarith)] @@ -3232,7 +3287,7 @@ lemma rewrite_norm_func {q : ℝ} {g : α' → E} lemma estimate_norm_rpow_range_operator {q : ℝ} {f : α → E₁} [NormedAddCommGroup E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] - (hq : 0 < q) (tc : ToneCouple) {A : ℝ} (hA : A > 0) + (hq : 0 < q) (tc : ToneCouple) {A : ℝ≥0} (hA : A > 0) (ht : Subadditive_trunc T A f ν) (hTf : AEMeasurable (T f) ν) : ∫⁻ x : α', ‖T f x‖₊ ^ q ∂ν ≤ ENNReal.ofReal ((2 * A)^q * q) * ∫⁻ s in Ioi (0 : ℝ), distribution (T (trunc f (tc.ton s))) @@ -3244,7 +3299,8 @@ lemma estimate_norm_rpow_range_operator {q : ℝ} {f : α → E₁} intro s s_pos rw [← add_mul] apply mul_le_mul' ?_ (le_refl _) - exact estimate_distribution_Subadditive_trunc s_pos (tc.ran_ton s s_pos) hA.le ht + convert estimate_distribution_Subadditive_trunc (tc.ran_ton s s_pos) ht + simp [ofReal_mul, ENNReal.ofNNReal_toNNReal] -- XXX: can this be golfed or unified with `ton_aeMeasurable`? @[measurability, fun_prop] @@ -3537,7 +3593,7 @@ lemma support_sigma_finite_from_Memℒp -- have : SigmaFinite (μ.restrict (Function.support f)) := support_sigma_finite_from_Memℒp hf hp hp' -- exact instSFiniteOfSigmaFinite -lemma combine_estimates₀ {A : ℝ} (hA : A > 0) +lemma combine_estimates₀ {A : ℝ≥0} (hA : A > 0) [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] {spf : ScaledPowerFunction} @@ -3685,7 +3741,7 @@ lemma combine_estimates₀ {A : ℝ} (hA : A > 0) · simp _ = _ := by ring_nf -lemma combine_estimates₁ {A : ℝ} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] +lemma combine_estimates₁ {A : ℝ≥0} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hA : A > 0) {spf : ScaledPowerFunction} (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (ht : t ∈ Ioo 0 1) @@ -3820,7 +3876,7 @@ lemma exists_hasStrongType_real_interpolation_aux₀ {p₀ p₁ q₀ q₁ p q : exact (eLpNorm_eq_zero_iff (h₂T hf) q_pos.ne').mpr this /-- The estimate for the real interpolation theorem in case `p₀ < p₁`. -/ -lemma exists_hasStrongType_real_interpolation_aux {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} {A : ℝ} +lemma exists_hasStrongType_real_interpolation_aux {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} {A : ℝ≥0} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hA : A > 0) (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁) @@ -4078,7 +4134,7 @@ lemma exists_hasStrongType_real_interpolation_aux₃ {p₀ p₁ q₀ q₁ p q : /-- The main estimate for the real interpolation theorem, before taking roots, combining the cases `p₀ ≠ p₁` and `p₀ = p₁`. -/ -lemma exists_hasStrongType_real_interpolation_aux₄ {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} {A : ℝ} +lemma exists_hasStrongType_real_interpolation_aux₄ {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} {A : ℝ≥0} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hA : A > 0) (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁) @@ -4251,7 +4307,7 @@ lemma Subadditive_trunc_from_SubadditiveOn_Lp₀p₁ {p₀ p₁ p : ℝ≥0∞} (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) {A : ℝ≥0} (ht : t ∈ Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) / p₀ + ENNReal.ofReal t / p₁) - (hT : AESubAdditiveOn T (fun f ↦ Memℒp f p₀ μ ∨ Memℒp f p₁ μ) A ν) + (hT : AESubadditiveOn T (fun f ↦ Memℒp f p₀ μ ∨ Memℒp f p₁ μ) A ν) (hf : Memℒp f p μ) : Subadditive_trunc T A f ν := by refine fun a a_pos ↦ ?_ @@ -4280,7 +4336,7 @@ theorem exists_hasStrongType_real_interpolation {p₀ p₁ q₀ q₁ p q : ℝ {C₀ C₁ t A : ℝ≥0} (hA : A > 0) (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hp : p⁻¹ = (1 - t) / p₀ + t / p₁) (hq : q⁻¹ = (1 - t) / q₀ + t / q₁) (hmT : ∀ f, Memℒp f p μ → AEStronglyMeasurable (T f) ν) - (hT : AESubAdditiveOn T (fun f ↦ Memℒp f p₀ μ ∨ Memℒp f p₁ μ) A ν) + (hT : AESubadditiveOn T (fun f ↦ Memℒp f p₀ μ ∨ Memℒp f p₁ μ) A ν) (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₁T : HasWeakType T p₁ q₁ μ ν C₁) : HasStrongType T p q μ ν (C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t) := by intro f hf diff --git a/Carleson/ToMathlib/ENorm.lean b/Carleson/ToMathlib/ENorm.lean index 1911ba2c..8c078743 100644 --- a/Carleson/ToMathlib/ENorm.lean +++ b/Carleson/ToMathlib/ENorm.lean @@ -1,386 +1,99 @@ -import Mathlib.Analysis.NormedSpace.IndicatorFunction -import Mathlib.MeasureTheory.Function.EssSup -import Mathlib.MeasureTheory.Function.AEEqFun -import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic - --- these imports are only needed in the `tmp` section -import Mathlib.Topology.MetricSpace.Pseudo.Defs -import Mathlib.MeasureTheory.Covering.Vitali +import Mathlib.Analysis.Normed.Group.Basic +import Mathlib.Topology.Instances.ENNReal +import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic noncomputable section -open ENNReal NNReal MeasureTheory Function Set - -/-- An enormed monoid is an additive monoid endowed with an enorm. -/ -class ENormedAddMonoid (E : Type*) extends ENorm E, AddMonoid E, TopologicalSpace E where - enorm_zero : ∀ x : E, enorm x = 0 ↔ x = 0 - enorm_neg : ∀ x y : E, x + y = 0 → ‖x‖ₑ = ‖y‖ₑ -- this is a silly way to write this - enorm_triangle : ∀ x y : E, ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ - -- the topology is somehow defined by the enorm. - -/-- An enormed monoid is an additive monoid endowed with an enorm. -/ -class ENormedAddCommMonoid (E : Type*) extends ENormedAddMonoid E, AddCommMonoid E where - -- the topology is somehow defined by the enorm. +open ENNReal NNReal Function Set variable {α α' E E₁ E₂ F : Type*} [ENorm F] -instance : ENormedAddCommMonoid ℝ≥0∞ where - enorm := id - enorm_zero := by simp - enorm_neg := by simp - enorm_triangle := by simp - add_comm := by simp [add_comm] - -instance [NormedAddGroup E] : ENormedAddMonoid E where - enorm_zero := by simp [enorm_eq_nnnorm] - enorm_neg := by - simp (config := {contextual := true}) [← eq_neg_iff_add_eq_zero, enorm_eq_nnnorm] - enorm_triangle := by simp [enorm_eq_nnnorm, ← ENNReal.coe_add, nnnorm_add_le] - -instance [NormedAddCommGroup E] : ENormedAddCommMonoid E where - add_comm := by simp [add_comm] - -namespace MeasureTheory - -/-- `(∫ ‖f a‖^q ∂μ) ^ (1/q)`, which is a seminorm on the space of measurable functions for which -this quantity is finite -/ -def eLpNorm' {_ : MeasurableSpace α} (f : α → F) (q : ℝ) (μ : Measure α) : ℝ≥0∞ := - (∫⁻ a, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) - -/-- seminorm for `ℒ∞`, equal to the essential supremum of `‖f‖`. -/ -def eLpNormEssSup {_ : MeasurableSpace α} (f : α → F) (μ : Measure α) := - essSup (fun x => ‖f x‖ₑ) μ - -/-- `ℒp` seminorm, equal to `0` for `p=0`, to `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞` and to -`essSup ‖f‖ μ` for `p = ∞`. -/ -def eLpNorm {_ : MeasurableSpace α} - (f : α → F) (p : ℝ≥0∞) (μ : Measure α := by volume_tac) : ℝ≥0∞ := - if p = 0 then 0 else if p = ∞ then eLpNormEssSup f μ else eLpNorm' f (ENNReal.toReal p) μ - -/-- The property that `f : α → E` is a.e. strongly measurable and `(∫ ‖f a‖^p ∂μ)^(1/p)` is finite -if `p < ∞`, or `essSup f < ∞` if `p = ∞`. -/ -def Memℒp [TopologicalSpace E] [ENorm E] {_ : MeasurableSpace α} (f : α → E) (p : ℝ≥0∞) - (μ : Measure α := by volume_tac) : Prop := - AEStronglyMeasurable f μ ∧ eLpNorm f p μ < ∞ - -variable [MeasurableSpace α] [MeasurableSpace α'] - -/-! # The distribution function `d_f` -/ - -/-- The distribution function of a function `f`. -Note that unlike the notes, we also define this for `t = ∞`. -Note: we also want to use this for functions with codomain `ℝ≥0∞`, but for those we just write -`μ { x | t < f x }` -/ -def distribution [ENorm E] (f : α → E) (t : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ := - μ { x | t < ‖f x‖ₑ } - -/-- The weak L^p norm of a function, for `p < ∞` -/ -def wnorm' [ENorm E] (f : α → E) (p : ℝ) (μ : Measure α) : ℝ≥0∞ := - ⨆ t : ℝ≥0, t * distribution f t μ ^ (p : ℝ)⁻¹ - -/-- The weak L^p norm of a function. -/ -def wnorm [ENorm E] (f : α → E) (p : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ := - if p = ∞ then eLpNormEssSup f μ else wnorm' f (ENNReal.toReal p) μ - -lemma wnorm'_zero [ENorm E] (f : α → E) (μ : Measure α) : wnorm' f 0 μ = ∞ := by - simp only [wnorm, zero_ne_top, ↓reduceIte, wnorm', zero_toReal, GroupWithZero.inv_zero, - ENNReal.rpow_zero, mul_one, iSup_eq_top] - refine fun b hb ↦ ⟨b.toNNReal + 1, ?_⟩ - rw [coe_add, ENNReal.coe_one, coe_toNNReal hb.ne_top] - exact lt_add_right hb.ne_top one_ne_zero +lemma ENNReal.ofReal_norm [SeminormedAddGroup E] (x : E) : .ofReal ‖x‖ = ‖x‖ₑ := by + simp_rw [enorm_eq_nnnorm, ofReal_norm_eq_coe_nnnorm] -lemma wnorm_zero [ENorm E] (f : α → E) (μ : Measure α) : wnorm f 0 μ = ∞ := by - simp [wnorm, wnorm'_zero] +lemma enorm_toReal_le {x : ℝ≥0∞} : ‖x.toReal‖ₑ ≤ x := by simp [← ofReal_norm, ofReal_toReal_le] -/-- A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm. -/ -def MemWℒp [TopologicalSpace E] [ENorm E] (f : α → E) (p : ℝ≥0∞) (μ : Measure α) : Prop := - AEStronglyMeasurable f μ ∧ wnorm f p μ < ∞ +@[simp] lemma enorm_toReal {x : ℝ≥0∞} (hx : x ≠ ⊤) : ‖x.toReal‖ₑ = x := by + simp [enorm_eq_nnnorm, hx, ← ofReal_norm_eq_coe_nnnorm] -lemma MemWℒp_zero [TopologicalSpace E] [ENorm E] (f : α → E) (μ : Measure α) : ¬ MemWℒp f 0 μ := by - simp [MemWℒp, wnorm_zero] - -variable [ENorm E₁] [ENorm E₂] [TopologicalSpace E₁] [TopologicalSpace E₂] - -/-- An operator has weak type `(p, q)` if it is bounded as a map from L^p to weak-L^q. -`HasWeakType T p p' μ ν c` means that `T` has weak type `(p, p')` w.r.t. measures `μ`, `ν` -and constant `c`. -/ -def HasWeakType (T : (α → E₁) → (α' → E₂)) (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') - (c : ℝ≥0) : Prop := - ∀ f : α → E₁, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ wnorm (T f) p' ν ≤ c * eLpNorm f p μ - -/-- An operator has strong type `(p, q)` if it is bounded as an operator on `L^p → L^q`. -`HasStrongType T p p' μ ν c` means that `T` has strong type `(p, p')` w.r.t. measures `μ`, `ν` -and constant `c`. -/ -def HasStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] - {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → E) → (α' → E')) - (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0) : Prop := - ∀ f : α → E, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ eLpNorm (T f) p' ν ≤ c * eLpNorm f p μ - -/-- A weaker version of `HasStrongType`. This is the same as `HasStrongType` if `T` is continuous -w.r.t. the L^2 norm, but weaker in general. -/ -def HasBoundedStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] - {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → E) → (α' → E')) - (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0) : Prop := - ∀ f : α → E, Memℒp f p μ → eLpNorm f ∞ μ < ∞ → μ (support f) < ∞ → - AEStronglyMeasurable (T f) ν ∧ eLpNorm (T f) p' ν ≤ c * eLpNorm f p μ - -/-- If a function `f : α → ENNReal` is `MemWℒp`, then its norm is almost everywhere finite.-/ -theorem MemWℒp.ae_ne_top [TopologicalSpace E] [ENorm E] {f : α → E} {p : ℝ≥0∞} {μ : Measure α} - (hf : MemWℒp f p μ) : ∀ᵐ x ∂μ, ‖f x‖ₑ ≠ ∞ := by - by_cases hp_inf : p = ∞ - · rw [hp_inf] at hf - simp_rw [← lt_top_iff_ne_top] - exact ae_lt_of_essSup_lt hf.2 - by_cases hp_zero : p = 0 - · exact (MemWℒp_zero _ _ <| hp_zero ▸ hf).elim - set A := {x | ‖f x‖ₑ = ∞} with hA - unfold MemWℒp wnorm wnorm' at hf - simp only [hp_inf] at hf - rw [Filter.eventually_iff, mem_ae_iff] - simp only [ne_eq, compl_def, mem_setOf_eq, Decidable.not_not, ← hA] - have hp_toReal_zero := toReal_ne_zero.mpr ⟨hp_zero, hp_inf⟩ - have h1 (t : ℝ≥0) : μ A ≤ distribution f t μ := by - refine μ.mono ?_ - simp_all only [setOf_subset_setOf, coe_lt_top, implies_true, A] - set C := ⨆ t : ℝ≥0, t * distribution f t μ ^ p.toReal⁻¹ - by_cases hC_zero : C = 0 - · simp only [ENNReal.iSup_eq_zero, mul_eq_zero, ENNReal.rpow_eq_zero_iff, inv_neg'', C] at hC_zero - specialize hC_zero 1 - simp only [one_ne_zero, ENNReal.coe_one, toReal_nonneg.not_lt, and_false, or_false, - false_or] at hC_zero - exact measure_mono_null (setOf_subset_setOf.mpr fun x hx => hx ▸ one_lt_top) hC_zero.1 - by_contra h - have h2 : C < ∞ := by aesop - have h3 (t : ℝ≥0) : distribution f t μ ≤ (C / t) ^ p.toReal := by - rw [← rpow_inv_rpow hp_toReal_zero (distribution ..)] - refine rpow_le_rpow ?_ toReal_nonneg - rw [ENNReal.le_div_iff_mul_le (Or.inr hC_zero) (Or.inl coe_ne_top), mul_comm] - exact le_iSup_iff.mpr fun _ a ↦ a t - have h4 (t : ℝ≥0) : μ A ≤ (C / t) ^ p.toReal := (h1 t).trans (h3 t) - have h5 : μ A ≤ μ A / 2 := by - convert h4 (C * (2 / μ A) ^ p.toReal⁻¹).toNNReal - rw [coe_toNNReal ?_] - swap - · refine mul_ne_top h2.ne_top (rpow_ne_top_of_nonneg (inv_nonneg.mpr toReal_nonneg) ?_) - simp [div_eq_top, h] - nth_rw 1 [← mul_one C] - rw [ENNReal.mul_div_mul_left _ _ hC_zero h2.ne_top, div_rpow_of_nonneg _ _ toReal_nonneg, - ENNReal.rpow_inv_rpow hp_toReal_zero, ENNReal.one_rpow, one_div, - ENNReal.inv_div (Or.inr two_ne_top) (Or.inr (NeZero.ne' 2).symm)] - have h6 : μ A = 0 := by - convert (fun hh ↦ ENNReal.half_lt_self hh (ne_top_of_le_ne_top (rpow_ne_top_of_nonneg - toReal_nonneg ((div_one C).symm ▸ h2.ne_top)) (h4 1))).mt h5.not_lt - tauto - exact h h6 - --- Maybe this statement is not needed, we can just use the previous one. -/-- If a function `f : α → ENNReal` is `MemWℒp`, then it is almost everywhere finite.-/ -theorem MemWℒp.ae_ne_top' {f : α → ENNReal} {p : ℝ≥0∞} {μ : Measure α} - (hf : MemWℒp f p μ) : ∀ᵐ x ∂μ, f x ≠ ∞ := hf.ae_ne_top - -/- Add temporary section. -/ -section tmp - -/- Copy-pasted all this code here temporarily to be able to prove `HasWeakType.MB_one'` while avoiding the import conflicts, the problem is that this file redefines some objects that are imported in the files that define `IsDoubling`, `MB` ecc. When these definitions will replace the old ones this can be fixed --/ - -open Metric Vitali MeasureTheory Measure - -/-- A doubling measure is a measure on a metric space with the condition doubling -the radius of a ball only increases the volume by a constant factor, independent of the ball. -/ -class Measure.IsDoubling {X : Type*} [MeasurableSpace X] [PseudoMetricSpace X] - (μ : Measure X) (A : outParam ℝ≥0) : Prop where - measure_ball_two_le_same : ∀ (x : X) r, μ (ball x (2 * r)) ≤ A * μ (ball x r) - -variable {X E : Type*} {A : ℝ≥0} [MetricSpace X] [MeasurableSpace X] - {μ : Measure X} [μ.IsDoubling A] [NormedAddCommGroup E] - {f : X → E} {x : X} {ι : Type*} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ} - -section laverage - -variable (μ : Measure α) - -/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. a measure `μ`, denoted `⨍⁻ x, f x ∂μ`. - -It is equal to `(μ univ)⁻¹ * ∫⁻ x, f x ∂μ`, so it takes value zero if `μ` is an infinite measure. If -`μ` is a probability measure, then the average of any function is equal to its integral. - -For the average on a set, use `⨍⁻ x in s, f x ∂μ`, defined as `⨍⁻ x, f x ∂(μ.restrict s)`. For the -average w.r.t. the volume, one can omit `∂volume`. -/ -noncomputable def laverage (f : α → ℝ≥0∞) := ∫⁻ x, f x ∂(μ univ)⁻¹ • μ +/-- A type `E` equipped with a continuous map `‖·‖ₑ : E → ℝ≥0∞`. +Note: do we want to unbundle this (at least separate out `TopologicalSpace E`?) +Note: not sure if this is the "right" class to add to Mathlib. -/ +class ContinuousENorm (E : Type*) extends ENorm E, TopologicalSpace E where + continuous_enorm : Continuous enorm + -- the topology is somehow defined by the enorm. -/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. a measure `μ`. +/-- An enormed monoid is an additive monoid endowed with a continuous enorm. +Note: not sure if this is the "right" class to add to Mathlib. -/ +class ENormedAddMonoid (E : Type*) extends ContinuousENorm E, AddMonoid E where + enorm_eq_zero : ∀ x : E, ‖x‖ₑ = 0 ↔ x = 0 + -- enorm_neg : ∀ x y : E, x + y = 0 → ‖x‖ₑ = ‖y‖ₑ -- this is a silly way to write this + enorm_add_le : ∀ x y : E, ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ -It is equal to `(μ univ)⁻¹ * ∫⁻ x, f x ∂μ`, so it takes value zero if `μ` is an infinite measure. If -`μ` is a probability measure, then the average of any function is equal to its integral. +/-- An enormed monoid is an additive monoid endowed with a continuous enorm. +Note: not sure if this is the "right" class to add to Mathlib. -/ +class ENormedAddCommMonoid (E : Type*) extends ENormedAddMonoid E, AddCommMonoid E where -For the average on a set, use `⨍⁻ x in s, f x ∂μ`, defined as `⨍⁻ x, f x ∂(μ.restrict s)`. For the -average w.r.t. the volume, one can omit `∂volume`. -/ -notation3 "⨍⁻ "(...)", "r:60:(scoped f => f)" ∂"μ:70 => laverage μ r +/-- An enormed space is an additive monoid endowed with a continuous enorm. +Note: not sure if this is the "right" class to add to Mathlib. -/ +class ENormedSpace (E : Type*) extends ENormedAddCommMonoid E, Module ℝ≥0 E where + enorm_smul : ∀ (c : ℝ≥0) (x : E), ‖c • x‖ₑ = c • ‖x‖ₑ -/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. a measure `μ` on a set `s`. +export ENormedAddMonoid (enorm_eq_zero enorm_add_le) +export ENormedSpace (enorm_smul) +attribute [simp] enorm_eq_zero enorm_smul -It is equal to `(μ s)⁻¹ * ∫⁻ x, f x ∂μ`, so it takes value zero if `s` has infinite measure. If `s` -has measure `1`, then the average of any function is equal to its integral. +@[simp] lemma enorm_zero {ε} [ENormedAddMonoid ε] : ‖(0 : ε)‖ₑ = 0 := by simp -For the average w.r.t. the volume, one can omit `∂volume`. -/ -notation3 "⨍⁻ "(...)" in "s", "r:60:(scoped f => f)" ∂"μ:70 => laverage (Measure.restrict μ s) r +instance : ENormedSpace ℝ≥0∞ where + enorm := id + enorm_eq_zero := by simp + -- enorm_neg := by simp + enorm_add_le := by simp + add_comm := by simp [add_comm] + continuous_enorm := continuous_id + enorm_smul := by simp -theorem laverage_eq' (f : α → ℝ≥0∞) : ⨍⁻ x, f x ∂μ = ∫⁻ x, f x ∂(μ univ)⁻¹ • μ := rfl +instance [SeminormedAddGroup E] : ContinuousENorm E where + continuous_enorm := ENNReal.continuous_coe.comp continuous_nnnorm -theorem laverage_eq (f : α → ℝ≥0∞) : ⨍⁻ x, f x ∂μ = (∫⁻ x, f x ∂μ) / μ univ := by - rw [laverage_eq', lintegral_smul_measure, ENNReal.div_eq_inv_mul] +instance [NormedAddGroup E] : ENormedAddMonoid E where + enorm_eq_zero := by simp [enorm_eq_nnnorm] + -- enorm_neg := by + -- simp (config := {contextual := true}) [← eq_neg_iff_add_eq_zero, enorm_eq_nnnorm] + enorm_add_le := by simp [enorm_eq_nnnorm, ← ENNReal.coe_add, nnnorm_add_le] -theorem setLaverage_eq (f : α → ℝ≥0∞) (s : Set α) : - ⨍⁻ x in s, f x ∂μ = (∫⁻ x in s, f x ∂μ) / μ s := by rw [laverage_eq, restrict_apply_univ] +@[simp] lemma enorm_neg [NormedAddGroup E] (x : E) : ‖-x‖ₑ = ‖x‖ₑ := by + simp_rw [enorm_eq_nnnorm, nnnorm_neg] -end laverage +instance [NormedAddCommGroup E] : ENormedAddCommMonoid E where + add_comm := by simp [add_comm] -/-- The Hardy-Littlewood maximal function w.r.t. a collection of balls 𝓑. -M_{𝓑, p} in the blueprint. -/ -def maximalFunction (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) - (p : ℝ) (u : X → E) (x : X) : ℝ≥0∞ := - (⨆ i ∈ 𝓑, (ball (c i) (r i)).indicator (x := x) - fun _ ↦ ⨍⁻ y in ball (c i) (r i), ‖u y‖₊ ^ p ∂μ) ^ p⁻¹ +instance [NormedAddCommGroup E] [NormedSpace ℝ E] : ENormedSpace E where + enorm_smul := by simp_rw [enorm_eq_nnnorm, ENNReal.smul_def, NNReal.smul_def, nnnorm_smul]; simp -/-- The Hardy-Littlewood maximal function w.r.t. a collection of balls 𝓑 with exponent 1. -M_𝓑 in the blueprint. -/ -abbrev MB (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) : ℝ≥0∞ := - maximalFunction μ 𝓑 c r 1 u x +namespace MeasureTheory +section ContinuousENorm +variable {α E : Type*} {m : MeasurableSpace α} [ContinuousENorm E] {μ : Measure α} --- todo: move --- slightly more general than the Mathlib version --- the extra conclusion says that if there is a nonnegative radius, then we can choose `r b` to be --- larger than `r a` (up to a constant) -theorem exists_disjoint_subfamily_covering_enlargement_closedBall' {α} [MetricSpace α] (t : Set ι) - (x : ι → α) (r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) (τ : ℝ) (hτ : 3 < τ) : - ∃ u ⊆ t, - (u.PairwiseDisjoint fun a => closedBall (x a) (r a)) ∧ - ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b) ∧ - (∀ u ∈ t, 0 ≤ r u → r a ≤ (τ - 1) / 2 * r b) := by - rcases eq_empty_or_nonempty t with (rfl | _) - · exact ⟨∅, Subset.refl _, pairwiseDisjoint_empty, by simp⟩ - by_cases ht : ∀ a ∈ t, r a < 0 - · refine ⟨t, .rfl, fun a ha b _ _ ↦ by - simp only [Function.onFun, closedBall_eq_empty.2 (ht a ha), empty_disjoint], - fun a ha => ⟨a, ha, by simp only [closedBall_eq_empty.2 (ht a ha), empty_subset], - fun u hut hu ↦ (ht u hut).not_le hu |>.elim⟩⟩ - push_neg at ht - let t' := { a ∈ t | 0 ≤ r a } - have h2τ : 1 < (τ - 1) / 2 := by linarith - rcases exists_disjoint_subfamily_covering_enlargement (fun a => closedBall (x a) (r a)) t' r - ((τ - 1) / 2) h2τ (fun a ha => ha.2) R (fun a ha => hr a ha.1) fun a ha => - ⟨x a, mem_closedBall_self ha.2⟩ with - ⟨u, ut', u_disj, hu⟩ - have A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b) ∧ - ∀ u ∈ t, 0 ≤ r u → r a ≤ (τ - 1) / 2 * r b := by - intro a ha - rcases hu a ha with ⟨b, bu, hb, rb⟩ - refine ⟨b, bu, ?_⟩ - have : dist (x a) (x b) ≤ r a + r b := dist_le_add_of_nonempty_closedBall_inter_closedBall hb - exact ⟨closedBall_subset_closedBall' <| by linarith, fun _ _ _ ↦ rb⟩ - refine ⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => ?_⟩ - rcases le_or_lt 0 (r a) with (h'a | h'a) - · exact A a ⟨ha, h'a⟩ - · rcases ht with ⟨b, rb⟩ - rcases A b ⟨rb.1, rb.2⟩ with ⟨c, cu, _, hc⟩ - refine ⟨c, cu, by simp only [closedBall_eq_empty.2 h'a, empty_subset], fun _ _ _ ↦ ?_⟩ - have : 0 ≤ r c := nonneg_of_mul_nonneg_right (rb.2.trans <| hc b rb.1 rb.2) (by positivity) - exact h'a.le.trans <| by positivity +export ContinuousENorm (continuous_enorm) --- move to Vitali -theorem Vitali.exists_disjoint_subfamily_covering_enlargement_ball {α} [MetricSpace α] (t : Set ι) - (x : ι → α) (r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) (τ : ℝ) (hτ : 3 < τ) : - ∃ u ⊆ t, - (u.PairwiseDisjoint fun a => ball (x a) (r a)) ∧ - ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b) := by - obtain ⟨σ, hσ, hστ⟩ := exists_between hτ - obtain ⟨u, hut, hux, hu⟩ := - exists_disjoint_subfamily_covering_enlargement_closedBall' t x r R hr σ hσ - refine ⟨u, hut, fun i hi j hj hij ↦ ?_, fun a ha => ?_⟩ - · exact (hux hi hj hij).mono ball_subset_closedBall ball_subset_closedBall - obtain ⟨b, hbu, hb⟩ := hu a ha - refine ⟨b, hbu, ?_⟩ - obtain h2a|h2a := le_or_lt (r a) 0 - · simp_rw [ball_eq_empty.mpr h2a, empty_subset] - refine ball_subset_closedBall.trans hb.1 |>.trans <| closedBall_subset_ball ?_ - gcongr - apply pos_of_mul_pos_right <| h2a.trans_le <| hb.2 a ha h2a.le - linarith +protected theorem Continuous.enorm {X : Type*} [TopologicalSpace X] {f : X → E} + (hf : Continuous f) : Continuous (fun x => (‖f x‖ₑ)) := + continuous_enorm.comp hf -/- NOTE: This was changed to use `ℝ≥0∞` rather than `ℝ≥0` because that was more convenient for the -proof of `first_exception'` in ExceptionalSet.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 _root_.Set.Countable.measure_biUnion_le_lintegral [OpensMeasurableSpace X] (h𝓑 : 𝓑.Countable) - (l : ℝ≥0∞) (u : X → ℝ≥0∞) (R : ℝ) (hR : ∀ a ∈ 𝓑, r a ≤ R) - (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 ∂μ := by - obtain ⟨B, hB𝓑, hB, h2B⟩ := Vitali.exists_disjoint_subfamily_covering_enlargement_ball - 𝓑 c r R hR (2 ^ 2) (by norm_num) - have : Countable B := h𝓑.mono hB𝓑 - have disj := fun i j hij ↦ - hB (Subtype.coe_prop i) (Subtype.coe_prop j) (Subtype.coe_ne_coe.mpr hij) - calc - l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ l * μ (⋃ i ∈ B, ball (c i) (2 ^ 2 * r i)) := by - refine mul_left_mono (μ.mono fun x hx ↦ ?_) - simp only [mem_iUnion, mem_ball, exists_prop] at hx - rcases hx with ⟨i, i𝓑, hi⟩ - obtain ⟨b, bB, hb⟩ := h2B i i𝓑 - refine mem_iUnion₂.mpr ⟨b, bB, hb <| mem_ball.mpr hi⟩ - _ ≤ l * ∑' i : B, μ (ball (c i) (2 ^ 2 * r i)) := - mul_left_mono <| measure_biUnion_le μ (h𝓑.mono hB𝓑) fun i ↦ ball (c i) (2 ^ 2 * r i) - _ ≤ l * ∑' i : B, A ^ 2 * μ (ball (c i) (r i)) := by - refine mul_left_mono <| ENNReal.tsum_le_tsum (fun i ↦ ?_) - rw [sq, sq, mul_assoc, mul_assoc] - apply (Measure.IsDoubling.measure_ball_two_le_same (c i) (2 * r i)).trans - exact mul_left_mono (Measure.IsDoubling.measure_ball_two_le_same (c i) (r i)) - _ = A ^ 2 * ∑' i : B, l * μ (ball (c i) (r i)) := by - rw [ENNReal.tsum_mul_left, ENNReal.tsum_mul_left, ← mul_assoc, ← mul_assoc, mul_comm l] - _ ≤ A ^ 2 * ∑' i : B, ∫⁻ x in ball (c i) (r i), u x ∂μ := by - gcongr; exact h2u _ (hB𝓑 (Subtype.coe_prop _)) - _ = A ^ 2 * ∫⁻ x in ⋃ i ∈ B, ball (c i) (r i), u x ∂μ := by - congr; simpa using (lintegral_iUnion (fun i ↦ measurableSet_ball) disj u).symm - _ ≤ A ^ 2 * ∫⁻ x, u x ∂μ := by - gcongr; exact setLIntegral_le_lintegral (⋃ i ∈ B, ball (c i) (r i)) u +theorem measurable_enorm [MeasurableSpace E] [OpensMeasurableSpace E] : + Measurable (fun a : E => (‖a‖ₑ)) := + continuous_enorm.measurable -protected theorem AEStronglyMeasurable.maximalFunction [BorelSpace X] {p : ℝ} - {u : X → E} (h𝓑 : 𝓑.Countable) : AEStronglyMeasurable (maximalFunction μ 𝓑 c r p u) μ := - (AEMeasurable.biSup 𝓑 h𝓑 fun _ _ ↦ aemeasurable_const.indicator measurableSet_ball).pow - aemeasurable_const |>.aestronglyMeasurable +protected theorem AEMeasurable.enorm [MeasurableSpace E] [OpensMeasurableSpace E] {f : α → E} + (hf : AEMeasurable f μ) : AEMeasurable (fun a => (‖f a‖ₑ)) μ := + measurable_enorm.comp_aemeasurable hf -protected theorem HasWeakType.MB_one' [BorelSpace X] (h𝓑 : 𝓑.Countable) - {R : ℝ} (hR : ∀ i ∈ 𝓑, r i ≤ R) : - HasWeakType (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x) 1 1 μ μ (A ^ 2) := by - intro f _ - use AEStronglyMeasurable.maximalFunction h𝓑 - let Bₗ (ℓ : ℝ≥0∞) := { i ∈ 𝓑 | ∫⁻ y in (ball (c i) (r i)), ‖f y‖₊ ∂μ ≥ ℓ * μ (ball (c i) (r i)) } - simp only [wnorm, one_ne_top, wnorm', one_toReal, inv_one, ENNReal.rpow_one, reduceIte, - ENNReal.coe_pow, eLpNorm, one_ne_zero, eLpNorm', ne_eq, not_false_eq_true, div_self, - iSup_le_iff] - intro t - by_cases ht : t = 0 - · simp [ht] - have hBₗ : (Bₗ t).Countable := h𝓑.mono (fun i hi ↦ mem_of_mem_inter_left hi) - refine le_trans ?_ (hBₗ.measure_biUnion_le_lintegral (c := c) (r := r) (l := t) - (u := fun x ↦ ‖f x‖₊) (R := R) ?_ ?_) - · refine mul_left_mono <| μ.mono (fun x hx ↦ mem_iUnion₂.mpr ?_) - -- We need a ball in `Bₗ t` containing `x`. Since `MB μ 𝓑 c r f x` is large, such a ball exists - simp only [mem_setOf_eq] at hx - -- replace hx := lt_of_lt_of_le hx coe_toNNReal_le_self - simp only [MB, maximalFunction, ENNReal.rpow_one, inv_one] at hx - obtain ⟨i, ht⟩ := lt_iSup_iff.mp hx - replace hx : x ∈ ball (c i) (r i) := - by_contradiction <| fun h ↦ not_lt_of_ge (zero_le t) (ENNReal.coe_lt_coe.mp <| by simp [h] at ht) - refine ⟨i, ?_, hx⟩ - -- It remains only to confirm that the chosen ball is actually in `Bₗ t` - simp only [ge_iff_le, mem_setOf_eq, Bₗ] - have hi : i ∈ 𝓑 := - by_contradiction <| fun h ↦ not_lt_of_ge (zero_le t) (ENNReal.coe_lt_coe.mp <| by simp [h] at ht) - exact ⟨hi, mul_le_of_le_div <| le_of_lt (by simpa [setLaverage_eq, hi, hx] using ht)⟩ - · exact fun i hi ↦ hR i (mem_of_mem_inter_left hi) - · exact fun i hi ↦ hi.2.trans (setLIntegral_mono' measurableSet_ball fun x _ ↦ by simp) +protected theorem AEStronglyMeasurable.enorm {f : α → E} + (hf : AEStronglyMeasurable f μ) : AEMeasurable (fun a => (‖f a‖ₑ)) μ := + continuous_enorm.comp_aestronglyMeasurable hf |>.aemeasurable -end tmp +end ContinuousENorm end MeasureTheory diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index 4f82be42..d098de83 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/Carleson/ToMathlib/Misc.lean @@ -181,6 +181,7 @@ lemma laverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g ⨍⁻ a, f a ∂μ ≤ ⨍⁻ a, g a ∂μ := by exact lintegral_mono_ae <| h.filter_mono <| Measure.ae_mono' Measure.smul_absolutelyContinuous +@[gcongr] 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 diff --git a/Carleson/WeakType.lean b/Carleson/WeakType.lean index 689cc8da..118a31fc 100644 --- a/Carleson/WeakType.lean +++ b/Carleson/WeakType.lean @@ -3,12 +3,39 @@ import Mathlib.MeasureTheory.Integral.Layercake import Mathlib.MeasureTheory.Integral.Lebesgue import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar import Mathlib.Analysis.SpecialFunctions.Pow.Integral +import Carleson.ToMathlib.ENorm +import Carleson.ToMathlib.Misc noncomputable section open NNReal ENNReal NormedSpace MeasureTheory Set Filter Topology Function -variable {α α' 𝕜 E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m : MeasurableSpace α'} +section move + + +variable {α 𝕜 E : Type*} {m : MeasurableSpace α} + {μ : Measure α} [NontriviallyNormedField 𝕜] + [NormedAddCommGroup E] [NormedSpace 𝕜 E] + +-- todo: move/rename/and perhaps reformulate in terms of ‖.‖ₑ +lemma ENNNorm_absolute_homogeneous {c : 𝕜} (z : E) : ofNNReal ‖c • z‖₊ = ↑‖c‖₊ * ↑‖z‖₊ := + (toReal_eq_toReal_iff' coe_ne_top coe_ne_top).mp (norm_smul c z) + +lemma ENNNorm_add_le (y z : E) : ofNNReal ‖y + z‖₊ ≤ ↑‖y‖₊ + ↑‖z‖₊ := + (toReal_le_toReal coe_ne_top coe_ne_top).mp (nnnorm_add_le ..) + +lemma measure_mono_ae' {A B : Set α} (h : μ (B \ A) = 0) : + μ B ≤ μ A := by + apply measure_mono_ae + change μ {x | ¬ B x ≤ A x} = 0 + simp only [le_Prop_eq, Classical.not_imp] + exact h + +end move + +namespace MeasureTheory + +variable {α α' ε ε₁ ε₂ 𝕜 E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m : MeasurableSpace α'} {p p' q : ℝ≥0∞} {c : ℝ≥0} {μ : Measure α} {ν : Measure α'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] @@ -16,14 +43,12 @@ variable {α α' 𝕜 E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m : Me [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] (L : E₁ →L[𝕜] E₂ →L[𝕜] E₃) - {f g : α → E} {t s x y : ℝ≥0∞} - {T : (α → E₁) → (α' → E₂)} + {t s x y : ℝ≥0∞} + {T : (α → ε₁) → (α' → ε₂)} --- #check meas_ge_le_mul_pow_eLpNorm -- Chebyshev's inequality +section ENorm -namespace MeasureTheory -/- If we need more properties of `E`, we can add `[RCLike 𝕜]` *instead of* the above type-classes-/ --- #check _root_.RCLike +variable [ENorm ε] {f g g₁ g₂ : α → ε} /- Proofs for this file can be found in Folland, Real Analysis. Modern Techniques and Their Applications, section 6.3. -/ @@ -34,20 +59,8 @@ Folland, Real Analysis. Modern Techniques and Their Applications, section 6.3. - Note that unlike the notes, we also define this for `t = ∞`. Note: we also want to use this for functions with codomain `ℝ≥0∞`, but for those we just write `μ { x | t < f x }` -/ -def distribution [NNNorm E] (f : α → E) (t : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ := - μ { x | t < ‖f x‖₊ } - -@[gcongr] -lemma distribution_mono_left (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) : - distribution f t μ ≤ distribution g t μ := by - have h₀ : {x | t < ‖f x‖₊} \ {x | t < ‖g x‖₊} ⊆ {x | ¬‖f x‖ ≤ ‖g x‖} := fun x ↦ by - simp only [mem_diff, mem_setOf_eq, not_lt, not_le, and_imp] - intro i₁ i₂; simpa using i₂.trans_lt i₁ - calc - _ ≤ μ ({x | t < ‖f x‖₊} ∩ {x | t < ‖g x‖₊}) - + μ ({x | t < ‖f x‖₊} \ {x | t < ‖g x‖₊}) := measure_le_inter_add_diff μ _ _ - _ = μ ({x | t < ‖f x‖₊} ∩ {x | t < ‖g x‖₊}) := by rw [measure_mono_null h₀ h, add_zero] - _ ≤ _ := by apply measure_mono; simp +def distribution (f : α → ε) (t : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ := + μ { x | t < ‖f x‖ₑ } @[gcongr] lemma distribution_mono_right (h : t ≤ s) : distribution f s μ ≤ distribution f t μ := @@ -56,17 +69,6 @@ lemma distribution_mono_right (h : t ≤ s) : distribution f s μ ≤ distributi lemma distribution_mono_right' : (Antitone (fun t ↦ distribution f t μ)) := fun _ _ h ↦ distribution_mono_right h -@[gcongr] -lemma distribution_mono (h₁ : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) (h₂ : t ≤ s) : - distribution f s μ ≤ distribution g t μ := - (distribution_mono_left h₁).trans (distribution_mono_right h₂) - -lemma ENNNorm_absolute_homogeneous {c : 𝕜} (z : E) : ofNNReal ‖c • z‖₊ = ↑‖c‖₊ * ↑‖z‖₊ := - (toReal_eq_toReal_iff' coe_ne_top coe_ne_top).mp (norm_smul c z) - -lemma distribution_snormEssSup : distribution f (eLpNormEssSup f μ) μ = 0 := - meas_eLpNormEssSup_lt - @[measurability, fun_prop] lemma distribution_measurable₀ : Measurable (fun t ↦ distribution f t μ) := Antitone.measurable (distribution_mono_right' (f := f) (μ := μ)) @@ -76,69 +78,40 @@ lemma distribution_measurable {g : α' → ℝ≥0∞} (hg : Measurable g) : Measurable (fun y : α' ↦ distribution f (g y) μ) := by fun_prop -/-@[measurability, deprecated] -lemma distribution_measurable_from_real : - Measurable (fun t : ℝ ↦ distribution f (.ofReal t) μ) := - distribution_measurable measurable_ofReal-/ - -lemma ENNNorm_add_le (y z : E) : ofNNReal ‖y + z‖₊ ≤ ↑‖y‖₊ + ↑‖z‖₊ := - (toReal_le_toReal coe_ne_top coe_ne_top).mp (nnnorm_add_le ..) - -lemma distribution_smul_left {c : 𝕜} (hc : c ≠ 0) : - distribution (c • f) t μ = distribution f (t / ‖c‖₊) μ := by +lemma distribution_toReal_le {f : α → ℝ≥0∞} : + distribution (ENNReal.toReal ∘ f) t μ ≤ distribution f t μ := by + simp_rw [distribution] + apply measure_mono + simp_rw [comp_apply, enorm_eq_self, setOf_subset_setOf] + intro x hx + exact hx.trans_le enorm_toReal_le + +lemma distribution_add_le_of_enorm {A : ℝ≥0∞} + (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ A * (‖g₁ x‖ₑ + ‖g₂ x‖ₑ)) : + distribution f (A * (t + s)) μ ≤ distribution g₁ t μ + distribution g₂ s μ := by unfold distribution - have h₀ : ofNNReal ‖c‖₊ ≠ 0 := ENNReal.coe_ne_zero.mpr (nnnorm_ne_zero_iff.mpr hc) - congr with x - simp only [Pi.smul_apply, mem_setOf_eq] - rw [← @ENNReal.mul_lt_mul_right (t / ‖c‖₊) _ (‖c‖₊) h₀ coe_ne_top, - ENNNorm_absolute_homogeneous _, mul_comm, ENNReal.div_mul_cancel h₀ coe_ne_top] - -lemma measure_mono_ae' {A B : Set α} (h : μ (B \ A) = 0) : - μ B ≤ μ A := by - apply measure_mono_ae - change μ {x | ¬ B x ≤ A x} = 0 - simp only [le_Prop_eq, Classical.not_imp] - exact h - -lemma distribution_add_le' {A : ℝ} (hA : A ≥ 0) (g₁ g₂ : α → E) - (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ A * (‖g₁ x‖ + ‖g₂ x‖)) : - distribution f (ENNReal.ofReal A * (t + s)) μ ≤ distribution g₁ t μ + distribution g₂ s μ := by - unfold distribution - have h₁ : μ ({x | ENNReal.ofReal A * (t + s) < ↑‖f x‖₊} \ - ({x | t < ↑‖g₁ x‖₊} ∪ {x | s < ↑‖g₂ x‖₊})) = 0 := by + have h₁ : μ ({x | A * (t + s) < ‖f x‖ₑ} \ + ({x | t < ‖g₁ x‖ₑ} ∪ {x | s < ‖g₂ x‖ₑ})) = 0 := by apply measure_mono_null ?_ h intro x simp only [mem_diff, mem_setOf_eq, mem_union, not_or, not_lt, mem_compl_iff, not_le, and_imp] intro h₁ h₂ h₃ - refine (ofReal_lt_ofReal_iff_of_nonneg (by positivity)).mp ?_ - rw [ofReal_mul, ofReal_add] <;> try positivity - repeat rw [ofReal_norm_eq_coe_nnnorm] <;> try positivity refine lt_of_le_of_lt ?_ h₁ gcongr calc - μ {x | ENNReal.ofReal A * (t + s) < ‖f x‖₊} - ≤ μ ({x | t < ↑‖g₁ x‖₊} ∪ {x | s < ↑‖g₂ x‖₊}) := measure_mono_ae' h₁ - _ ≤ μ {x | t < ↑‖g₁ x‖₊} + μ {x | s < ↑‖g₂ x‖₊} := measure_union_le _ _ - -lemma distribution_add_le : - distribution (f + g) (t + s) μ ≤ distribution f t μ + distribution g s μ := - calc - _ ≤ μ ({x | t < ↑‖f x‖₊} ∪ {x | s < ↑‖g x‖₊}) := by - refine measure_mono fun x h ↦ ?_ - simp only [mem_union, mem_setOf_eq, Pi.add_apply] at h ⊢ - contrapose! h - exact (ENNNorm_add_le _ _).trans (add_le_add h.1 h.2) - _ ≤ _ := measure_union_le _ _ + μ {x | A * (t + s) < ‖f x‖ₑ} + ≤ μ ({x | t < ‖g₁ x‖ₑ} ∪ {x | s < ‖g₂ x‖ₑ}) := measure_mono_ae' h₁ + _ ≤ μ {x | t < ‖g₁ x‖ₑ} + μ {x | s < ‖g₂ x‖ₑ} := measure_union_le _ _ lemma approx_above_superset (t₀ : ℝ≥0∞) : - ⋃ n, (fun n : ℕ ↦ {x | t₀ + (↑n)⁻¹ < ↑‖f x‖₊}) n = {x | t₀ < ‖f x‖₊} := by + ⋃ n, (fun n : ℕ ↦ {x | t₀ + (↑n)⁻¹ < ‖f x‖ₑ}) n = {x | t₀ < ‖f x‖ₑ} := by ext y constructor <;> intro h · obtain ⟨n, wn⟩ := exists_exists_eq_and.mp h calc t₀ ≤ t₀ + (↑n)⁻¹ := le_self_add - _ < ↑‖f y‖₊ := wn - · have h₁ : Iio (↑‖f y‖₊ - t₀) ∈ 𝓝 0 := Iio_mem_nhds (tsub_pos_of_lt h) + _ < ‖f y‖ₑ := wn + · have h₁ : Iio (‖f y‖ₑ - t₀) ∈ 𝓝 0 := Iio_mem_nhds (tsub_pos_of_lt h) have h₂ := ENNReal.tendsto_inv_nat_nhds_zero h₁ simp only [mem_map, mem_atTop_sets, mem_preimage, mem_Iio] at h₂ rcases h₂ with ⟨n, wn⟩ @@ -147,8 +120,8 @@ lemma approx_above_superset (t₀ : ℝ≥0∞) : exact lt_tsub_iff_left.mp (wn n (Nat.le_refl n)) lemma tendsto_measure_iUnion_distribution (t₀ : ℝ≥0∞) : - Filter.Tendsto (⇑μ ∘ (fun n : ℕ ↦ {x | t₀ + (↑n)⁻¹ < ‖f x‖₊})) - Filter.atTop (nhds (μ ({x | t₀ < ‖f x‖₊}))) := by + Filter.Tendsto (⇑μ ∘ (fun n : ℕ ↦ {x | t₀ + (↑n)⁻¹ < ‖f x‖ₑ})) + Filter.atTop (nhds (μ ({x | t₀ < ‖f x‖ₑ}))) := by rw [← approx_above_superset] apply tendsto_measure_iUnion_atTop intro a b h x h₁ @@ -156,7 +129,8 @@ lemma tendsto_measure_iUnion_distribution (t₀ : ℝ≥0∞) : _ ≤ t₀ + (↑a)⁻¹ := by gcongr _ < _ := h₁ -lemma select_neighborhood_distribution (t₀ : ℝ≥0∞) (l : ℝ≥0∞) (hu : l < distribution f t₀ μ) : +lemma select_neighborhood_distribution (t₀ : ℝ≥0∞) (l : ℝ≥0∞) + (hu : l < distribution f t₀ μ) : ∃ n : ℕ, l < distribution f (t₀ + (↑n)⁻¹) μ := by have h₁ : Ioi l ∈ (𝓝 (distribution f t₀ μ)) := Ioi_mem_nhds hu have h₂ := (tendsto_measure_iUnion_distribution t₀) h₁ @@ -221,27 +195,6 @@ lemma continuousWithinAt_distribution (t₀ : ℝ≥0∞) : ≤ distribution f t₀ μ := distribution_mono_right (le_of_lt h.2) _ ≤ distribution f t₀ μ + ε := le_self_add -lemma _root_.ContinuousLinearMap.distribution_le {f : α → E₁} {g : α → E₂} : - distribution (fun x ↦ L (f x) (g x)) (‖L‖₊ * t * s) μ ≤ - distribution f t μ + distribution g s μ := by - unfold distribution - have h₀ : {x | ↑‖L‖₊ * t * s < ↑‖(fun x ↦ (L (f x)) (g x)) x‖₊} ⊆ - {x | t < ↑‖f x‖₊} ∪ {x | s < ↑‖g x‖₊} := fun z hz ↦ by - simp only [mem_union, mem_setOf_eq, Pi.add_apply] at hz ⊢ - contrapose! hz - calc - (‖(L (f z)) (g z)‖₊ : ℝ≥0∞) ≤ ‖L‖₊ * ‖f z‖₊ * ‖g z‖₊ := by - refine (toNNReal_le_toNNReal coe_ne_top coe_ne_top).mp ?_ - simp only [toNNReal_coe, coe_mul, toNNReal_mul] - calc - _ ≤ ↑‖L (f z)‖₊ * ↑‖g z‖₊ := ContinuousLinearMap.le_opNNNorm (L (f z)) (g z) - _ ≤ ‖L‖₊ * ‖f z‖₊ * ‖g z‖₊ := - mul_le_mul' (ContinuousLinearMap.le_opNNNorm L (f z)) (by rfl) - _ ≤ _ := mul_le_mul' (mul_le_mul_left' hz.1 ↑‖L‖₊) hz.2 - calc - _ ≤ μ ({x | t < ↑‖f x‖₊} ∪ {x | s < ↑‖g x‖₊}) := measure_mono h₀ - _ ≤ _ := measure_union_le _ _ - /- The lemmas below are almost already in Mathlib, see `MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul`. -/ @@ -252,136 +205,251 @@ lemma _root_.ContinuousLinearMap.distribution_le {f : α → E₁} {g : α → E -- ∫⁻ t in Ioi (0 : ℝ), .ofReal (p * t ^ (p - 1)) * μ { x | ENNReal.ofReal t < f x } := by -- sorry -section BorelSpace +/-- The weak L^p norm of a function, for `p < ∞` -/ +def wnorm' (f : α → ε) (p : ℝ) (μ : Measure α) : ℝ≥0∞ := + ⨆ t : ℝ≥0, t * distribution f t μ ^ (p : ℝ)⁻¹ -variable [MeasurableSpace E] [BorelSpace E] (hf : AEMeasurable f μ) -include hf +lemma wnorm'_zero (f : α → ε) (μ : Measure α) : wnorm' f 0 μ = ∞ := by + simp only [wnorm', GroupWithZero.inv_zero, ENNReal.rpow_zero, mul_one, iSup_eq_top] + refine fun b hb ↦ ⟨b.toNNReal + 1, ?_⟩ + rw [coe_add, ENNReal.coe_one, coe_toNNReal hb.ne_top] + exact lt_add_right hb.ne_top one_ne_zero -/-- The layer-cake theorem, or Cavalieri's principle for functions into a normed group. -/ -lemma lintegral_norm_pow_eq_distribution {p : ℝ} (hp : 0 < p) : - ∫⁻ x, ‖f x‖ₑ ^ p ∂μ = - ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (p * t ^ (p - 1)) * distribution f (.ofReal t) μ := by - have h2p : 0 ≤ p := hp.le - have := lintegral_rpow_eq_lintegral_meas_lt_mul μ (f := fun x ↦ ‖f x‖) - (Eventually.of_forall fun x ↦ norm_nonneg _) hf.norm hp - simp only [norm_nonneg, ← ofReal_rpow_of_nonneg, mul_comm (μ _), ne_eq, ofReal_ne_top, - not_false_eq_true, ← lintegral_const_mul', ← mul_assoc, ← ofReal_norm_eq_coe_nnnorm, ofReal_mul, - distribution, h2p] at this ⊢ - convert this using 1 - · simp [ENNReal.ofReal, enorm_eq_nnnorm, norm_toNNReal] - refine setLIntegral_congr_fun measurableSet_Ioi (Eventually.of_forall fun x hx ↦ ?_) - simp_rw [ENNReal.ofReal_lt_ofReal_iff_of_nonneg (le_of_lt hx)] +lemma wnorm'_toReal_le {f : α → ℝ≥0∞} {p : ℝ} (hp : 0 ≤ p) : + wnorm' (ENNReal.toReal ∘ f) p μ ≤ wnorm' f p μ := by + refine iSup_mono fun x ↦ ?_ + gcongr + exact distribution_toReal_le -/-- The layer-cake theorem, or Cavalieri's principle, written using `eLpNorm`. -/ -lemma eLpNorm_pow_eq_distribution {p : ℝ≥0} (hp : 0 < p) : - eLpNorm f p μ ^ (p : ℝ) = - ∫⁻ t in Ioi (0 : ℝ), p * ENNReal.ofReal (t ^ ((p : ℝ) - 1)) * distribution f (.ofReal t) μ := by - have h2p : 0 < (p : ℝ) := hp - simp_rw [eLpNorm_nnreal_eq_eLpNorm' hp.ne', eLpNorm', one_div, ← ENNReal.rpow_mul, - inv_mul_cancel₀ h2p.ne', ENNReal.rpow_one, lintegral_norm_pow_eq_distribution hf h2p, - ENNReal.ofReal_mul zero_le_coe, ofReal_coe_nnreal] +/-- The weak L^p norm of a function. -/ +def wnorm (f : α → ε) (p : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ := + if p = ∞ then eLpNormEssSup f μ else wnorm' f (ENNReal.toReal p) μ -/-- The layer-cake theorem, or Cavalieri's principle, written using `eLpNorm`, without - taking powers. -/ -lemma eLpNorm_eq_distribution {p : ℝ} (hp : 0 < p) : - eLpNorm f (.ofReal p) μ = - (ENNReal.ofReal p * ∫⁻ t in Ioi (0 : ℝ), distribution f (.ofReal t) μ * - ENNReal.ofReal (t ^ (p - 1)) ) ^ p⁻¹ := by - unfold eLpNorm - split_ifs with sgn_p sz_p - · exact False.elim (not_le_of_lt hp (ofReal_eq_zero.mp sgn_p)) - · exact False.elim (coe_ne_top sz_p) - · unfold eLpNorm' - rw [toReal_ofReal (le_of_lt hp), one_div] - congr 1 - rw [← lintegral_const_mul'] - on_goal 2 => exact coe_ne_top - rw [lintegral_norm_pow_eq_distribution hf hp] - congr 1 with x; rw [ofReal_mul] <;> [ring; positivity] +lemma wnorm_zero : wnorm f 0 μ = ∞ := by + simp [wnorm, wnorm'_zero] -lemma lintegral_pow_mul_distribution {p : ℝ} (hp : -1 < p) : - ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (t ^ p) * distribution f (.ofReal t) μ = - ENNReal.ofReal (p + 1)⁻¹ * ∫⁻ x, ‖f x‖ₑ ^ (p + 1) ∂μ := by - have h2p : 0 < p + 1 := by linarith - have h3p : 0 ≤ p + 1 := by linarith - have h4p : p + 1 ≠ 0 := by linarith - simp [*, lintegral_norm_pow_eq_distribution, ← lintegral_const_mul', ← ofReal_mul, ← mul_assoc] +@[simp] +lemma wnorm_top : wnorm f ⊤ μ = eLpNormEssSup f μ := by simp [wnorm] -end BorelSpace +lemma wnorm_coe {p : ℝ≥0} : wnorm f p μ = wnorm' f p μ := by simp [wnorm] -/-- The weak L^p norm of a function, for `p < ∞` -/ -def wnorm' [NNNorm E] (f : α → E) (p : ℝ) (μ : Measure α) : ℝ≥0∞ := - ⨆ t : ℝ≥0, t * distribution f t μ ^ (p : ℝ)⁻¹ +lemma wnorm_ofReal {p : ℝ} (hp : 0 ≤ p) : wnorm f (.ofReal p) μ = wnorm' f p μ := by + simp [wnorm, hp] + +-- todo: move +lemma eLpNormEssSup_toReal_le {f : α → ℝ≥0∞} : + eLpNormEssSup (ENNReal.toReal ∘ f) μ ≤ eLpNormEssSup f μ := by + simp_rw [eLpNormEssSup, enorm_eq_self] + apply essSup_mono_ae + apply Eventually.of_forall + simp [enorm_toReal_le, implies_true] + +lemma wnorm_toReal_le {f : α → ℝ≥0∞} {p : ℝ≥0∞} : + wnorm (ENNReal.toReal ∘ f) p μ ≤ wnorm f p μ := by + induction p + · simp [eLpNormEssSup_toReal_le] + refine iSup_mono fun x ↦ ?_ + gcongr + exact distribution_toReal_le + +end ENorm + +section ContinuousENorm + +variable [ContinuousENorm ε] [ContinuousENorm ε₁] [ContinuousENorm ε₂] {f : α → ε} {f₁ : α → ε₁} -lemma wnorm'_le_eLpNorm' {f : α → E} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 1 ≤ p) : +lemma wnorm'_le_eLpNorm' (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 1 ≤ p) : wnorm' f p μ ≤ eLpNorm' f p μ := by refine iSup_le (fun t ↦ ?_) - unfold eLpNorm' distribution + simp_rw [distribution, eLpNorm'] have p0 : 0 < p := lt_of_lt_of_le one_pos hp have p0' : 0 ≤ 1 / p := (div_pos one_pos p0).le - have set_eq : {x | ofNNReal t < ‖f x‖₊} = {x | ofNNReal t ^ p < ‖f x‖₊ ^ p} := by + have set_eq : {x | ofNNReal t < ‖f x‖ₑ} = {x | ofNNReal t ^ p < ‖f x‖ₑ ^ p} := by simp [ENNReal.rpow_lt_rpow_iff p0] have : ofNNReal t = (ofNNReal t ^ p) ^ (1 / p) := by simp [p0.ne.symm] nth_rewrite 1 [inv_eq_one_div p, this, ← mul_rpow_of_nonneg _ _ p0', set_eq] refine rpow_le_rpow ?_ p0' - refine le_trans ?_ <| mul_meas_ge_le_lintegral₀ (hf.ennnorm.pow_const p) (ofNNReal t ^ p) + refine le_trans ?_ <| mul_meas_ge_le_lintegral₀ (hf.enorm.pow_const p) (ofNNReal t ^ p) gcongr exact setOf_subset_setOf.mpr (fun _ h ↦ h.le) -/-- The weak L^p norm of a function. -/ -def wnorm [NNNorm E] (f : α → E) (p : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ := - if p = ∞ then eLpNormEssSup f μ else wnorm' f (ENNReal.toReal p) μ - -lemma wnorm_le_eLpNorm {f : α → E} (hf : AEStronglyMeasurable f μ) {p : ℝ≥0∞} (hp : 1 ≤ p) : +lemma wnorm_le_eLpNorm (hf : AEStronglyMeasurable f μ) {p : ℝ≥0∞} (hp : 1 ≤ p) : wnorm f p μ ≤ eLpNorm f p μ := by by_cases h : p = ⊤ - · simp [h, wnorm] + · simp [h, wnorm, eLpNorm] · have p0 : p ≠ 0 := (lt_of_lt_of_le one_pos hp).ne.symm simpa [h, wnorm, eLpNorm, p0] using wnorm'_le_eLpNorm' hf (toReal_mono h hp) /-- A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm. -/ -def MemWℒp [NNNorm E] (f : α → E) (p : ℝ≥0∞) (μ : Measure α) : Prop := +def MemWℒp (f : α → ε) (p : ℝ≥0∞) (μ : Measure α) : Prop := AEStronglyMeasurable f μ ∧ wnorm f p μ < ∞ -lemma Memℒp.memWℒp {f : α → E} {p : ℝ≥0∞} (hp : 1 ≤ p) (hf : Memℒp f p μ) : - MemWℒp f p μ := - ⟨hf.1, lt_of_le_of_lt (wnorm_le_eLpNorm hf.1 hp) hf.2⟩ +lemma Memℒp.memWℒp (hp : 1 ≤ p) (hf : Memℒp f p μ) : MemWℒp f p μ := + ⟨hf.1, wnorm_le_eLpNorm hf.1 hp |>.trans_lt hf.2⟩ + +lemma MemWℒp_zero : ¬ MemWℒp f 0 μ := by + simp [MemWℒp, wnorm_zero] + +lemma MemWℒp.aeStronglyMeasurable (hf : MemWℒp f p μ) : AEStronglyMeasurable f μ := + hf.1 + +lemma MemWℒp.wnorm_lt_top (hf : MemWℒp f p μ) : wnorm f p μ < ⊤ := + hf.2 + +lemma MemWℒp.ennreal_toReal {f : α → ℝ≥0∞} (hf : MemWℒp f p μ) : + MemWℒp (ENNReal.toReal ∘ f) p μ := + ⟨hf.aeStronglyMeasurable.ennreal_toReal, wnorm_toReal_le.trans_lt hf.2⟩ + +/-- If a function `f` is `MemWℒp`, then its norm is almost everywhere finite.-/ +theorem MemWℒp.ae_ne_top {f : α → ε} {p : ℝ≥0∞} {μ : Measure α} + (hf : MemWℒp f p μ) : ∀ᵐ x ∂μ, ‖f x‖ₑ ≠ ∞ := by + by_cases hp_inf : p = ∞ + · rw [hp_inf] at hf + simp_rw [← lt_top_iff_ne_top] + exact ae_lt_of_essSup_lt hf.2 + by_cases hp_zero : p = 0 + · exact (MemWℒp_zero <| hp_zero ▸ hf).elim + set A := {x | ‖f x‖ₑ = ∞} with hA + unfold MemWℒp wnorm wnorm' at hf + simp only [hp_inf] at hf + rw [Filter.eventually_iff, mem_ae_iff] + simp only [ne_eq, compl_def, mem_setOf_eq, Decidable.not_not, ← hA] + have hp_toReal_zero := toReal_ne_zero.mpr ⟨hp_zero, hp_inf⟩ + have h1 (t : ℝ≥0) : μ A ≤ distribution f t μ := by + refine μ.mono ?_ + simp_all only [setOf_subset_setOf, coe_lt_top, implies_true, A] + set C := ⨆ t : ℝ≥0, t * distribution f t μ ^ p.toReal⁻¹ + by_cases hC_zero : C = 0 + · simp only [ENNReal.iSup_eq_zero, mul_eq_zero, ENNReal.rpow_eq_zero_iff, inv_neg'', C] at hC_zero + specialize hC_zero 1 + simp only [one_ne_zero, ENNReal.coe_one, toReal_nonneg.not_lt, and_false, or_false, + false_or] at hC_zero + exact measure_mono_null (setOf_subset_setOf.mpr fun x hx => hx ▸ one_lt_top) hC_zero.1 + by_contra h + have h2 : C < ∞ := by aesop + have h3 (t : ℝ≥0) : distribution f t μ ≤ (C / t) ^ p.toReal := by + rw [← rpow_inv_rpow hp_toReal_zero (distribution ..)] + refine rpow_le_rpow ?_ toReal_nonneg + rw [ENNReal.le_div_iff_mul_le (Or.inr hC_zero) (Or.inl coe_ne_top), mul_comm] + exact le_iSup_iff.mpr fun _ a ↦ a t + have h4 (t : ℝ≥0) : μ A ≤ (C / t) ^ p.toReal := (h1 t).trans (h3 t) + have h5 : μ A ≤ μ A / 2 := by + convert h4 (C * (2 / μ A) ^ p.toReal⁻¹).toNNReal + rw [coe_toNNReal ?_] + swap + · refine mul_ne_top h2.ne_top (rpow_ne_top_of_nonneg (inv_nonneg.mpr toReal_nonneg) ?_) + simp [div_eq_top, h] + nth_rw 1 [← mul_one C] + rw [ENNReal.mul_div_mul_left _ _ hC_zero h2.ne_top, div_rpow_of_nonneg _ _ toReal_nonneg, + ENNReal.rpow_inv_rpow hp_toReal_zero, ENNReal.one_rpow, one_div, + ENNReal.inv_div (Or.inr two_ne_top) (Or.inr (NeZero.ne' 2).symm)] + have h6 : μ A = 0 := by + convert (fun hh ↦ ENNReal.half_lt_self hh (ne_top_of_le_ne_top (rpow_ne_top_of_nonneg + toReal_nonneg ((div_one C).symm ▸ h2.ne_top)) (h4 1))).mt h5.not_lt + tauto + exact h h6 /- Todo: define `MeasureTheory.WLp` as a subgroup, similar to `MeasureTheory.Lp` -/ /-- An operator has weak type `(p, q)` if it is bounded as a map from L^p to weak-L^q. `HasWeakType T p p' μ ν c` means that `T` has weak type (p, p') w.r.t. measures `μ`, `ν` and constant `c`. -/ -def HasWeakType (T : (α → E₁) → (α' → E₂)) (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') +def HasWeakType (T : (α → ε₁) → (α' → ε₂)) (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0) : Prop := - ∀ f : α → E₁, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ wnorm (T f) p' ν ≤ c * eLpNorm f p μ + ∀ f : α → ε₁, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ wnorm (T f) p' ν ≤ c * eLpNorm f p μ /-- An operator has strong type (p, q) if it is bounded as an operator on `L^p → L^q`. `HasStrongType T p p' μ ν c` means that `T` has strong type (p, p') w.r.t. measures `μ`, `ν` and constant `c`. -/ -def HasStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] - {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → E) → (α' → E')) +def HasStrongType {α α' : Type*} + {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → ε₁) → (α' → ε₂)) (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0) : Prop := - ∀ f : α → E, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ eLpNorm (T f) p' ν ≤ c * eLpNorm f p μ + ∀ f : α → ε₁, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ eLpNorm (T f) p' ν ≤ c * eLpNorm f p μ /-- A weaker version of `HasStrongType`. This is the same as `HasStrongType` if `T` is continuous w.r.t. the L^2 norm, but weaker in general. -/ -def HasBoundedStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] - {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → E) → (α' → E')) +def HasBoundedStrongType {α α' : Type*} [Zero ε₁] + {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → ε₁) → (α' → ε₂)) (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0) : Prop := - ∀ f : α → E, Memℒp f p μ → eLpNorm f ∞ μ < ∞ → μ (support f) < ∞ → + ∀ f : α → ε₁, Memℒp f p μ → eLpNorm f ∞ μ < ∞ → μ (support f) < ∞ → AEStronglyMeasurable (T f) ν ∧ eLpNorm (T f) p' ν ≤ c * eLpNorm f p μ +lemma HasWeakType.memWℒp (h : HasWeakType T p p' μ ν c) (hf₁ : Memℒp f₁ p μ) : + MemWℒp (T f₁) p' ν := + ⟨(h f₁ hf₁).1, h f₁ hf₁ |>.2.trans_lt <| mul_lt_top coe_lt_top hf₁.2⟩ + +lemma HasWeakType.ennreal_toReal {T : (α → ε₁) → (α' → ℝ≥0∞)} (h : HasWeakType T p p' μ ν c) : + HasWeakType (fun u x ↦ T u x |>.toReal) p p' μ ν c := + fun f hf ↦ ⟨(h f hf).1.ennreal_toReal, wnorm_toReal_le.trans (h f hf).2 ⟩ + + +lemma HasStrongType.memℒp (h : HasStrongType T p p' μ ν c) (hf₁ : Memℒp f₁ p μ) : + Memℒp (T f₁) p' ν := + ⟨(h f₁ hf₁).1, h f₁ hf₁ |>.2.trans_lt <| mul_lt_top coe_lt_top hf₁.2⟩ + 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_eLpNorm (h f hf).1 hp').trans (h f hf).2⟩ + fun f hf ↦ ⟨(h f hf).1, wnorm_le_eLpNorm (h f hf).1 hp' |>.trans (h f hf).2⟩ + -lemma HasStrongType.hasBoundedStrongType (h : HasStrongType T p p' μ ν c) : +lemma HasBoundedStrongType.memℒp [Zero ε₁] (h : HasBoundedStrongType T p p' μ ν c) + (hf₁ : Memℒp f₁ p μ) (h2f₁ : eLpNorm f₁ ∞ μ < ∞) (h3f₁ : μ (support f₁) < ∞) : + Memℒp (T f₁) p' ν := + ⟨(h f₁ hf₁ h2f₁ h3f₁).1, h f₁ hf₁ h2f₁ h3f₁ |>.2.trans_lt <| mul_lt_top coe_lt_top hf₁.2⟩ + +lemma HasStrongType.hasBoundedStrongType [Zero ε₁] (h : HasStrongType T p p' μ ν c) : HasBoundedStrongType T p p' μ ν c := fun f hf _ _ ↦ h f hf -lemma HasStrongType.const_smul {𝕜 E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] - {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} {T : (α → E) → (α' → E')} +end ContinuousENorm + +section NormedGroup + +-- todo: generalize various results to ENorm. + +variable {f g : α → ε} +section +variable [ContinuousENorm ε] + +lemma distribution_eq_nnnorm {f : α → E} : distribution f t μ = μ { x | t < ‖f x‖₊ } := rfl + +@[gcongr] +lemma distribution_mono_left (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) : + distribution f t μ ≤ distribution g t μ := by + have h₀ : {x | t < ‖f x‖ₑ} \ {x | t < ‖g x‖ₑ} ⊆ {x | ¬‖f x‖ₑ ≤ ‖g x‖ₑ} := fun x ↦ by + simp_rw [mem_diff, mem_setOf_eq, not_lt, not_le, and_imp] + intro i₁ i₂; simpa using i₂.trans_lt i₁ + calc + _ ≤ μ ({x | t < ‖f x‖ₑ} ∩ {x | t < ‖g x‖ₑ}) + + μ ({x | t < ‖f x‖ₑ} \ {x | t < ‖g x‖ₑ}) := measure_le_inter_add_diff μ _ _ + _ = μ ({x | t < ‖f x‖ₑ} ∩ {x | t < ‖g x‖ₑ}) := by rw [measure_mono_null h₀ h, add_zero] + _ ≤ _ := by apply measure_mono; simp + +@[gcongr] +lemma distribution_mono (h₁ : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) (h₂ : t ≤ s) : + distribution f s μ ≤ distribution g t μ := + (distribution_mono_left h₁).trans (distribution_mono_right h₂) + +lemma distribution_snormEssSup : distribution f (eLpNormEssSup f μ) μ = 0 := + meas_essSup_lt -- meas_eLpNormEssSup_lt + +lemma distribution_smul_left {f : α → E} {c : 𝕜} (hc : c ≠ 0) : + distribution (c • f) t μ = distribution f (t / ‖c‖₊) μ := by + simp_rw [distribution_eq_nnnorm] + have h₀ : ofNNReal ‖c‖₊ ≠ 0 := ENNReal.coe_ne_zero.mpr (nnnorm_ne_zero_iff.mpr hc) + congr with x + simp only [Pi.smul_apply, mem_setOf_eq] + rw [← @ENNReal.mul_lt_mul_right (t / ‖c‖₊) _ (‖c‖₊) h₀ coe_ne_top, + ENNNorm_absolute_homogeneous _, mul_comm, ENNReal.div_mul_cancel h₀ coe_ne_top] + +lemma distribution_add_le' {A : ℝ≥0∞} {g₁ g₂ : α → ε} + (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ A * (‖g₁ x‖ₑ + ‖g₂ x‖ₑ)) : + distribution f (A * (t + s)) μ ≤ distribution g₁ t μ + distribution g₂ s μ := by + apply distribution_add_le_of_enorm + simp (discharger := positivity) [← ofReal_mul, ← ofReal_add, h] + +lemma HasStrongType.const_smul {𝕜 E' α α' : Type*} [NormedAddCommGroup E'] + {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} {T : (α → ε) → (α' → E')} {p p' : ℝ≥0∞} {μ : Measure α} {ν : Measure α'} {c : ℝ≥0} (h : HasStrongType T p p' μ ν c) [NormedRing 𝕜] [MulActionWithZero 𝕜 E'] [BoundedSMul 𝕜 E'] (k : 𝕜) : HasStrongType (k • T) p p' μ ν (‖k‖₊ * c) := by @@ -391,10 +459,100 @@ lemma HasStrongType.const_smul {𝕜 E E' α α' : Type*} [NormedAddCommGroup E] gcongr exact (h f hf).2 -lemma HasStrongType.const_mul {E E' α α' : Type*} [NormedAddCommGroup E] [NormedRing E'] - {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} {T : (α → E) → (α' → E')} {p p' : ℝ≥0∞} +lemma HasStrongType.const_mul {E' α α' : Type*} [NormedRing E'] + {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} {T : (α → ε) → (α' → E')} {p p' : ℝ≥0∞} {μ : Measure α} {ν : Measure α'} {c : ℝ≥0} (h : HasStrongType T p p' μ ν c) (e : E') : HasStrongType (fun f x ↦ e * T f x) p p' μ ν (‖e‖₊ * c) := h.const_smul e +end + +lemma distribution_add_le [ENormedAddMonoid ε] : + distribution (f + g) (t + s) μ ≤ distribution f t μ + distribution g s μ := + calc + _ ≤ μ ({x | t < ↑‖f x‖ₑ} ∪ {x | s < ↑‖g x‖ₑ}) := by + refine measure_mono fun x h ↦ ?_ + simp only [mem_union, mem_setOf_eq, Pi.add_apply] at h ⊢ + contrapose! h + exact (enorm_add_le _ _).trans (add_le_add h.1 h.2) + _ ≤ _ := measure_union_le _ _ + +lemma _root_.ContinuousLinearMap.distribution_le {f : α → E₁} {g : α → E₂} : + distribution (fun x ↦ L (f x) (g x)) (‖L‖₊ * t * s) μ ≤ + distribution f t μ + distribution g s μ := by + unfold distribution + have h₀ : {x | ↑‖L‖₊ * t * s < ↑‖(fun x ↦ (L (f x)) (g x)) x‖₊} ⊆ + {x | t < ↑‖f x‖₊} ∪ {x | s < ↑‖g x‖₊} := fun z hz ↦ by + simp only [mem_union, mem_setOf_eq, Pi.add_apply] at hz ⊢ + contrapose! hz + calc + (‖(L (f z)) (g z)‖₊ : ℝ≥0∞) ≤ ‖L‖₊ * ‖f z‖₊ * ‖g z‖₊ := by + refine (toNNReal_le_toNNReal coe_ne_top coe_ne_top).mp ?_ + simp only [toNNReal_coe, coe_mul, toNNReal_mul] + calc + _ ≤ ↑‖L (f z)‖₊ * ↑‖g z‖₊ := ContinuousLinearMap.le_opNNNorm (L (f z)) (g z) + _ ≤ ‖L‖₊ * ‖f z‖₊ * ‖g z‖₊ := + mul_le_mul' (ContinuousLinearMap.le_opNNNorm L (f z)) (by rfl) + _ ≤ _ := mul_le_mul' (mul_le_mul_left' hz.1 ↑‖L‖₊) hz.2 + calc + _ ≤ μ ({x | t < ↑‖f x‖₊} ∪ {x | s < ↑‖g x‖₊}) := measure_mono h₀ + _ ≤ _ := measure_union_le _ _ + +section BorelSpace + +variable [ContinuousENorm ε] [MeasurableSpace E] [BorelSpace E] + +/-- The layer-cake theorem, or Cavalieri's principle for functions into a normed group. -/ +lemma lintegral_norm_pow_eq_distribution {f : α → E} (hf : AEMeasurable f μ) {p : ℝ} (hp : 0 < p) : + ∫⁻ x, ‖f x‖ₑ ^ p ∂μ = + ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (p * t ^ (p - 1)) * distribution f (.ofReal t) μ := by + have h2p : 0 ≤ p := hp.le + have := lintegral_rpow_eq_lintegral_meas_lt_mul μ (f := fun x ↦ ‖f x‖) + (Eventually.of_forall fun x ↦ norm_nonneg _) hf.norm hp + simp only [enorm_eq_nnnorm, norm_nonneg, ← ofReal_rpow_of_nonneg, mul_comm (μ _), ne_eq, + ofReal_ne_top, not_false_eq_true, ← lintegral_const_mul', ← mul_assoc, + ← ofReal_norm_eq_coe_nnnorm, ofReal_mul, distribution, h2p] at this ⊢ + convert this using 1 + refine setLIntegral_congr_fun measurableSet_Ioi (Eventually.of_forall fun x hx ↦ ?_) + simp_rw [ENNReal.ofReal_lt_ofReal_iff_of_nonneg (le_of_lt hx)] + +/-- The layer-cake theorem, or Cavalieri's principle, written using `eLpNorm`. -/ +lemma eLpNorm_pow_eq_distribution {f : α → E} (hf : AEMeasurable f μ) {p : ℝ≥0} (hp : 0 < p) : + eLpNorm f p μ ^ (p : ℝ) = + ∫⁻ t in Ioi (0 : ℝ), p * ENNReal.ofReal (t ^ ((p : ℝ) - 1)) * distribution f (.ofReal t) μ := by + have h2p : 0 < (p : ℝ) := hp + simp_rw [eLpNorm_nnreal_eq_eLpNorm' hp.ne', eLpNorm', one_div, ← ENNReal.rpow_mul, + inv_mul_cancel₀ h2p.ne', ENNReal.rpow_one, lintegral_norm_pow_eq_distribution hf h2p, + ENNReal.ofReal_mul zero_le_coe, ofReal_coe_nnreal] + +/-- The layer-cake theorem, or Cavalieri's principle, written using `eLpNorm`, without + taking powers. -/ +lemma eLpNorm_eq_distribution {f : α → E} (hf : AEMeasurable f μ) {p : ℝ} (hp : 0 < p) : + eLpNorm f (.ofReal p) μ = + (ENNReal.ofReal p * ∫⁻ t in Ioi (0 : ℝ), distribution f (.ofReal t) μ * + ENNReal.ofReal (t ^ (p - 1)) ) ^ p⁻¹ := by + unfold eLpNorm + split_ifs with sgn_p sz_p + · exact False.elim (not_le_of_lt hp (ofReal_eq_zero.mp sgn_p)) + · exact False.elim (coe_ne_top sz_p) + · unfold eLpNorm' + rw [toReal_ofReal (le_of_lt hp), one_div] + congr 1 + rw [← lintegral_const_mul'] + on_goal 2 => exact coe_ne_top + rw [lintegral_norm_pow_eq_distribution hf hp] + congr 1 with x; rw [ofReal_mul] <;> [ring; positivity] + +lemma lintegral_pow_mul_distribution {f : α → E} (hf : AEMeasurable f μ) {p : ℝ} (hp : -1 < p) : + ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (t ^ p) * distribution f (.ofReal t) μ = + ENNReal.ofReal (p + 1)⁻¹ * ∫⁻ x, ‖f x‖ₑ ^ (p + 1) ∂μ := by + have h2p : 0 < p + 1 := by linarith + have h3p : 0 ≤ p + 1 := by linarith + have h4p : p + 1 ≠ 0 := by linarith + simp [*, lintegral_norm_pow_eq_distribution, ← lintegral_const_mul', ← ofReal_mul, ← mul_assoc] + +end BorelSpace + +end NormedGroup + end MeasureTheory