From b86d9502fba44a8198e65f3bf0900efb8ee3ba22 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 25 Jul 2024 16:12:32 +0200 Subject: [PATCH] Cleanup Add some \leanok's in chapter 11 Move some lemmas from HardyLittlewood to ToMathlib Fix some lemma/section numbers. --- Carleson/Classical/Approximation.lean | 2 +- Carleson/Classical/Basic.lean | 2 +- Carleson/Classical/CarlesonOnTheRealLine.lean | 8 +- .../Classical/ControlApproximationEffect.lean | 6 +- Carleson/Classical/DirichletKernel.lean | 4 +- Carleson/Classical/HilbertKernel.lean | 4 +- Carleson/Classical/VanDerCorput.lean | 2 +- Carleson/DiscreteCarleson.lean | 4 +- Carleson/HardyLittlewood.lean | 56 ++------------ Carleson/ToMathlib/Misc.lean | 73 +++++++++++++++++-- Carleson/WeakType.lean | 1 - blueprint/src/chapter/main.tex | 24 +++++- 12 files changed, 111 insertions(+), 75 deletions(-) diff --git a/Carleson/Classical/Approximation.lean b/Carleson/Classical/Approximation.lean index fb4f7c1e..2fc78fae 100644 --- a/Carleson/Classical/Approximation.lean +++ b/Carleson/Classical/Approximation.lean @@ -1,4 +1,4 @@ -/- The arguments in this file replace section 10.2 (Piecewise constant functions) from the paper. -/ +/- The arguments in this file contains section 11.2 (smooth functions) from the paper. -/ import Carleson.MetricCarleson import Carleson.Classical.Basic diff --git a/Carleson/Classical/Basic.lean b/Carleson/Classical/Basic.lean index a3714559..daa78c63 100644 --- a/Carleson/Classical/Basic.lean +++ b/Carleson/Classical/Basic.lean @@ -190,7 +190,7 @@ lemma lower_secant_bound' {η : ℝ} {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_l · simp [pow_two_nonneg] · linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)] -/-Slightly weaker version of Lemma 10.11 (lower secant bound) with simplified constant. -/ +/-Slightly weaker version of Lemma 11..1.9 (lower secant bound) with simplified constant. -/ lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)) (xAbs : η ≤ |x|) : η / 2 ≤ Complex.abs (1 - Complex.exp (Complex.I * x)) := by by_cases ηpos : η < 0 diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean index 57828af9..227421f1 100644 --- a/Carleson/Classical/CarlesonOnTheRealLine.lean +++ b/Carleson/Classical/CarlesonOnTheRealLine.lean @@ -1,4 +1,4 @@ -/- This file contains the proof of Lemma 10.4, from section 10.7-/ +/- This file contains the proof of Lemma 11.1.4, from section 11.7 -/ import Carleson.MetricCarleson import Carleson.Classical.Basic @@ -434,10 +434,10 @@ instance compatibleFunctions_R : CompatibleFunctions ℝ ℝ (2 ^ 4) where intro x R R' f exact integer_ball_cover.mono_nat (by norm_num) ---TODO : What is Lemma 10.34 (frequency ball growth) needed for? +--TODO : What is Lemma 11.7.10 (frequency ball growth) needed for? instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where - /- Lemma 10.36 (real van der Corput) from the paper. -/ + /- Lemma 11.7.12 (real van der Corput) from the paper. -/ norm_integral_exp_le := by intro x r ϕ K hK _ f g by_cases r_pos : 0 ≥ r @@ -599,7 +599,7 @@ lemma CarlesonOperatorReal_le_CarlesonOperator : T ≤ CarlesonOperator K := by ring_nf -/- Lemma 10.4 (ENNReal version) -/ +/- Lemma 11.1.4 (ENNReal version) -/ lemma rcarleson {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G) (f : ℝ → ℂ) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) diff --git a/Carleson/Classical/ControlApproximationEffect.lean b/Carleson/Classical/ControlApproximationEffect.lean index d3834115..a3d7ef16 100644 --- a/Carleson/Classical/ControlApproximationEffect.lean +++ b/Carleson/Classical/ControlApproximationEffect.lean @@ -1,4 +1,4 @@ -/- This file formalizes section 10.8 (The error bound) from the paper. -/ +/- This file formalizes section 11.6 (The error bound) from the paper. -/ import Carleson.MetricCarleson import Carleson.Classical.Helper import Carleson.Classical.Basic @@ -181,7 +181,7 @@ lemma intervalIntegrable_mul_dirichletKernel'_max' {x : ℝ} (hx : x ∈ Set.Icc lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) : ∫ (y : ℝ) in x - Real.pi..x + Real.pi, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) - = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, + = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by calc _ _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 Real.pi}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by @@ -527,7 +527,7 @@ lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ --TODO: add doc-strings ! -/-ENNReal version of a generalized Lemma 10.3 (control approximation effect).-/ +/-ENNReal version of a generalized Lemma 11.1.3 (control approximation effect).-/ --added subset assumption --changed interval to match the interval in the theorem lemma control_approximation_effect {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real.pi) {δ : ℝ} (hδ : 0 < δ) diff --git a/Carleson/Classical/DirichletKernel.lean b/Carleson/Classical/DirichletKernel.lean index fe9b4e9f..7faa1cc9 100644 --- a/Carleson/Classical/DirichletKernel.lean +++ b/Carleson/Classical/DirichletKernel.lean @@ -57,7 +57,7 @@ lemma dirichletKernel'_periodic {N : ℕ} : Function.Periodic (dirichletKernel' lemma dirichletKernel'_measurable {N : ℕ} : Measurable (dirichletKernel' N) := by apply Measurable.add <;> apply Measurable.div <;> measurability -/-Second part of Lemma 10.10 (Dirichlet kernel) from the paper.-/ +/-Second part of Lemma 11.1.8 (Dirichlet kernel) from the paper.-/ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : dirichletKernel N x = dirichletKernel' N x := by have : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x @@ -167,7 +167,7 @@ lemma norm_dirichletKernel'_le {N : ℕ} {x : ℝ} : ‖dirichletKernel' N x‖ rw [dirichletKernel'_eq_zero h, norm_zero] linarith -/-First part of lemma 10.10 (Dirichlet kernel) from the paper.-/ +/-First part of lemma 11.1.8 (Dirichlet kernel) from the paper.-/ /-TODO (maybe): correct statement so that the integral is taken over the interval [-pi, pi] -/ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) : partialFourierSum f N x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y) := by diff --git a/Carleson/Classical/HilbertKernel.lean b/Carleson/Classical/HilbertKernel.lean index a11fbb42..973b9bf0 100644 --- a/Carleson/Classical/HilbertKernel.lean +++ b/Carleson/Classical/HilbertKernel.lean @@ -32,7 +32,7 @@ def K (x y : ℝ) : ℂ := k (x - y) @[measurability] lemma Hilbert_kernel_measurable : Measurable (Function.uncurry K) := k_measurable.comp measurable_sub -/- Lemma 10.13 (Hilbert kernel bound) -/ +/- Lemma 11.1.11 (Hilbert kernel bound) -/ lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x - y|) := by by_cases h : 0 < |x - y| ∧ |x - y| < 1 · calc ‖K x y‖ @@ -202,7 +202,7 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ · rwa [abs_neg, abs_of_nonneg yy'nonneg.2] · rwa [abs_neg, abs_of_nonneg yy'nonneg.1] -/- Lemma 10.14 (Hilbert kernel regularity) -/ +/- Lemma 11.1.12 (Hilbert kernel regularity) -/ lemma Hilbert_kernel_regularity {x y y' : ℝ} : 2 * |y - y'| ≤ |x - y| → ‖K x y - K x y'‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|) := by rw [K, K] diff --git a/Carleson/Classical/VanDerCorput.lean b/Carleson/Classical/VanDerCorput.lean index f9ee031c..4d49adca 100644 --- a/Carleson/Classical/VanDerCorput.lean +++ b/Carleson/Classical/VanDerCorput.lean @@ -1,4 +1,4 @@ -/- This file formalizes section 10.6 (The proof of the van der Corput Lemma) from the paper. -/ +/- This file formalizes section 11.4 (The proof of the van der Corput Lemma) from the paper. -/ import Carleson.Classical.Basic diff --git a/Carleson/DiscreteCarleson.lean b/Carleson/DiscreteCarleson.lean index 085a8a9a..87de41d8 100644 --- a/Carleson/DiscreteCarleson.lean +++ b/Carleson/DiscreteCarleson.lean @@ -1,7 +1,5 @@ import Carleson.Forest import Carleson.HardyLittlewood --- import Carleson.Proposition2 --- import Carleson.Proposition3 open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology open scoped ENNReal @@ -325,7 +323,7 @@ lemma first_exception' : volume (G₁ : Set X) ≤ 2 ^ (- 5 : ℤ) * volume G := simp only [Finset.mem_image, mem_toFinset, 𝓑] at hz rcases hz with ⟨p, h, rfl⟩ simpa [u, lintegral_indicator, Measure.restrict_apply, measurableSet_F, r, h] using (hr h).2.le - have ineq := measure_biUnion_le_lintegral' (A := defaultA a) 𝓑 K0 hu h2u + have ineq := Finset.measure_biUnion_le_lintegral (A := defaultA a) 𝓑 K0 hu h2u simp only [u, lintegral_indicator, measurableSet_F, Pi.one_apply, lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter, one_mul] at ineq rw [← mul_le_mul_left K0.ne.symm K_ne_top] diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean index ab39f417..0f38005a 100644 --- a/Carleson/HardyLittlewood.lean +++ b/Carleson/HardyLittlewood.lean @@ -30,15 +30,11 @@ M_𝓑 in the blueprint. -/ abbrev MB (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) := maximalFunction μ 𝓑 c r 1 u x -lemma covering_separable_space (X : Type*) [MetricSpace X] [SeparableSpace X] : +lemma covering_separable_space (X : Type*) [PseudoMetricSpace X] [SeparableSpace X] : ∃ C : Set X, C.Countable ∧ ∀ r > 0, ⋃ c ∈ C, ball c r = univ := by - obtain ⟨C, hC, h2C⟩ := exists_countable_dense X - use C, hC - simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball] - intro r hr x - simp_rw [Dense, Metric.mem_closure_iff] at h2C - exact h2C x r hr + simp_rw [← Metric.dense_iff_iUnion_ball, exists_countable_dense] +-- this can be removed next Mathlib bump /-- A slight generalization of Mathlib's version, with 5 replaced by τ. Already PR'd -/ theorem Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall' {α ι} [MetricSpace α] (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) (τ : ℝ) (hτ : 3 < τ) : @@ -80,7 +76,7 @@ theorem Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall' {α ι} proof of `first_exception` in DiscreteCarleson.lean. But everything involved there is finite, so you can prove this with `ℝ≥0` and deal with casting between `ℝ≥0` and `ℝ≥0∞` there, if that turns out to be easier. -/ -theorem measure_biUnion_le_lintegral (h𝓑 : 𝓑.Countable) {l : ℝ≥0∞} (hl : 0 < l) +theorem Set.Countable.measure_biUnion_le_lintegral (h𝓑 : 𝓑.Countable) {l : ℝ≥0∞} (hl : 0 < l) {u : X → ℝ≥0∞} (hu : AEStronglyMeasurable u μ) (R : ℝ) (hR : ∀ a ∈ 𝓑, r a ≤ R) (h2u : ∀ i ∈ 𝓑, l * μ (ball (c i) (r i)) ≤ ∫⁻ x in ball (c i) (r i), u x ∂μ) : @@ -96,56 +92,18 @@ theorem measure_biUnion_le_lintegral (h𝓑 : 𝓑.Countable) {l : ℝ≥0∞} ( _ = A ^ 2 * ∫⁻ x in ⋃ i ∈ B, ball (c i) (r i), u x ∂μ := sorry -- does this exist in Mathlib? _ ≤ A ^ 2 * ∫⁻ x, u x ∂μ := sorry -theorem measure_biUnion_le_lintegral' (𝓑 : Finset ι) {l : ℝ≥0∞} (hl : 0 < l) +protected theorem Finset.measure_biUnion_le_lintegral (𝓑 : Finset ι) {l : ℝ≥0∞} (hl : 0 < l) {u : X → ℝ≥0∞} (hu : AEStronglyMeasurable u μ) (h2u : ∀ i ∈ 𝓑, l * μ (ball (c i) (r i)) ≤ ∫⁻ x in ball (c i) (r i), u x ∂μ) : l * μ (⋃ i ∈ 𝓑, ball (c i) (r i)) ≤ A ^ 2 * ∫⁻ x, u x ∂μ := let ⟨c, hc⟩ := (𝓑.image r).exists_le - measure_biUnion_le_lintegral 𝓑.countable_toSet hl hu c (by simpa using hc) h2u - -attribute [gcongr] Set.indicator_le_indicator mulIndicator_le_mulIndicator_of_subset -attribute [simp] MeasureTheory.laverage_const - - -namespace MeasureTheory -variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} - {F : Type*} [NormedAddCommGroup F] -lemma laverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) : - ⨍⁻ a, f a ∂μ ≤ ⨍⁻ a, g a ∂μ := by - exact lintegral_mono_ae <| h.filter_mono <| Measure.ae_mono' Measure.smul_absolutelyContinuous - -lemma setLAverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) : - ⨍⁻ a in s, f a ∂μ ≤ ⨍⁻ a in s, g a ∂μ := by - refine laverage_mono_ae <| h.filter_mono <| ae_mono Measure.restrict_le_self - -lemma setLaverage_const_le {c : ℝ≥0∞} : ⨍⁻ _x in s, c ∂μ ≤ c := by - simp_rw [setLaverage_eq, lintegral_const, Measure.restrict_apply MeasurableSet.univ, - univ_inter, div_eq_mul_inv, mul_assoc] - conv_rhs => rw [← mul_one c] - gcongr - exact ENNReal.mul_inv_le_one (μ s) - -theorem snormEssSup_lt_top_of_ae_ennnorm_bound {f : α → F} {C : ℝ≥0∞} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) : - snormEssSup f μ ≤ C := - essSup_le_of_ae_le C hfC - -@[simp] -lemma ENNReal.nnorm_toReal {x : ℝ≥0∞} : ‖x.toReal‖₊ = x.toNNReal := by - ext; simp [ENNReal.toReal] - -end MeasureTheory + 𝓑.countable_toSet.measure_biUnion_le_lintegral hl hu c (by simpa using hc) h2u protected theorem MeasureTheory.AEStronglyMeasurable.maximalFunction {p : ℝ} {u : X → E} (hu : AEStronglyMeasurable u μ) (h𝓑 : 𝓑.Countable) : AEStronglyMeasurable (maximalFunction μ 𝓑 c r p u) μ := by sorry -theorem MeasureTheory.AEStronglyMeasurable.ennreal_toReal - {u : X → ℝ≥0∞} (hu : AEStronglyMeasurable u μ) : - AEStronglyMeasurable (fun x ↦ (u x).toReal) μ := by - refine aestronglyMeasurable_iff_aemeasurable.mpr ?_ - exact ENNReal.measurable_toReal.comp_aemeasurable hu.aemeasurable - theorem MeasureTheory.AEStronglyMeasurable.maximalFunction_toReal {p : ℝ} {u : X → E} (hu : AEStronglyMeasurable u μ) (h𝓑 : 𝓑.Countable) : AEStronglyMeasurable (fun x ↦ maximalFunction μ 𝓑 c r p u x |>.toReal) μ := @@ -239,7 +197,7 @@ lemma countable_globalMaximalFunction : (covering_separable_space X).choose ×ˢ (univ : Set ℤ) |>.Countable := (covering_separable_space X).choose_spec.1.prod countable_univ --- prove if needed. Use `MB_le_snormEssSup` +-- prove only if needed. Use `MB_le_snormEssSup` theorem globalMaximalFunction_lt_top {p : ℝ≥0} (hp₁ : 1 ≤ p) {u : X → E} (hu : AEStronglyMeasurable u μ) (hu : IsBounded (range u)) {x : X} : globalMaximalFunction μ p u x < ∞ := by diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index 33fe25a5..52add832 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/Carleson/ToMathlib/Misc.lean @@ -1,5 +1,6 @@ import Mathlib.Analysis.Convex.PartitionOfUnity import Mathlib.Analysis.Calculus.ContDiff.Basic +import Mathlib.MeasureTheory.Integral.Average import Mathlib.MeasureTheory.Integral.Bochner import Mathlib.MeasureTheory.Measure.Haar.OfBasis import Mathlib.Topology.MetricSpace.Holder @@ -14,12 +15,32 @@ import Carleson.ToMathlib.MeasureReal open Function Set open scoped ENNReal + +section Metric + attribute [gcongr] Metric.ball_subset_ball + +lemma Metric.dense_iff_iUnion_ball {X : Type*} [PseudoMetricSpace X] (s : Set X) : + Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ := by + simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, Metric.mem_closure_iff, + forall_comm (α := X)] + +theorem PseudoMetricSpace.dist_eq_of_dist_zero {X : Type*} [PseudoMetricSpace X] (x : X) {y y' : X} + (hyy' : dist y y' = 0) : dist x y = dist x y' := + dist_comm y x ▸ dist_comm y' x ▸ sub_eq_zero.1 (abs_nonpos_iff.1 (hyy' ▸ abs_dist_sub_le y y' x)) + +end Metric + +section Order + lemma IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i := by simp_rw [le_antisymm_iff, h j, true_and] refine ⟨(· (h j)), swap (fun _ ↦ h · |>.trans ·)⟩ +end Order + +section Int theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < z + 1 := by rw_mod_cast [← Int.floor_le_sub_one_iff, add_sub_cancel_right] @@ -39,6 +60,10 @@ theorem Int.Icc_of_eq_sub_1 {a b : ℤ} (h : a = b - 1) : Finset.Icc a b = {a, b · exact Finset.mem_Icc.2 ⟨le_refl t, hab⟩ · rw [Finset.mem_singleton.1 hb]; exact Finset.mem_Icc.2 ⟨hab, le_refl b⟩ +end Int + +section ENNReal + lemma tsum_one_eq' {α : Type*} (s : Set α) : ∑' (_:s), (1 : ℝ≥0∞) = s.encard := by if hfin : s.Finite then have hfin' : Finite s := by exact hfin @@ -80,10 +105,6 @@ lemma ENNReal.tsum_const_eq' {α : Type*} (s : Set α) (c : ℝ≥0∞) : nth_rw 1 [← one_mul c] rw [ENNReal.tsum_mul_right,tsum_one_eq'] -theorem PseudoMetricSpace.dist_eq_of_dist_zero {X : Type*} [PseudoMetricSpace X] (x : X) {y y' : X} - (hyy' : dist y y' = 0) : dist x y = dist x y' := - dist_comm y x ▸ dist_comm y' x ▸ sub_eq_zero.1 (abs_nonpos_iff.1 (hyy' ▸ abs_dist_sub_le y y' x)) - /-! ## `ENNReal` manipulation lemmas -/ lemma ENNReal.sum_geometric_two_pow_toNNReal {k : ℕ} (hk : k > 0) : @@ -110,10 +131,18 @@ lemma ENNReal.sum_geometric_two_pow_neg_two : conv_lhs => enter [1, n, 2]; rw [← Nat.cast_two] rw [ENNReal.sum_geometric_two_pow_toNNReal zero_lt_two]; norm_num -/-! ## Partitioning an interval -/ +end ENNReal + +section Indicator +attribute [gcongr] Set.indicator_le_indicator mulIndicator_le_mulIndicator_of_subset +end Indicator + namespace MeasureTheory +/-! ## Partitioning an interval -/ + + lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc : 0 ≤ c) : ∫⁻ t in Ioc (a * c) (b * c), f t = ∑ l ∈ Finset.Ico a b, ∫⁻ t in Ioc (l * c) ((l + 1 : ℕ) * c), f t := by @@ -132,6 +161,40 @@ lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc end MeasureTheory +namespace MeasureTheory +variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} + {F : Type*} [NormedAddCommGroup F] + +theorem AEStronglyMeasurable.ennreal_toReal {u : α → ℝ≥0∞} (hu : AEStronglyMeasurable u μ) : + AEStronglyMeasurable (fun x ↦ (u x).toReal) μ := by + refine aestronglyMeasurable_iff_aemeasurable.mpr ?_ + exact ENNReal.measurable_toReal.comp_aemeasurable hu.aemeasurable + +lemma laverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) : + ⨍⁻ a, f a ∂μ ≤ ⨍⁻ a, g a ∂μ := by + exact lintegral_mono_ae <| h.filter_mono <| Measure.ae_mono' Measure.smul_absolutelyContinuous + +lemma setLAverage_mono_ae {f g : α → ℝ≥0∞} (h : ∀ᵐ a ∂μ, f a ≤ g a) : + ⨍⁻ a in s, f a ∂μ ≤ ⨍⁻ a in s, g a ∂μ := by + refine laverage_mono_ae <| h.filter_mono <| ae_mono Measure.restrict_le_self + +lemma setLaverage_const_le {c : ℝ≥0∞} : ⨍⁻ _x in s, c ∂μ ≤ c := by + simp_rw [setLaverage_eq, lintegral_const, Measure.restrict_apply MeasurableSet.univ, + univ_inter, div_eq_mul_inv, mul_assoc] + conv_rhs => rw [← mul_one c] + gcongr + exact ENNReal.mul_inv_le_one (μ s) + +theorem snormEssSup_lt_top_of_ae_ennnorm_bound {f : α → F} {C : ℝ≥0∞} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) : + snormEssSup f μ ≤ C := + essSup_le_of_ae_le C hfC + +@[simp] +lemma ENNReal.nnorm_toReal {x : ℝ≥0∞} : ‖x.toReal‖₊ = x.toNNReal := by + ext; simp [ENNReal.toReal] + +end MeasureTheory + /-! ## `EquivalenceOn` -/ /-- An equivalence relation on the set `s`. -/ diff --git a/Carleson/WeakType.lean b/Carleson/WeakType.lean index ef3e07b9..c2d3f589 100644 --- a/Carleson/WeakType.lean +++ b/Carleson/WeakType.lean @@ -310,7 +310,6 @@ def HasBoundedStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAdd ∀ f : α → E, Memℒp f p μ → snorm f ∞ μ < ∞ → μ (support f) < ∞ → AEStronglyMeasurable (T f) ν ∧ snorm (T f) p' ν ≤ c * snorm f p μ - lemma HasStrongType.hasWeakType (hp' : 1 ≤ p') (h : HasStrongType T p p' μ ν c) : HasWeakType T p p' μ ν c := fun f hf ↦ ⟨(h f hf).1, (wnorm_le_snorm (h f hf).1 hp').trans (h f hf).2⟩ diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index ccf4c4fc..cc47ed18 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -6536,7 +6536,7 @@ \chapter{Two-sided Metric Space Carleson} \end{equation} \begin{theorem}[two-sided metric space Carleson] \label{two-sided-metric-space-Carleson} - \uses{metric-space-Carleson,non-tangential-from-simple} + \uses{metric-space-Carleson, nontangential-from-simple} For all integers $a \ge 4$ and real numbers $10$ and every $x\in\R$, \begin{equation} |g(x)|\le \delta \,. @@ -8615,6 +8620,7 @@ \section{The error bound} \end{lemma} \begin{proof} + \leanok Let $x\in [0,2\pi]$ and $N>0$. We have with \Cref{Dirichlet-kernel} \begin{equation*} |S_N g(x)| = \frac{1}{2\pi} \left| \int_0^{2\pi} g(y) K_N(x-y) \, dy\right|\,. @@ -8746,6 +8752,7 @@ \section{The error bound} %fixme: It seems unnecessary to have the extra lemma with this proof that is really only application. \begin{proof}[Proof of \Cref{control-approximation-effect}] +\proves{control-approximation-effect} \leanok \Cref{control-approximation-effect} now follows directly from \Cref{partial-Fourier-sums-of-small} with $\delta:=\epsilon'$. \end{proof} @@ -8765,9 +8772,12 @@ \section{Carleson on the real line} on the real line $\R$. \begin{lemma}[real line metric] \label{real-line-metric} +\leanok +\lean{instProperSpaceReal, locally_compact_of_proper, Real.instCompleteSpace} The space $(\R,\rho)$ is a complete locally compact metric space. \end{lemma} \begin{proof} + \leanok This is part of the Lean library. \end{proof} \begin{lemma}[real line ball] @@ -8791,10 +8801,13 @@ \section{Carleson on the real line} We consider the Lebesgue measure $\mu$ on $\R$. \begin{lemma}[real line measure] \label{real-line-measure} +\leanok +\lean{instIsAddHaarMeasureVolume} The measure $\mu$ is a sigma-finite non-zero Radon-Borel measure on $\R$. \end{lemma} \begin{proof} + \leanok This is part of the Lean library. \end{proof} \begin{lemma}[real line ball measure] @@ -8817,6 +8830,8 @@ \section{Carleson on the real line} \begin{lemma}[real line doubling] \label{real-line-doubling} +\leanok +\lean{MeasureTheory.InnerProductSpace.IsDoubling} \uses{real-line-ball-measure} We have for every $x\in \R$ and $R>0$ \begin{equation} @@ -8826,7 +8841,7 @@ \section{Carleson on the real line} \begin{proof} We have with \Cref{real-line-ball-measure} \begin{equation} - \mu(B(x,2R)=4R=2\mu(B(x,R)\, . + \mu(B(x,2R)=4R=2\mu(B(x,R))\, . \end{equation} This proves the lemma. \end{proof} @@ -8854,10 +8869,12 @@ \section{Carleson on the real line} \begin{lemma}[frequency metric] \label{frequency-metric} + \leanok For every $R > 0$ and $x \in X$, the function $d_{B(x,R)}$ is a metric on $\Mf$. \end{lemma} \begin{proof} + \lean{instFunctionDistancesReal} This follows immediately from the fact that the standard metric on $\mathbb{Z}$ is a metric. \end{proof} @@ -9011,6 +9028,7 @@ \section{Carleson on the real line} \end{equation} \end{lemma} \begin{proof} + \leanok Set $n'=n-m$. Then we have to prove \begin{equation} \label{eq-vdc-cond2}