From b732845afc1e5b076229e060d85d71a47fbf1e48 Mon Sep 17 00:00:00 2001 From: ldiedering <129694072+ldiedering@users.noreply.github.com> Date: Wed, 7 Aug 2024 10:33:08 +0200 Subject: [PATCH 1/2] Added a.e. version of classical Carleson; some cleanup. (#108) Co-authored-by: Floris van Doorn --- Carleson/Classical/Approximation.lean | 69 +------- Carleson/Classical/Basic.lean | 25 +-- Carleson/Classical/CarlesonOnTheRealLine.lean | 100 +++++------ Carleson/Classical/CarlesonOperatorReal.lean | 62 ++++--- Carleson/Classical/ClassicalCarleson.lean | 165 +++++++++++++++++- .../Classical/ControlApproximationEffect.lean | 27 ++- Carleson/Classical/DirichletKernel.lean | 41 ++--- Carleson/Classical/Helper.lean | 24 ++- Carleson/Classical/HilbertKernel.lean | 62 +++---- .../Classical/SpectralProjectionBound.lean | 24 +-- Carleson/MetricCarleson.lean | 5 + blueprint/src/chapter/main.tex | 79 +++++---- 12 files changed, 384 insertions(+), 299 deletions(-) diff --git a/Carleson/Classical/Approximation.lean b/Carleson/Classical/Approximation.lean index 0120841a..be9b7e72 100644 --- a/Carleson/Classical/Approximation.lean +++ b/Carleson/Classical/Approximation.lean @@ -1,4 +1,4 @@ -/- The arguments in this file contains section 11.2 (smooth functions) from the paper. -/ +/- This file contains the arguments from section 11.2 (smooth functions) from the blueprint. -/ import Carleson.MetricCarleson import Carleson.Classical.Basic @@ -14,40 +14,9 @@ noncomputable section open BigOperators open Finset -section -open Metric ---might be generalized ---TODO : choose better name -lemma uniformContinuous_iff_bounded {α : Type*} {β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {b : ℝ} (bpos : b > 0): - UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε := by - rw [Metric.uniformContinuous_iff] - refine ⟨fun h ε εpos ↦ ?_, fun h ε εpos ↦ ?_⟩ - · obtain ⟨δ', δ'pos, hδ'⟩ := h ε εpos - use min δ' (b / 2) - refine ⟨(lt_min δ'pos (by linarith)).gt, ⟨min_lt_of_right_lt (div_two_lt_of_pos bpos), - fun hxy ↦ hδ' (lt_of_lt_of_le hxy (min_le_left δ' (b / 2)))⟩⟩ - · obtain ⟨δ, δpos, _, hδ⟩ := h ε εpos - use δ -end section - local notation "S_" => partialFourierSum -/- TODO: might be generalized. -/ ---TODO: probably not needed here in this form -lemma close_smooth_approx {f : ℝ → ℂ} (unicontf : UniformContinuous f) {ε : ℝ} (εpos : ε > 0): - ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ⊤ f₀ ∧ ∀ x, Complex.abs (f x - f₀ x) ≤ ε := by - obtain ⟨δ, δpos, hδ⟩ := (Metric.uniformContinuous_iff.mp unicontf) ε εpos - let φ : ContDiffBump (0 : ℝ) := ⟨δ/2, δ, by linarith, by linarith⟩ - let f₀ := MeasureTheory.convolution (φ.normed MeasureTheory.volume) f - (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume - refine ⟨f₀, ?_, fun x ↦ ?_⟩ - · exact HasCompactSupport.contDiff_convolution_left _ φ.hasCompactSupport_normed - φ.contDiff_normed unicontf.continuous.locallyIntegrable - · rw [← Complex.dist_eq, dist_comm] - exact ContDiffBump.dist_normed_convolution_le unicontf.continuous.aestronglyMeasurable - fun y hy ↦ (hδ hy).le -/- Slightly different version-/ lemma close_smooth_approx_periodic {f : ℝ → ℂ} (unicontf : UniformContinuous f) (periodicf : f.Periodic (2 * Real.pi)) {ε : ℝ} (εpos : ε > 0): ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ⊤ f₀ ∧ f₀.Periodic (2 * Real.pi) ∧ @@ -59,8 +28,7 @@ lemma close_smooth_approx_periodic {f : ℝ → ℂ} (unicontf : UniformContinuo refine ⟨f₀, ?_, fun x ↦ ?_, fun x ↦ ?_⟩ · exact HasCompactSupport.contDiff_convolution_left _ φ.hasCompactSupport_normed φ.contDiff_normed unicontf.continuous.locallyIntegrable - · /-TODO: improve this. -/ - rw [f₀def, MeasureTheory.convolution, MeasureTheory.convolution] + · rw [f₀def, MeasureTheory.convolution, MeasureTheory.convolution] congr with t congr 1 convert periodicf (x - t) using 2 @@ -69,25 +37,6 @@ lemma close_smooth_approx_periodic {f : ℝ → ℂ} (unicontf : UniformContinuo exact ContDiffBump.dist_normed_convolution_le unicontf.continuous.aestronglyMeasurable fun y hy ↦ (hδ hy).le -/- Inspired by mathlib : NNReal.summable_of_le-/ -lemma Real.summable_of_le {β : Type} {f g : β → ℝ} - (hgpos : 0 ≤ g) (hgf : ∀ (b : β), g b ≤ f b) (summablef : Summable f) : - Summable g := Summable.of_nonneg_of_le hgpos hgf summablef - /- - set g' : β → NNReal := fun b ↦ ⟨g b, hgpos b⟩ with g'def - set f' : β → NNReal := fun b ↦ ⟨f b, (hgpos b).trans (hgf b)⟩ with f'def - have hf'f: f = (fun b ↦ (f' b : ℝ)) := by norm_cast - have hg'g: g = (fun b ↦ (g' b : ℝ)) := by norm_cast - rw [hg'g, NNReal.summable_coe] - have : ∀ b : β, g' b ≤ f' b := by - intro b - rw [f'def, g'def, ←NNReal.coe_le_coe] - simp - exact hgf b - apply NNReal.summable_of_le this - rwa [←NNReal.summable_coe, ←hf'f] - -/ - -- local lemma lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀ i ≠ 0, g i ≤ f i) (summablef : Summable f) : Summable g := by set f' : ℤ → ℝ := fun i ↦ if i = 0 then g i else f i with f'def @@ -98,7 +47,7 @@ lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀ · simp [h] · simp only [h, ↓reduceIte] exact hgf i h - apply Real.summable_of_le hgpos this + apply Summable.of_nonneg_of_le hgpos this let s : Finset ℤ := {0} rw [← s.summable_compl_iff] apply (summable_congr _).mpr (s.summable_compl_iff.mpr summablef) @@ -166,10 +115,9 @@ lemma periodic_deriv {𝕜 : Type} [NontriviallyNormedField 𝕜] {F : Type} [No simp [(periodic_f y).symm] /-TODO: might be generalized. -/ -/-TODO: Assumption periodicf is probably not needed actually. -/ -lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodic (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f): ∃ C, ∀ n ≠ 0, Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / n ^ 2 := by ---#check IsCompact.exists_isMaxOn - --TODO: improve this +/-TODO: The assumption periodicf is probably not needed actually. -/ +lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodic (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f) : + ∃ C, ∀ n ≠ 0, Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / n ^ 2 := by have h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x := by intro x _ rw [hasDerivAt_deriv_iff] @@ -200,7 +148,7 @@ lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodi open Topology Filter /-TODO : Assumptions might be weakened-/ -lemma int_sum_nat {β : Type} [AddCommGroup β] [TopologicalSpace β] [ContinuousAdd β] {f : ℤ → β} {a : β} (hfa : HasSum f a) : +lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [ContinuousAdd β] {f : ℤ → β} {a : β} (hfa : HasSum f a) : Filter.Tendsto (fun N ↦ ∑ n in Icc (-Int.ofNat ↑N) N, f n) Filter.atTop (𝓝 a) := by have := hfa.nat_add_neg.tendsto_sum_nat have := (Filter.Tendsto.add_const (- (f 0))) this @@ -230,10 +178,7 @@ lemma int_sum_nat {β : Type} [AddCommGroup β] [TopologicalSpace β] [Continuou · norm_num linarith ---theorem HasSum.nat_add_neg {f : ℤ → M} (hf : HasSum f m) : --- HasSum (fun n : ℕ ↦ f n + f (-n)) (m + f 0) := by -/-TODO: Weaken statement to pointwise convergence to simplify proof?-/ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodic (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) : ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x - S_ N f x‖ ≤ ε := by have fact_two_pi_pos : Fact (0 < 2 * Real.pi) := by diff --git a/Carleson/Classical/Basic.lean b/Carleson/Classical/Basic.lean index 1a764033..505145e6 100644 --- a/Carleson/Classical/Basic.lean +++ b/Carleson/Classical/Basic.lean @@ -1,30 +1,30 @@ +/- This file contains basic definitions and lemmas. -/ + import Carleson.MetricCarleson import Mathlib.Analysis.Fourier.AddCircle import Mathlib.Analysis.Convex.SpecificFunctions.Deriv import Mathlib.Analysis.Convolution +import Carleson.Classical.Helper + open BigOperators open Finset ---open Complex noncomputable section ---TODO : add reasonable notation ---local notation "S_" => partialFourierSum f ---TODO: use this as base to build on? +def partialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) : ℂ := ∑ n ∈ Icc (-(N : ℤ)) N, + fourierCoeffOn Real.two_pi_pos f n * fourier n (x : AddCircle (2 * Real.pi)) + +--TODO: Add an AddCircle version? /- def AddCircle.partialFourierSum' {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : AddCircle T → ℂ) (x : AddCircle T) : ℂ := ∑ n in Icc (-Int.ofNat ↑N) N, fourierCoeff f n * fourier n x -/ ---TODO: switch N and f -def partialFourierSum (N : ℕ) (f : ℝ → ℂ) : ℝ → ℂ := fun x ↦ ∑ n in Icc (-Int.ofNat ↑N) N, - fourierCoeffOn Real.two_pi_pos f n * fourier n (x : AddCircle (2 * Real.pi)) ---fun x ↦ ∑ n in Icc (-Int.ofNat ↑N) N, fourierCoeffOn Real.two_pi_pos f n * fourier n (x : AddCircle (2 * Real.pi)) - local notation "S_" => partialFourierSum + @[simp] lemma fourierCoeffOn_mul {a b : ℝ} {hab : a < b} {f: ℝ → ℂ} {c : ℂ} {n : ℤ} : fourierCoeffOn hab (fun x ↦ c * f x) n = c * (fourierCoeffOn hab f n):= by @@ -77,13 +77,6 @@ lemma fourier_periodic {n : ℤ} : lemma partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} : (S_ N f).Periodic (2 * Real.pi) := by simp [Function.Periodic, partialFourierSum, fourier_periodic] -/-Adapted from mathlib Function.Periodic.exists_mem_Ico₀-/ -theorem Function.Periodic.exists_mem_Ico₀' {α : Type} {β : Type} {f : α → β} {c : α} - [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x : α) : ∃ (n : ℤ), (x - n • c) ∈ Set.Ico 0 c ∧ f x = f (x - n • c) := - let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x - ⟨n, H, (h.sub_zsmul_eq n).symm⟩ - - --TODO: maybe generalize to (hc : ContinuousOn f (Set.Icc 0 T)) and leave out condition (hT : 0 < T) lemma Function.Periodic.uniformContinuous_of_continuous {f : ℝ → ℂ} {T : ℝ} (hT : 0 < T) (hp : Function.Periodic f T) (hc : ContinuousOn f (Set.Icc (-T) (2 * T))) : UniformContinuous f := by have : IsCompact (Set.Icc (-T) (2 * T)) := isCompact_Icc diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean index 928c7ee0..291d5ebb 100644 --- a/Carleson/Classical/CarlesonOnTheRealLine.lean +++ b/Carleson/Classical/CarlesonOnTheRealLine.lean @@ -1,4 +1,7 @@ -/- This file contains the proof of Lemma 11.1.4, from section 11.7 -/ +/- This file contains the proof of Lemma 11.1.4 (real Carleson), from section 11.7. + We need to verify the assumptions of the two-sided metric Carleson theorem. + All smaller ones are done but the estimate for the truncated Hilbert transform is still missing. +-/ import Carleson.TwoSidedMetricCarleson import Carleson.Classical.Basic @@ -36,7 +39,7 @@ lemma localOscillation_on_empty_ball {X : Type} [PseudoMetricSpace X] {x : X} {f section -open ENNReal +open ENNReal MeasureTheory section @@ -48,13 +51,9 @@ local notation "θ" => integer_linear local notation "Θ" => {(θ n) | n : ℤ} -/-Stronger version of oscillation_control from the paper-/ -/-Based on earlier version of the paper. -/ -/- - -theorem localOscillation_of_same {X : Type} [PseudoMetricSpace X] {E : Set X} {f : C(X, ℝ)} : - localOscillation E f f = 0 := by simp [localOscillation] +/- +/-Stronger version of oscillation_control based on earlier version of the blueprint -/ lemma localOscillation_of_integer_linear {x R : ℝ} (R_nonneg : 0 ≤ R) : ∀ n m : ℤ, localOscillation (Metric.ball x R) (θ n) (θ m) = 2 * R * |(n : ℝ) - m| := by intro n m by_cases n_ne_m : n = m @@ -169,8 +168,11 @@ instance instFunctionDistancesReal : FunctionDistances ℝ ℝ where edist_dist := fun x y ↦ rfl } ---TODO: add lemma to avoid unfolds. ---lemma dist_eq_ + +lemma dist_integer_linear_eq {n m : Θ ℝ} {x R : ℝ} : dist_{x, R} n m = 2 * max R 0 * |(n : ℝ) - m| := by + unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance + FunctionDistances.metric instFunctionDistancesReal integer_linear + norm_cast lemma coeΘ_R (n : Θ ℝ) (x : ℝ) : n x = n * x := rfl lemma coeΘ_R_C (n : Θ ℝ) (x : ℝ) : (n x : ℂ) = n * x := by norm_cast @@ -182,9 +184,7 @@ lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} : unfold localOscillation simp [dist_nonneg] push_neg at r_pos - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - localOscillation integer_linear - dsimp + rw [dist_integer_linear_eq] calc ⨆ z ∈ ball x r ×ˢ ball x r, |↑f * z.1 - ↑g * z.1 - ↑f * z.2 + ↑g * z.2| _ = ⨆ z ∈ ball x r ×ˢ ball x r, ‖(f - g) * (z.1 - x) - (f - g) * (z.2 - x)‖ := by congr @@ -216,11 +216,9 @@ lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} : _ ≤ 2 * max r 0 * |↑f - ↑g| := by gcongr apply le_max_left - norm_cast lemma frequency_monotone {x₁ x₂ r R : ℝ} {f g : Θ ℝ} (h : ball x₁ r ⊆ ball x₂ R) : dist_{x₁,r} f g ≤ dist_{x₂,R} f g := by - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp + rw [dist_integer_linear_eq, dist_integer_linear_eq] by_cases r_pos : r ≤ 0 . rw [ball_eq_empty.mpr r_pos] at h rw [max_eq_right r_pos] @@ -232,8 +230,7 @@ lemma frequency_monotone {x₁ x₂ r R : ℝ} {f g : Θ ℝ} (h : ball x₁ r linarith [h.1, h.2] lemma frequency_ball_doubling {x₁ x₂ r : ℝ} {f g : Θ ℝ} : dist_{x₂, 2 * r} f g ≤ 2 * dist_{x₁, r} f g := by - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal Real.pseudoMetricSpace - dsimp + rw [dist_integer_linear_eq, dist_integer_linear_eq] by_cases r_nonneg : r ≥ 0 . rw [max_eq_left, max_eq_left] ring_nf;rfl @@ -243,8 +240,7 @@ lemma frequency_ball_doubling {x₁ x₂ r : ℝ} {f g : Θ ℝ} : dist_{x₂, 2 all_goals linarith [r_nonneg] theorem frequency_ball_growth {x₁ x₂ r : ℝ} {f g : Θ ℝ} : 2 * dist_{x₁, r} f g ≤ dist_{x₂, 2 * r} f g := by - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp + rw [dist_integer_linear_eq, dist_integer_linear_eq] by_cases r_nonneg : r ≥ 0 . rw [max_eq_left, max_eq_left] ring_nf;rfl @@ -277,8 +273,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}: constructor . simp simp only [Set.mem_univ, mem_ball, true_implies] - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp + rw [dist_integer_linear_eq] convert R'pos simp left @@ -306,10 +301,9 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}: constructor · rw [balls_def] simp - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp - calc 2 * max R 0 * |↑φ - m₁| - _ = 2 * R * |↑φ - m₁| := by + rw [dist_integer_linear_eq] + calc 2 * max R 0 * |↑φ - ↑m₁| + _ = 2 * R * |↑φ - ↑m₁| := by congr rw [max_eq_left_iff] exact Rpos.le @@ -336,9 +330,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}: apply le_abs_self _ < 2 * R' := by convert hφ - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp - norm_cast + rw [dist_integer_linear_eq] congr symm rw [max_eq_left_iff] @@ -351,9 +343,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}: · rw [balls_def] simp rw [m₂def, dist_comm] - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp - push_cast + rw [dist_integer_linear_eq] calc 2 * max R 0 * |↑f - ↑φ| _ = 2 * R * |↑f - ↑φ| := by congr @@ -368,9 +358,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}: use m₃ constructor . simp [balls_def] - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp - push_cast + rw [dist_integer_linear_eq] calc 2 * max R 0 * |↑φ - ↑m₃| _ = 2 * R * (↑φ - ↑m₃) := by rw [abs_of_nonneg] @@ -391,9 +379,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}: exact abs_sub_comm _ _ _ < 2 * R' := by convert hφ - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp - norm_cast + rw [dist_integer_linear_eq] congr symm rw [max_eq_left_iff] @@ -409,7 +395,6 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}: _ = R' := by ring ---TODO: Some of the statements are stronger in the paper. Extract these instance compatibleFunctions_R : CompatibleFunctions ℝ ℝ (2 ^ 4) where eq_zero := by use 0 @@ -424,17 +409,15 @@ instance compatibleFunctions_R : CompatibleFunctions ℝ ℝ (2 ^ 4) where le_cdist := by intro x₁ x₂ r f g _ apply le_trans (@frequency_ball_growth x₁ x₂ r _ _) - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric instFunctionDistancesReal - dsimp + rw [dist_integer_linear_eq, dist_integer_linear_eq] by_cases r_nonneg : 0 ≤ r . gcongr; norm_num . push_neg at r_nonneg - rw [max_eq_right (by linarith), max_eq_right (by linarith)] + rw [max_eq_right (by linarith), max_eq_right (by norm_num; linarith)] ballsCoverBalls := by intro x R R' f exact integer_ball_cover.mono_nat (by norm_num) ---TODO : What is Lemma 11.7.10 (frequency ball growth) needed for? instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where /- Lemma 11.7.12 (real van der Corput) from the paper. -/ @@ -444,12 +427,9 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where . rw [ball_eq_empty.mpr r_pos] simp push_neg at r_pos - rw [defaultτ, ← one_div, measureReal_def, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [r_pos]), Real.ball_eq_Ioo, ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by linarith [r_pos])] - unfold dist PseudoMetricSpace.toDist instPseudoMetricSpaceWithFunctionDistance FunctionDistances.metric CompatibleFunctions.toFunctionDistances compatibleFunctions_R - dsimp only - unfold instFunctionDistancesReal - dsimp only - rw [max_eq_left r_pos.le] + rw [defaultτ, ← one_div, measureReal_def, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [r_pos]), + Real.ball_eq_Ioo, ← integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le (by linarith [r_pos]), + dist_integer_linear_eq, max_eq_left r_pos.le] set L : NNReal := ⟨⨆ (x : ℝ) (y : ℝ) (_ : x ≠ y), ‖ϕ x - ϕ y‖ / dist x y, Real.iSup_nonneg fun x ↦ Real.iSup_nonneg fun y ↦ Real.iSup_nonneg @@ -475,7 +455,6 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where . rw [hxy] simp rw [dist_eq_norm, ← div_le_iff (dist_pos.mpr hxy), Ldef, NNReal.coe_mk] - --apply ConditionallyCompleteLattice.le_csSup apply le_ciSup_of_le _ x apply le_ciSup_of_le _ y apply le_ciSup_of_le _ hxy @@ -532,12 +511,11 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where apply Real.rpow_le_rpow_of_exponent_le _ (by norm_num) simp only [Int.cast_abs, Int.cast_sub, le_add_iff_nonneg_right] exact mul_nonneg (by linarith) (abs_nonneg _) + norm_cast ---TODO : add some Real.vol lemma - lemma Real.vol_real_eq {x y : ℝ} : Real.vol x y = 2 * |x - y| := by - rw [Real.vol, MeasureTheory.measureReal_def, Real.dist_eq, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [abs_nonneg (x-y)])] + rw [Real.vol, measureReal_def, Real.dist_eq, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [abs_nonneg (x-y)])] lemma Real.vol_real_symm {x y : ℝ} : Real.vol x y = Real.vol y x := by rw [Real.vol_real_eq, Real.vol_real_eq, abs_sub_comm] @@ -546,7 +524,7 @@ instance isOneSidedKernelHilbert : IsOneSidedKernel 4 K where /- uses Hilbert_kernel_bound -/ norm_K_le_vol_inv := by intro x y - rw [Complex.norm_eq_abs, Real.vol, MeasureTheory.measureReal_def, Real.dist_eq, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [abs_nonneg (x-y)])] + rw [Complex.norm_eq_abs, Real.vol, measureReal_def, Real.dist_eq, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [abs_nonneg (x-y)])] calc Complex.abs (K x y) _ ≤ 2 ^ (2 : ℝ) / (2 * |x - y|) := Hilbert_kernel_bound _ ≤ 2 ^ (4 : ℝ) ^ 3 / (2 * |x - y|) := by gcongr <;> norm_num @@ -574,9 +552,7 @@ instance isOneSidedKernelHilbert : IsOneSidedKernel 4 K where · norm_num · norm_num · norm_num - /- Lemma ?-/ measurable_K_left := fun y ↦ Hilbert_kernel_measurable.of_uncurry_right - /- Lemma ?-/ measurable_K_right := Hilbert_kernel_measurable instance isTwoSidedKernelHilbert : IsTwoSidedKernel 4 K where @@ -586,6 +562,10 @@ instance isTwoSidedKernelHilbert : IsTwoSidedKernel 4 K where rw [dist_comm x y] at h exact isOneSidedKernelHilbert.norm_K_sub_le h + +/- This verifies the assumption on the operators T_r in two-sided metric space Carleson. + Its proof is done in Section 11.3 (The truncated Hilbert transform) and is yet to be formalized. +-/ lemma Hilbert_strong_2_2 : ∀ r > 0, HasBoundedStrongType (CZOperator K r) 2 2 volume volume (C_Ts 4) := sorry @@ -611,11 +591,9 @@ lemma CarlesonOperatorReal_le_CarlesonOperator : T ≤ CarlesonOperator K := by ring_nf -/- Lemma 11.1.4 (ENNReal version) -/ -lemma rcarleson {F G : Set ℝ} - (hF : MeasurableSet F) (hG : MeasurableSet G) - (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) - : +/- Lemma 11.1.4 -/ +lemma rcarleson {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G) + (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) : ∫⁻ x in G, T f x ≤ ENNReal.ofReal (C10_0_1 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ := by have conj_exponents : Real.IsConjExponent 2 2 := by rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num diff --git a/Carleson/Classical/CarlesonOperatorReal.lean b/Carleson/Classical/CarlesonOperatorReal.lean index 0162849f..c3eb8195 100644 --- a/Carleson/Classical/CarlesonOperatorReal.lean +++ b/Carleson/Classical/CarlesonOperatorReal.lean @@ -1,3 +1,6 @@ +/- This file contains the definition and basic properties of the Carleson operator on the real line. +-/ + import Carleson.Classical.HilbertKernel noncomputable section @@ -47,16 +50,16 @@ lemma sup_eq_sup_dense_of_continuous {f : ℝ → ENNReal} {S : Set ℝ} (D : Se rw [Set.mem_inter_iff, Set.mem_inter_iff, Set.mem_preimage, Set.mem_Ioi] at hy exact hy.1.2.le.trans (le_biSup _ ⟨hy.1.1, hy.2⟩) -lemma helper {n : ℤ} {f : ℝ → ℂ} (hf : Measurable f) : +lemma measurable_mul_kernel {n : ℤ} {f : ℝ → ℂ} (hf : Measurable f) : Measurable (Function.uncurry fun x y ↦ f y * K x y * (Complex.I * n * y).exp) := ((hf.comp measurable_snd).mul Hilbert_kernel_measurable).mul (measurable_const.mul (Complex.measurable_ofReal.comp measurable_snd)).cexp + local notation "T" => CarlesonOperatorReal K lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurable f) {B : ℝ} (f_bounded : ∀ x, ‖f x‖ ≤ B) : Measurable (T f):= by - --TODO: clean up proof apply measurable_iSup intro n set F : ℝ → ℝ → ℝ → ℂ := fun x r y ↦ {y | dist x y ∈ Set.Ioo r 1}.indicator (fun t ↦ f t * K x t * (Complex.I * ↑n * ↑t).exp) y with Fdef @@ -106,7 +109,8 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab . rw [Sdef] constructor <;> linarith [hr.1] apply MeasureTheory.continuousAt_of_dominated _ h_bound - . have F_bound_on_set : ∀ a ∈ {y | dist x y ∈ Set.Ioo (r / 2) 1}, ‖f a * K x a * (Complex.I * ↑n * ↑a).exp‖ ≤ B * ‖2 ^ (2 : ℝ) / (2 * (r / 2))‖ := by + . have F_bound_on_set : ∀ a ∈ {y | dist x y ∈ Set.Ioo (r / 2) 1}, + ‖f a * K x a * (Complex.I * ↑n * ↑a).exp‖ ≤ B * ‖2 ^ (2 : ℝ) / (2 * (r / 2))‖ := by intro a ha rw [norm_mul, norm_mul, mul_assoc Complex.I, mul_comm Complex.I] norm_cast @@ -130,8 +134,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab apply MeasureTheory.Measure.integrableOn_of_bounded . rw [annulus_real_volume (by constructor <;> linarith [hr.1, hr.2])] exact ENNReal.ofReal_ne_top - . --measurability - apply ((Measurable.of_uncurry_left (helper f_measurable)).norm).aestronglyMeasurable + . apply ((Measurable.of_uncurry_left (measurable_mul_kernel f_measurable)).norm).aestronglyMeasurable . --interesting part rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet] simp_rw [norm_norm] @@ -200,7 +203,7 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab rw [MeasureTheory.ae_iff] exact MeasureTheory.measure_mono_null subset_finite (Finset.measure_zero _ _) . exact Filter.eventually_of_forall fun r ↦ ((Measurable.of_uncurry_left - (helper f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable + (measurable_mul_kernel f_measurable)).indicator annulus_measurableSet).aestronglyMeasurable rw [this] apply measurable_biSup _ . apply Set.Countable.mono Set.inter_subset_right hQ.2 @@ -209,7 +212,31 @@ lemma CarlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab rw [← stronglyMeasurable_iff_measurable] apply MeasureTheory.StronglyMeasurable.integral_prod_right rw [stronglyMeasurable_iff_measurable, Fdef] - exact (helper f_measurable).indicator (measurable_dist measurableSet_Ioo) + exact (measurable_mul_kernel f_measurable).indicator (measurable_dist measurableSet_Ioo) + +--TODO: Refactor the measurability proof to use the following. + +/- +import Mathlib.MeasureTheory.Measure.MeasureSpace +import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic + +open TopologicalSpace MeasureTheory Set + +variable {α β : Type*} [MeasurableSpace α] + [MeasurableSpace β] + {ι : Type*} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [SecondCountableTopology ι] + {f : ι → α → β} [ConditionallyCompleteLattice β] + [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] + [BorelSpace β] + +lemma Measurable_iSup_gt {s : Set ι} [OrdConnected s] + (h1f : ∀ x i, ContinuousWithinAt (f · x) s i) + (h2f : ∀ i, Measurable (f i)) : + Measurable (⨆ i ∈ s, f i ·) := sorry + -- use SecondCountableTopology to rewrite the sup as a sup over the countable dense set (or similar) + -- then use measurable_iSup +-/ + lemma CarlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a) : T f x = a.toNNReal * T (fun x ↦ 1 / a * f x) x := by rw [CarlesonOperatorReal, CarlesonOperatorReal, ENNReal.mul_iSup] @@ -252,24 +279,3 @@ lemma CarlesonOperatorReal_eq_of_restrict_interval {f : ℝ → ℂ} {a b : ℝ} rcases hy with hy | hy . left; linarith [hx.1] . right; linarith [hx.2] - -/- -import Mathlib.MeasureTheory.Measure.MeasureSpace -import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic - -open TopologicalSpace MeasureTheory Set - -variable {α β : Type*} [MeasurableSpace α] - [MeasurableSpace β] - {ι : Type*} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [SecondCountableTopology ι] - {f : ι → α → β} [ConditionallyCompleteLattice β] - [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] - [BorelSpace β] - -lemma Measurable_iSup_gt {s : Set ι} [OrdConnected s] - (h1f : ∀ x i, ContinuousWithinAt (f · x) s i) - (h2f : ∀ i, Measurable (f i)) : - Measurable (⨆ i ∈ s, f i ·) := sorry - -- use SecondCountableTopology to rewrite the sup as a sup over the countable dense set (or similar) - -- then use measurable_iSup --/ diff --git a/Carleson/Classical/ClassicalCarleson.lean b/Carleson/Classical/ClassicalCarleson.lean index 050f747f..d2d509fd 100644 --- a/Carleson/Classical/ClassicalCarleson.lean +++ b/Carleson/Classical/ClassicalCarleson.lean @@ -1,3 +1,5 @@ +/- This file contains the proof of the classical Carleson theorem from Section 11.1. -/ + import Carleson.MetricCarleson import Carleson.Classical.Basic import Carleson.Classical.Approximation @@ -5,6 +7,7 @@ import Carleson.Classical.ControlApproximationEffect import Mathlib.Analysis.Fourier.AddCircle +open MeasureTheory noncomputable section @@ -14,14 +17,13 @@ local notation "S_" => partialFourierSum theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * Real.pi)) {ε : ℝ} (εpos : 0 < ε) : - ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ MeasureTheory.volume.real E ≤ ε ∧ + ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ volume.real E ≤ ε ∧ ∃ N₀, ∀ x ∈ (Set.Icc 0 (2 * Real.pi)) \ E, ∀ N > N₀, ‖f x - S_ N f x‖ ≤ ε := by - --rcases hε with ⟨εpos, εle⟩ set ε' := ε / 4 / C_control_approximation_effect ε with ε'def have ε'pos : ε' > 0 := div_pos (div_pos εpos (by norm_num)) (C_control_approximation_effect_pos εpos) - -- Approximation + /- Approximate f by a smooth f₀. -/ have unicont_f : UniformContinuous f := periodic_f.uniformContinuous_of_continuous Real.two_pi_pos cont_f.continuousOn obtain ⟨f₀, contDiff_f₀, periodic_f₀, hf₀⟩ := close_smooth_approx_periodic unicont_f periodic_f ε'pos have ε4pos : ε / 4 > 0 := by linarith @@ -36,10 +38,10 @@ theorem classical_carleson {f : ℝ → ℂ} rw [← Complex.dist_eq, dist_comm, Complex.dist_eq] exact hf₀ x - -- Control approximation effect + /- Control approximation effect: Get a bound on the partial Fourier sums of h. -/ obtain ⟨E, Esubset, Emeasurable, Evolume, hE⟩ := control_approximation_effect εpos ε'pos h_measurable h_periodic h_bound - -- "epsilon third" argument + /- This is a classical "epsilon third" argument. -/ use E, Esubset, Emeasurable, Evolume, N₀ intro x hx N NgtN₀ calc ‖f x - S_ N f x‖ @@ -64,3 +66,156 @@ theorem classical_carleson {f : ℝ → ℂ} rw [← div_le_iff' (by norm_num)] exact le_trans' (lt_C_control_approximation_effect εpos).le (by linarith [Real.two_le_pi]) _ ≤ ε := by linarith + + + +theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * Real.pi)) : + ∀ᵐ x ∂volume.restrict (Set.Icc 0 (2 * Real.pi)), + Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by + + let δ (k : ℕ) : ℝ := 1 / (k + 1) --arbitrary sequence tending to zero + have δconv : Filter.Tendsto δ Filter.atTop (nhds 0) := tendsto_one_div_add_atTop_nhds_zero_nat + have δpos (k : ℕ) : 0 < δ k := by apply div_pos zero_lt_one (by linarith) + + -- ENNReal version to be comparable to volumes + let δ' (k : ℕ) := ENNReal.ofReal (δ k) + have δ'conv : Filter.Tendsto δ' Filter.atTop (nhds 0) := by + rw [← ENNReal.ofReal_zero] + exact ENNReal.tendsto_ofReal δconv + + set ε := fun k n ↦ (1 / 2) ^ n * 2⁻¹ * δ k with εdef + have εpos (k n : ℕ) : 0 < ε k n := by positivity + have εsmall (k : ℕ) {e : ℝ} (epos : 0 < e) : ∃ n, ε k n < e := by + have : Filter.Tendsto (ε k) Filter.atTop (nhds 0) := by + rw [εdef] + simp_rw [mul_assoc] + rw [← zero_mul (2⁻¹ * δ k)] + apply Filter.Tendsto.mul_const + exact tendsto_pow_atTop_nhds_zero_of_lt_one (by linarith) (by linarith) + rw [Metric.tendsto_atTop] at this + rcases (this e epos) with ⟨n, hn⟩ + use n + convert (hn n (by simp)) + simp_rw [dist_zero_right, Real.norm_eq_abs, abs_of_nonneg (εpos k n).le] + + have δ'_eq {k : ℕ} : δ' k = ∑' n, ENNReal.ofReal (ε k n) := by + rw [εdef] + conv => rhs; pattern ENNReal.ofReal _; rw [ENNReal.ofReal_mul' (δpos k).le, ENNReal.ofReal_mul' (by norm_num), ENNReal.ofReal_pow (by norm_num)] + rw [ENNReal.tsum_mul_right, ENNReal.tsum_mul_right, ENNReal.tsum_geometric, ← ENNReal.ofReal_one, + ← ENNReal.ofReal_sub, ← ENNReal.ofReal_inv_of_pos (by norm_num), ← ENNReal.ofReal_mul' (by norm_num)] + conv => pattern ENNReal.ofReal _; ring_nf; rw [ENNReal.ofReal_one] + rw [one_mul] + norm_num + + -- Main step: Apply classical_carleson to get a family of exceptional sets parameterized by ε. + choose Eε hEε_subset _ hEε_measure hEε using (@classical_carleson f cont_f periodic_f) + + have Eεmeasure {ε : ℝ} (hε : 0 < ε) : volume (Eε hε) ≤ ENNReal.ofReal ε := by + rw [ENNReal.le_ofReal_iff_toReal_le _ hε.le] + . exact hEε_measure hε + . rw [← lt_top_iff_ne_top] + apply lt_of_le_of_lt (measure_mono (hEε_subset hε)) measure_Icc_lt_top + + -- Define exceptional sets parameterized by δ. + let Eδ (k : ℕ) := ⋃ (n : ℕ), Eε (εpos k n) + have Eδmeasure (k : ℕ) : volume (Eδ k) ≤ δ' k := by + apply le_trans (measure_iUnion_le _) + rw [δ'_eq] + exact ENNReal.tsum_le_tsum (fun n ↦ Eεmeasure (εpos k n)) + + -- Define final exceptional set. + let E := ⋂ (k : ℕ), Eδ k + + -- Show that it has the desired property. + have hE : ∀ x ∈ (Set.Icc 0 (2 * Real.pi)) \ E, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by + intro x hx + rw [Set.diff_iInter, Set.mem_iUnion] at hx + rcases hx with ⟨k,hk⟩ + rw [Set.diff_iUnion, Set.mem_iInter] at hk + + rw [Metric.tendsto_atTop'] + intro e epos + rcases (εsmall k epos) with ⟨n, lt_e⟩ + + rcases (hEε (εpos k n)) with ⟨N₀,hN₀⟩ + use N₀ + intro N hN + rw [dist_comm, dist_eq_norm] + exact (hN₀ x (hk n) N hN).trans_lt lt_e + + -- Show that is has measure zero. + have Emeasure : volume E ≤ 0 := by + have : ∀ k, volume E ≤ δ' k := by + intro k + apply le_trans' (Eδmeasure k) + apply measure_mono + apply Set.iInter_subset + exact ge_of_tendsto' δ'conv this + + -- Use results to prove the statement. + rw [ae_restrict_iff' measurableSet_Icc] + apply le_antisymm _ (zero_le _) + apply le_trans' Emeasure + apply measure_mono + intro x hx + simp only [and_imp, Set.mem_compl_iff, Set.mem_setOf_eq, Classical.not_imp] at hx + by_contra h + exact hx.2 (hE x ⟨hx.1, h⟩) + + + +section +open Pointwise + +--TODO: might be generalized +lemma Function.Periodic.ae_of_ae_restrict {T : ℝ} (hT : 0 < T) {a : ℝ} {P : (x : ℝ) → Prop} (hP : Function.Periodic P T) + (h : ∀ᵐ x ∂volume.restrict (Set.Ico a (a + T)), P x) : + ∀ᵐ x, P x := by + rw [ae_restrict_iff' measurableSet_Ico, ae_iff] at h + set E_interval := {x | ¬(x ∈ Set.Ico a (a + T) → P x)} with E_interval_def + -- Define exceptional set as countable union of translations of the exceptional set on the interval + set E := ⋃ (k : ℤ), k • T +ᵥ E_interval with Edef + + have hE : E = {a | ¬P a} := by + ext x + rw [Set.mem_iUnion] + constructor + . intro h + rcases h with ⟨k, hk⟩ + rw [Set.mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, ← sub_eq_neg_add, E_interval_def] at hk + simp only [and_imp, Classical.not_imp, Set.mem_setOf_eq, hP.sub_zsmul_eq k] at hk + exact hk.2 + . dsimp + rcases (hP.exists_mem_Ico' hT x a) with ⟨n, hn, hxn⟩ + rw [hxn] + intro h + use n + rw [Set.mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, ← sub_eq_neg_add, E_interval_def] + simp only [and_imp, Classical.not_imp, Set.mem_setOf_eq] + exact ⟨hn, h⟩ + + -- The union still has measure zero + have Emeasure : volume E = 0 := by + rw [Edef, measure_iUnion_null] + intro k + apply measure_vadd_null h + + rw [ae_iff, ← hE] + exact Emeasure + +end section + +/- Carleson's theorem asserting a.e. convergence of the partial Fourier sums for continous functions. -/ +theorem carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * Real.pi)) : + ∀ᵐ x, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by + -- Reduce to a.e. convergence on [0,2π] + apply @Function.Periodic.ae_of_ae_restrict _ Real.two_pi_pos 0 + . rw [Function.Periodic] + intro x + conv => pattern S_ _ _ _; rw [partialFourierSum_periodic] + conv => pattern f _; rw [periodic_f] + apply MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict MeasureTheory.Ico_ae_eq_Icc.symm + rw [zero_add] + + -- Show a.e. convergence on [0,2π] + exact carleson_interval cont_f periodic_f diff --git a/Carleson/Classical/ControlApproximationEffect.lean b/Carleson/Classical/ControlApproximationEffect.lean index e80468f8..135618e5 100644 --- a/Carleson/Classical/ControlApproximationEffect.lean +++ b/Carleson/Classical/ControlApproximationEffect.lean @@ -1,4 +1,6 @@ -/- This file formalizes section 11.6 (The error bound) from the paper. -/ +/- This file contains most of Section 11.6 (The error bound) from the blueprint. + The main result is control_approximation_effect. +-/ import Carleson.MetricCarleson import Carleson.Classical.Helper import Carleson.Classical.Basic @@ -136,7 +138,6 @@ lemma Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-Real.pi) section open Filter Topology ---TODO: proof might be improved lemma le_iSup_of_tendsto {α β} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (ha : Tendsto f atTop (𝓝 a)) : a ≤ iSup f := by apply le_of_forall_lt @@ -232,7 +233,6 @@ lemma intervalIntegrable_mul_dirichletKernel'_specific {x : ℝ} (hx : x ∈ Set lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) : - --‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤ T f x + T (conj ∘ f) x := by ‖∫ (y : ℝ) in x - Real.pi..x + Real.pi, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊ ≤ T g x + T (conj ∘ g) x := by rw [domain_reformulation hg hx] @@ -258,7 +258,8 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g Measu refine ⟨lt_trans' hn.1 ?_, hn.2⟩ norm_num linarith - have : Tendsto (fun i => ∫ y in s i, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) atTop (𝓝 (∫ y in ⋃ n, s n, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) := by + have : Tendsto (fun i => ∫ y in s i, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) + atTop (𝓝 (∫ y in ⋃ n, s n, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) := by apply MeasureTheory.tendsto_setIntegral_of_monotone · intro n exact annulus_measurableSet @@ -387,11 +388,14 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu (periodic_g : Function.Periodic g (2 * Real.pi)) (bound_g : ∀ x, ‖g x‖ ≤ δ) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) : ‖S_ N g x‖₊ - ≤ (T g x + T (conj ∘ g) x) / (ENNReal.ofReal (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ) := by + ≤ (T g x + T (conj ∘ g) x) / (ENNReal.ofReal (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ) := by have intervalIntegrable_g : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi) := intervalIntegrable_of_bdd measurable_g bound_g have decomposition : S_ N g x - = ( (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) - + (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) / (2 * Real.pi) := by + = ( (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), + g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) + + (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), + g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) + / (2 * Real.pi) := by calc S_ N g x _ = (∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), g y * dirichletKernel' N (x - y)) / (2 * Real.pi) := by rw [partialFourierSum_eq_conv_dirichletKernel' (intervalIntegrable_g.mono_set _)] @@ -412,6 +416,7 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu rw [← intervalIntegral.integral_add (intervalIntegrable_mul_dirichletKernel'_max hx intervalIntegrable_g) (intervalIntegrable_mul_dirichletKernel'_max' hx intervalIntegrable_g)] congr with y ring + calc ENNReal.ofNNReal ‖S_ N g x‖₊ _ ≤ ( ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊ + ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊) / ENNReal.ofReal (2 * Real.pi) := by @@ -448,8 +453,6 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu congr rw [← ENNReal.ofReal_div_of_pos Real.two_pi_pos, mul_div_assoc, div_self Real.two_pi_pos.ne.symm, mul_one] ---TODO: replace congr;ext by congr with - end section lemma rcarleson_exceptional_set_estimate {δ : ℝ} (δpos : 0 < δ) {f : ℝ → ℂ} (hmf : Measurable f) @@ -527,11 +530,8 @@ lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ all_goals linarith [Real.pi_pos] ---TODO: add doc-strings ! -/-ENNReal version of a generalized Lemma 11.1.3 (control approximation effect).-/ ---added subset assumption ---changed interval to match the interval in the theorem +/- This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint.-/ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ : 0 < δ) {h : ℝ → ℂ} (h_measurable : Measurable h) (h_periodic : h.Periodic (2 * Real.pi)) (h_bound : ∀ x, ‖h x‖ ≤ δ ) : ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ MeasureTheory.volume.real E ≤ ε ∧ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, @@ -643,7 +643,6 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ : rw [← ENNReal.ofReal_le_ofReal_iff, ENNReal.ofReal_mul ε'_δ_expression_pos.le, MeasureTheory.measureReal_def, ENNReal.ofReal_toReal E'volume.ne] apply le_trans E'volume_bound rw [ENNReal.ofReal_mul δ_mul_const_pos.le, ← ENNReal.ofReal_rpow_of_nonneg ENNReal.toReal_nonneg (by norm_num), ENNReal.ofReal_toReal E'volume.ne] - --small goal remaining apply mul_nonneg δ_mul_const_pos.le apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg _ = ε := by diff --git a/Carleson/Classical/DirichletKernel.lean b/Carleson/Classical/DirichletKernel.lean index 0d95e6d1..98e3f2be 100644 --- a/Carleson/Classical/DirichletKernel.lean +++ b/Carleson/Classical/DirichletKernel.lean @@ -1,3 +1,5 @@ +/- This file contains definitions and lemmas regarding the Dirichlet kernel. -/ + import Carleson.MetricCarleson import Carleson.Classical.Basic import Mathlib.Analysis.Fourier.AddCircle @@ -11,7 +13,7 @@ open Complex noncomputable section def dirichletKernel (N : ℕ) : ℝ → ℂ := - fun x ↦ ∑ n in Icc (-Int.ofNat ↑N) N, fourier n (x : AddCircle (2 * Real.pi)) + fun x ↦ ∑ n in Icc (-Int.ofNat N) N, fourier n (x : AddCircle (2 * Real.pi)) def dirichletKernel' (N : ℕ) : ℝ → ℂ := fun x ↦ (exp (I * N * x) / (1 - exp (-I * x)) + exp (-I * N * x) / (1 - exp (I * x))) @@ -23,7 +25,6 @@ lemma dirichletKernel_periodic {N : ℕ} : Function.Periodic (dirichletKernel N) simp lemma dirichletKernel'_periodic {N : ℕ} : Function.Periodic (dirichletKernel' N) (2 * Real.pi) := by - --TODO: improve proof intro x simp_rw [dirichletKernel'] push_cast @@ -43,7 +44,7 @@ lemma dirichletKernel'_periodic {N : ℕ} : Function.Periodic (dirichletKernel' . rw [mul_add, exp_add] conv => rhs; rw [← mul_one (cexp _)] congr - convert exp_int_mul_two_pi_mul_I (-Int.ofNat N) using 2 + convert exp_int_mul_two_pi_mul_I (-(N : ℤ)) using 2 simp ring . congr 1 @@ -63,7 +64,7 @@ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : have : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by calc (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) * dirichletKernel N x - _ = ∑ n in Icc (-Int.ofNat N) ↑N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by + _ = ∑ n in Icc (-(N : ℤ)) N, (cexp ((n + 1 / 2) * I * ↑x) - cexp ((n - 1 / 2) * I * ↑x)) := by rw [dirichletKernel, mul_sum] congr with n simp [sub_mul, ← exp_add, ← exp_add] @@ -74,21 +75,22 @@ lemma dirichletKernel_eq {N : ℕ} {x : ℝ} (h : cexp (I * x) ≠ 1) : congr rw_mod_cast [← mul_assoc, mul_comm, ← mul_assoc, inv_mul_cancel, one_mul] exact Real.pi_pos.ne.symm - _ = ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n + 1 / 2) * I * ↑x) - ∑ n in Icc (-Int.ofNat N) ↑N, cexp ((n - 1 / 2) * I * ↑x) := by + _ = ∑ n in Icc (-(N : ℤ)) N, cexp ((n + 1 / 2) * I * ↑x) - ∑ n in Icc (-(N : ℤ)) N, cexp ((n - 1 / 2) * I * ↑x) := by rw [sum_sub_distrib] _ = cexp ((N + 1 / 2) * I * x) - cexp (-(N + 1 / 2) * I * x) := by rw [← sum_Ico_add_eq_sum_Icc, ← sum_Ioc_add_eq_sum_Icc, add_sub_add_comm, - ← zero_add (cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x))] + ← zero_add (cexp ((N + 1 / 2) * I * ↑x) - cexp (-(N + 1 / 2) * I * ↑x))] congr rw [sub_eq_zero] - conv => lhs; rw [← Int.add_sub_cancel (-Int.ofNat N) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add'] + conv => lhs; rw [← Int.add_sub_cancel (-(N : ℤ)) 1, sub_eq_add_neg, ← Int.add_sub_cancel (Nat.cast N) 1, sub_eq_add_neg, ← sum_Ico_add'] congr with n · rw [mem_Ico, mem_Ioc, Int.lt_iff_add_one_le, add_le_add_iff_right, ← mem_Icc, Int.lt_iff_add_one_le, ← mem_Icc] + simp · simp only [Int.reduceNeg, Int.cast_add, Int.cast_neg, Int.cast_one, one_div, add_assoc, sub_eq_add_neg] norm_num - · rw [neg_add_rev, add_comm, Int.ofNat_eq_coe, Int.cast_neg, sub_eq_add_neg] + · rw [neg_add_rev, add_comm, Int.cast_neg, sub_eq_add_neg] norm_cast all_goals simp have h' : (cexp (1 / 2 * I * x) - cexp (-1 / 2 * I * x)) ≠ 0 := by @@ -148,14 +150,14 @@ lemma dirichletKernel_eq_ae {N : ℕ} : ∀ᵐ (x : ℝ), dirichletKernel N x = lemma norm_dirichletKernel_le {N : ℕ} {x : ℝ} : ‖dirichletKernel N x‖ ≤ 2 * N + 1 := by rw [dirichletKernel] - calc ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖ - _ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier n) ↑x‖ := norm_sum_le _ _ - _ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, 1 := by + calc ‖∑ n ∈ Icc (-(N : ℤ)) N, (fourier n) ↑x‖ + _ ≤ ∑ n ∈ Icc (-(N : ℤ)) N, ‖(fourier n) ↑x‖ := norm_sum_le _ _ + _ ≤ ∑ n ∈ Icc (-(N : ℤ)) N, 1 := by apply sum_le_sum have : Fact (0 < 2 * Real.pi) := by rw [fact_iff]; exact Real.two_pi_pos exact fun n _ ↦ le_trans (ContinuousMap.norm_coe_le_norm (fourier n) x) (fourier_norm n).le _ = 2 * N + 1 := by - rw_mod_cast [sum_const, Int.ofNat_eq_coe, Int.card_Icc, sub_neg_eq_add, nsmul_eq_mul, mul_one, + rw_mod_cast [sum_const, Int.card_Icc, sub_neg_eq_add, nsmul_eq_mul, mul_one, Int.toNat_ofNat] ring @@ -167,26 +169,25 @@ lemma norm_dirichletKernel'_le {N : ℕ} {x : ℝ} : ‖dirichletKernel' N x‖ rw [dirichletKernel'_eq_zero h, norm_zero] linarith -/-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] -/ +/-First part of lemma 11.1.8 (Dirichlet kernel) from the blueprint.-/ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) : partialFourierSum N f x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y) := by calc partialFourierSum N f x - _ = ∑ n in Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x := by + _ = ∑ n in Icc (-(N : ℤ)) N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x := by rw [partialFourierSum] - _ = ∑ n in Icc (-Int.ofNat N) ↑N, (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by + _ = ∑ n in Icc (-(N : ℤ)) N, (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by congr 1 with n rw [fourierCoeffOn_eq_integral, smul_mul_assoc] - _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-Int.ofNat N) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by + _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by rw_mod_cast [← smul_sum, real_smul, sub_zero] - _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-Int.ofNat N) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by + _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by congr with n exact (intervalIntegral.integral_mul_const _ _).symm - _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), ∑ n in Icc (-Int.ofNat N) ↑N, (fourier (-n)) y • f y * (fourier n) x := by + _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), ∑ n in Icc (-(N : ℤ)) N, (fourier (-n)) y • f y * (fourier n) x := by rw [← intervalIntegral.integral_finset_sum] exact fun _ _ ↦ IntervalIntegrable.mul_const (h.continuousOn_mul fourier_uniformContinuous.continuous.continuousOn) _ - _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * ∑ n in Icc (-Int.ofNat N) ↑N, (fourier (-n)) y * (fourier n) x := by + _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * ∑ n in Icc (-(N : ℤ)) N, (fourier (-n)) y * (fourier n) x := by congr with y rw [mul_sum] congr with n diff --git a/Carleson/Classical/Helper.lean b/Carleson/Classical/Helper.lean index 01b74c83..aa70d7af 100644 --- a/Carleson/Classical/Helper.lean +++ b/Carleson/Classical/Helper.lean @@ -1,9 +1,13 @@ +/- This file contains helper lemmas. Either they should be replaced by a mathlib version if there is + one or they might be candidates to go there, possibly in a generalized form. -/ + import Carleson.ToMathlib.Misc import Mathlib.MeasureTheory.Integral.IntervalIntegral -/-The lemmas in this file might either already exist in mathlib or be candidates to go there - (in a generalized form). --/ + +theorem Real.volume_uIoc {a b : ℝ} : MeasureTheory.volume (Set.uIoc a b) = ENNReal.ofReal |b - a| := by + /- Cf. proof of Real.volume_interval-/ + rw [Set.uIoc, volume_Ioc, max_sub_min_eq_abs] lemma intervalIntegral.integral_conj' {μ : MeasureTheory.Measure ℝ} {𝕜 : Type} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ}: ∫ x in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ x in a..b, f x ∂μ) := by @@ -34,6 +38,7 @@ lemma MeasureTheory.IntegrableOn.sub {α : Type} {β : Type} {m : MeasurableSpac {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {s : Set α} {f g : α → β} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) : IntegrableOn (f - g) s μ := by apply MeasureTheory.Integrable.sub <;> rwa [← IntegrableOn] + lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLinearOrder α] {ι : Type} [Nonempty ι] {f : ι → α} {s : Set ι} {a : α} (hfs : BddAbove (f '' s)) (ha : ∃ i ∈ s, f i = a) : a ≤ ⨆ i ∈ s, f i := by @@ -69,3 +74,16 @@ lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLi refine ⟨⟨hi, fia⟩, fun x hx ↦ ?_⟩ simp only [Set.mem_range, exists_prop] at hx rwa [hx.2] at fia + + +/-Adapted from mathlib Function.Periodic.exists_mem_Ico₀-/ +theorem Function.Periodic.exists_mem_Ico₀' {α : Type} {β : Type} {f : α → β} {c : α} + [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x : α) : ∃ (n : ℤ), (x - n • c) ∈ Set.Ico 0 c ∧ f x = f (x - n • c) := + let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x + ⟨n, H, (h.sub_zsmul_eq n).symm⟩ + +/-Adapted from mathlib Function.Periodic.exists_mem_Ico₀-/ +theorem Function.Periodic.exists_mem_Ico' {α : Type} {β : Type} {f : α → β} {c : α} + [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x a: α) : ∃ (n : ℤ), (x - n • c) ∈ Set.Ico a (a + c) ∧ f x = f (x - n • c) := + let ⟨n, H, _⟩ := existsUnique_sub_zsmul_mem_Ico hc x a + ⟨n, H, (h.sub_zsmul_eq n).symm⟩ diff --git a/Carleson/Classical/HilbertKernel.lean b/Carleson/Classical/HilbertKernel.lean index 09ccc657..5770beff 100644 --- a/Carleson/Classical/HilbertKernel.lean +++ b/Carleson/Classical/HilbertKernel.lean @@ -1,14 +1,20 @@ +/- This file contains definitions and lemmas regarding the Hilbert kernel. -/ + +import Carleson.Classical.Helper import Carleson.Classical.Basic + import Mathlib.Tactic.FunProp + noncomputable section open Complex ComplexConjugate ---TODO: rename this and introduce local notation def k (x : ℝ) : ℂ := max (1 - |x|) 0 / (1 - exp (I * x)) -/- Little helper lemmas. -/ + +/- Basic properties of k. -/ + lemma k_of_neg_eq_conj_k {x : ℝ} : k (-x) = conj (k x) := by simp [k, conj_ofReal, ← exp_conj, conj_I, neg_mul] @@ -19,7 +25,6 @@ lemma k_of_one_le_abs {x : ℝ} (abs_le_one : 1 ≤ |x|) : k x = 0 := by rw [k, max_eq_right (by linarith)] simp - @[measurability] lemma k_measurable : Measurable k := by unfold k @@ -50,7 +55,6 @@ lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x · linarith · apply lower_secant_bound _ (by rfl) rw [Set.mem_Icc] - --TODO : improve calculations constructor · simp calc |x - y| @@ -78,14 +82,8 @@ lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x rw [this] exact div_nonneg (by norm_num) (by linarith [abs_nonneg (x-y)]) -/-TODO: to mathlib-/ -theorem Real.volume_uIoc {a b : ℝ} : MeasureTheory.volume (Set.uIoc a b) = ENNReal.ofReal |b - a| := by - /- Cf. proof of Real.volume_interval-/ - rw [Set.uIoc, volume_Ioc, max_sub_min_eq_abs] - /-Main part of the proof of Hilbert_kernel_regularity -/ /-TODO: This can be local, i.e. invisible to other files. -/ -/-TODO: might be improved using lower_secant_bound' -/ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ 0 ≤ y') (ypos : 0 < y) (y2ley' : y / 2 ≤ y') (hy : y ≤ 1) (hy' : y' ≤ 1) : ‖k (-y) - k (-y')‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by rw [k_of_abs_le_one, k_of_abs_le_one] @@ -93,7 +91,6 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ rw [_root_.abs_of_nonneg yy'nonneg.1, _root_.abs_of_nonneg yy'nonneg.2] let f : ℝ → ℂ := fun t ↦ (1 - t) / (1 - exp (-(I * t))) set f' : ℝ → ℂ := fun t ↦ (-1 + exp (-(I * t)) + I * (t - 1) * exp (-(I * t))) / (1 - exp (-(I * t))) ^ 2 with f'def - /-TODO: externalize as lemma?-/ set c : ℝ → ℂ := fun t ↦ (1 - t) with cdef set c' : ℝ → ℂ := fun t ↦ -1 with c'def set d : ℝ → ℂ := fun t ↦ (1 - exp (-(I * t))) with ddef @@ -223,29 +220,27 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} : simp at h simp only [zero_sub, abs_neg] wlog yy'nonneg : 0 ≤ y ∧ 0 ≤ y' generalizing y y' - · --TODO : improve case distinction to avoid nesting - by_cases yge0 : 0 ≤ y + · by_cases yge0 : 0 ≤ y · push_neg at yy'nonneg exfalso rw [_root_.abs_of_nonneg yge0, _root_.abs_of_nonneg] at h <;> linarith [yy'nonneg yge0] - --rcases ltTrichotomy - · push_neg at yge0 - by_cases y'ge0 : 0 ≤ y' - · exfalso - rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith - · -- This is the only interesting case. - push_neg at y'ge0 - set! y_ := -y with y_def - set! y'_ := -y' with y'_def - have h_ : 2 * |y_ - y'_| ≤ |y_| := by - rw [y_def, y'_def, ← abs_neg] - simpa [neg_add_eq_sub] - have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith - have := this h_ y_y'_nonneg - rw [y_def, y'_def] at this - simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this - rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this - simpa + push_neg at yge0 + by_cases y'ge0 : 0 ≤ y' + · exfalso + rw [abs_of_neg yge0, abs_of_neg] at h <;> linarith + /- This is the only interesting case. -/ + push_neg at y'ge0 + set! y_ := -y with y_def + set! y'_ := -y' with y'_def + have h_ : 2 * |y_ - y'_| ≤ |y_| := by + rw [y_def, y'_def, ← abs_neg] + simpa [neg_add_eq_sub] + have y_y'_nonneg : 0 ≤ y_ ∧ 0 ≤ y'_ := by constructor <;> linarith + have := this h_ y_y'_nonneg + rw [y_def, y'_def] at this + simp only [neg_neg, abs_neg, sub_neg_eq_add, neg_add_eq_sub] at this + rw [← RCLike.norm_conj, map_sub, ← k_of_neg_eq_conj_k, ← k_of_neg_eq_conj_k, ←abs_neg (y' - y)] at this + simpa /-"Wlog" 0 < y-/ by_cases ypos : y ≤ 0 · have y_eq_zero : y = 0 := le_antisymm ypos yy'nonneg.1 @@ -255,7 +250,7 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} : simp [y_eq_zero, y'_eq_zero] push_neg at ypos - -- Beginning of the main proof. + /- Beginning of the main proof -/ have y2ley' : y / 2 ≤ y' := by rw [div_le_iff two_pos] calc y @@ -266,7 +261,7 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} : rw [abs_eq_self.mpr yy'nonneg.1] at h exact h _ = y' * 2 := by ring - /- Distinguish four cases. -/ + /- Distinguish four cases -/ rcases le_or_gt y 1, le_or_gt y' 1 with ⟨hy | hy, hy' | hy'⟩ · apply le_trans (Hilbert_kernel_regularity_main_part yy'nonneg ypos y2ley' hy hy') gcongr <;> norm_num @@ -317,7 +312,6 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} : rw [_root_.abs_of_nonneg yy'nonneg.1] _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by norm_num · rw [abs_neg, _root_.abs_of_nonneg] <;> linarith - · calc ‖k (-y) - k (-y')‖ _ = 0 := by rw [norm_eq_abs, AbsoluteValue.map_sub_eq_zero_iff, k_of_one_le_abs, diff --git a/Carleson/Classical/SpectralProjectionBound.lean b/Carleson/Classical/SpectralProjectionBound.lean index 63a60001..b3c040c7 100644 --- a/Carleson/Classical/SpectralProjectionBound.lean +++ b/Carleson/Classical/SpectralProjectionBound.lean @@ -1,3 +1,9 @@ +/- This file contains the proof of Lemma 11.1.10 (spectral projection bound). + At the moment, its results are not used as the section about truncated Hilbert transforms + is still missing. + Thus, the result here might not yet have the exact form needed later. +-/ + import Carleson.Classical.Basic open MeasureTheory AddCircle @@ -16,27 +22,18 @@ lemma fourierCoeff_eq_innerProduct {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 exact HilbertBasis.repr_apply_apply fourierBasis f n ---TODO: add version of partialFourierSum for the AddCircle? noncomputable section def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (N : ℕ) (f : ↥(Lp ℂ 2 (@haarAddCircle T hT))) : Lp ℂ p (@haarAddCircle T hT) := ∑ n in Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • fourierLp p n --TODO: add some lemma relating partialFourierSum and partialFourierSumLp -/- -lemma partialFourierSumLp_apply {T : ℝ} [hT : Fact (0 < T)] {p : ENNReal} [Fact (1 ≤ p)] {f : ↥(Lp ℂ 2 (@haarAddCircle T hT))} {N : ℕ} {x : AddCircle T} : - partialFourierSumLp p N f x = partialFourierSum N f x := by --/ - ---TODO: completely reformulate partialFourierSum in terms of more abstract structures? - ---#check Finset.sum lemma partialFourierSumL2_norm {T : ℝ} [hT : Fact (0 < T)] [h2 : Fact (1 ≤ (2 : ENNReal))] {f : ↥(Lp ℂ 2 haarAddCircle)} {N : ℕ} : ‖partialFourierSumLp 2 N f‖ ^ 2 = ∑ n in Finset.Icc (-Int.ofNat N) N, ‖@fourierCoeff T hT _ _ _ f n‖ ^ 2 := by - --TODO: this can probably be simplified calc ‖partialFourierSumLp 2 N f‖ ^ 2 - _ = ‖partialFourierSumLp 2 N f‖ ^ (2 : ℝ) := Eq.symm (Real.rpow_two ‖partialFourierSumLp 2 N f‖) + _ = ‖partialFourierSumLp 2 N f‖ ^ (2 : ℝ) := by + rw [← Real.rpow_natCast]; rfl _ = ‖fourierBasis.repr (partialFourierSumLp 2 N f)‖ ^ (2 : ℝ) := by rw [fourierBasis.repr.norm_map (partialFourierSumLp 2 N f)] _ = ‖∑ n ∈ Finset.Icc (-Int.ofNat N) N, fourierCoeff f n • (fourierBasis.repr (@fourierLp T hT 2 h2 n))‖ ^ (2 : ℝ) := by @@ -69,8 +66,3 @@ lemma spectral_projection_bound {N : ℕ} {T : ℝ} [hT : Fact (0 < T)] (f : Lp ‖partialFourierSumLp 2 N f‖ ≤ ‖f‖ := by rw [← abs_norm, ← abs_norm f, ← sq_le_sq] exact spectral_projection_bound_sq _ _ - --- Bessel's inequality --- #check Orthonormal.sum_inner_products_le --- #check OrthogonalFamily.norm_sum --- #check orthonormal_fourier diff --git a/Carleson/MetricCarleson.lean b/Carleson/MetricCarleson.lean index f231c1dd..83249f12 100644 --- a/Carleson/MetricCarleson.lean +++ b/Carleson/MetricCarleson.lean @@ -31,3 +31,8 @@ theorem metric_carleson [CompatibleFunctions ℝ X (defaultA a)] ∫⁻ x in G, CarlesonOperator K f x ≤ ENNReal.ofReal (C1_0_2 a q) * (volume G) ^ q'⁻¹ * (volume F) ^ q⁻¹ := by sorry + +/- maybe investigate: making `volume` implicit in both `hg` and `h3g` of `metric_carleson` causes slow +elaboration. -/ + +end diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index b7a05faf..5cdb5036 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -6616,7 +6616,7 @@ \chapter{Two-sided Metric Space Carleson} |K(x,y) - K(x',y)| \leq \left(\frac{\rho(x,x')}{\rho(x,y)}\right)^{\frac{1}{a}}\frac{2^{a^3}}{V(x,y)}. \end{equation} %fixme: Should it be V(y,x) rather? -By the additional regularity, we can weaken the assumption \eqref{nontanbound} to an operator that is easier to work with in applications. +By the additional regularity, we can weaken the assumption \eqref{nontanbound} to a family of operators that is easier to work with in applications. Namely, for $r > 0$, $x\in X$, and a bounded, measurable function $f:X\to\C$ supported on a set of finite measure, we define \begin{equation} \label{def-T_r} @@ -6658,7 +6658,7 @@ \chapter{Two-sided Metric Space Carleson} \begin{proof}[Proof of \Cref{two-sided-metric-space-Carleson}] \proves{two-sided-metric-space-Carleson} Let $10$ that for every bounded measurable function $g$ on $X$ supported on a set of finite measure, + Let $f:X\to\C$ be a bounded measurable function supported on a set of finite measure and assume for some $r>0$ that for every bounded measurable function $g:X\to\C$ supported on a set of finite measure, \begin{equation} \label{eq-strong-2-2-assumption} \|T_rg\|_{2}\le 2^{a^3} \|g\|_2. @@ -6708,10 +6708,9 @@ \section{Proof of Cotlar's Inequality} \begin{lemma} \label{geometric-series-estimate} - %fixme: Rename a to something else, make the estimate sharp? - For all real numbers $a\ge 4$, + For all real numbers $x\ge 4$, \begin{equation*} - \sum_{n=0}^\infty 2^{-\frac{n}{a}} \le 2^a. + \sum_{n=0}^\infty 2^{-\frac{n}{x}} \le 2^x. \end{equation*} \end{lemma} \begin{proof} @@ -6719,13 +6718,13 @@ \section{Proof of Cotlar's Inequality} \begin{equation*} 2^{\lambda(-\frac{1}{4})} \le \lambda 2^{-\frac{1}{4}} + (1-\lambda)2^0. \end{equation*} - For $\lambda:=\frac{4}{a}$, we obtain + For $\lambda:=\frac{4}{x}$, we obtain \begin{equation*} - 2^{-\frac 1 a} \le 1 - (1-2^{-\frac 1 4}) \frac{4}{a}. + 2^{-\frac 1 x} \le 1 - (1-2^{-\frac 1 4}) \frac{4}{x}. \end{equation*} We conclude \begin{equation*} - \sum_{n=0}^\infty 2^{-\frac{n}{a}} = \frac{1}{1-2^{-\frac 1 a}} \le \frac{1}{4(1-2^{-\frac 1 4})} a \le 2^a. + \sum_{n=0}^\infty 2^{-\frac{n}{x}} = \frac{1}{1-2^{-\frac 1 x}} \le \frac{1}{4(1-2^{-\frac 1 4})} x \le 2^x. \end{equation*} \end{proof} @@ -6766,14 +6765,13 @@ \section{Proof of Cotlar's Inequality} \end{equation} \begin{equation} \label{secondxx'} - + \left|\int_{2r\le\rho(x,y)} (K(x',y)-K(x,y)) g(y) \,d\mu(y) + + \left|\int_{2r\le\rho(x,y)} (K(x,y)-K(x',y)) g(y) \,d\mu(y) \right| \end{equation} \begin{equation} \label{thirdxx'} - +\left|\int_{r\le\rho(x',y), r\le\rho(x,y)<2r} -|K(x',y) g(y)|\, d\mu(y) -\right| + +\int_{r\le\rho(x',y), r\le\rho(x,y)<2r} +|K(x',y)| |g(y)|\, d\mu(y)\,. \end{equation} Using the bound on $K$ in \eqref{eqkernel-size} and the doubling condition \eqref{doublingx}, we estimate \eqref{firstxx'} by \begin{align} @@ -6814,13 +6812,13 @@ \section{Proof of Cotlar's Inequality} \begin{align} &\sum_{j=1}^\infty \int_{2^jr\le\rho(x,y)< 2^{j+1}r} \left(\frac{\rho(x,x')}{\rho(x,y)}\right)^{\frac{1}{a}}\frac{2^{a^3}}{V(x,y)} |g(y)| \,d\mu(y)\, \\ - &\le + \le& \sum_{j=1}^\infty \left( 2^{-j} \right)^{\frac{1}{a}} \int_{2^jr\le\rho(x,y)< 2^{j+1}r} \frac{2^{a^3}}{\mu(B(x,2^j r))} |g(y)| \,d\mu(y) \\ - &\le + \le& \sum_{j=1}^\infty 2^{-\frac{j}{a}} \frac{2^{a^3 + a}}{\mu(B(x,2^{j+1} r))} \int_{\rho(x,y)<2^{j+1}r} |g(y)| \, d\mu(y) \\ \label{secondxx'c} -&\le 2^{a^3 + a} \sum_{j=1}^\infty 2^{-\frac{j}{a}} Mg(x)\,. +\le& 2^{a^3 + a} \sum_{j=1}^\infty 2^{-\frac{j}{a}} Mg(x)\,. \end{align} Using \Cref{geometric-series-estimate}, we estimate \eqref{secondxx'c} by @@ -6888,7 +6886,7 @@ \section{Proof of Cotlar's Inequality} = \int_{B(x',R)\setminus (B(x',r) \cup B(x,\frac{R}{2}))} K(x',y) g(y) \,d\mu(y) \end{equation} As $\frac{R}{2}\le\rho(x,y)$ together with $\rho(x,x')\le\frac {R}{4}$ implies -$\frac {R}{4}\le\rho(x',y)$, we can estimate \eqref{eqcotlar2} with \eqref{eqkernel-size} by +$\frac {R}{4}\le\rho(x',y)$, we can estimate the absolute value of \eqref{eqcotlar2} with \eqref{eqkernel-size} by \begin{align*} \le &\frac{2^{a^3}}{\mu(B(x',\frac{R}{4}))} \int_{B(x,2R)\setminus B(x',\frac{R}{4})} |g(y)|\, d\mu(y) \\ @@ -6930,7 +6928,7 @@ \section{Proof of Cotlar's Inequality} \end{equation} \begin{equation} \ge - \frac 1{\mu(B(x,\frac{R}{4}))}\int_{F_1} 4 M(T_rg)(x)\, dx' + \frac 1{\mu(B(x,\frac{R}{4}))}\int_{F_1} 4 M(T_rg)(x)\, dx' \,. \end{equation} Dividing by $M(T_rg)(x)$ gives \begin{equation} @@ -7004,9 +7002,9 @@ \section{Proof of Cotlar's Inequality} \le 2^{a^3+20a+4} \|Mg\|_2 + 2^{2}\|M(T_rg)\|_2 \end{equation} \begin{equation} - \le 2^{a^3+24a+5} \|g\|_2 + 2^{4a+3}\|T_r(g)\|_2\, . + \le 2^{a^3+24a+5} \|g\|_2 + 2^{4a+3}\|T_r g\|_2\, . \end{equation} -Applying \eqref{two-sided-Hr-bound-assumption}, gives +Applying \eqref{two-sided-Hr-bound-assumption} gives \begin{equation} \|T_{*}^r g\|_2\le 2^{a^3+24a+5}\|g\|_2 + 2^{a^3+4a+3}\|g\|_2\, . \end{equation} @@ -7015,7 +7013,7 @@ \section{Proof of Cotlar's Inequality} %fixme: Change location of next argument? In order to pass from the one-sided truncation in $T_r$ and $T_{*}^r$ to the two-sided truncation in $T_*$, we show in the following two lemmas that the integral in \eqref{def-tang-unm-op} can be exchanged for an integral over the difference of two balls. \begin{lemma} \label{small-annulus} - Let $f$ be a bounded measurable function with bounded support on $X$. + Let $f:X\to\C$ be a bounded measurable function supported on a set of finite measure. Let $x\in X$ and $R>0$. Then, for all $\epsilon>0$, there exists some $\delta>0$ such that \begin{equation} @@ -7038,7 +7036,7 @@ \section{Proof of Cotlar's Inequality} \begin{lemma}\label{tang-unm-op-ball-diff} \uses{small-annulus} - Let $f$ be a bounded measurable function with bounded support on $X$. + Let $f:X\to\C$ be a bounded measurable function supported on a set of finite measure. For all $x\in X$, \begin{equation} \label{tang-unm-op-eq} @@ -7047,7 +7045,7 @@ \section{Proof of Cotlar's Inequality} \end{lemma} \begin{proof} We show two inequalities. Let $\epsilon>0$. -Let $R_10$, +Let $R_10$, \begin{alignat}{3} \label{eq-without-suprema-1} &&&\left|\int_{R_1<\rho(x',y)\alpha\}$. -Then $E_\alpha$ is open. Assume first that $E_\alpha \ne X$. We apply \Cref{ball-covering} with $O=E_\alpha$ to obtain the family $B_j, j\in J,$. Without loss of generality, we can assume $J=\N$. Define +Then $E_\alpha$ is open. Assume first that $E_\alpha \ne X$. We apply \Cref{ball-covering} with $O=E_\alpha$ to obtain the family $B_j, j\in J,$. Without loss of generality, we can assume $J=\N$. Define inductively \begin{equation} Q_j := B_j^* \setminus \left(\bigcup_{ij} B_i \right). \end{equation} -Then the $B_j\subset Q_j\subset B_j^*$, the $Q_j$ are pairwise disjoint and $\bigcup_j Q_j = E_\alpha$. +Then $B_j\subset Q_j\subset B_j^*$, the $Q_j$ are pairwise disjoint and $\bigcup_j Q_j = E_\alpha$. Define \begin{equation} \label{eq-g-def} @@ -7415,7 +7414,7 @@ \section{Calder\'on-Zygmund Decomposition} \mu\left(\{x\in X: |T_r f(x)|>\alpha\}\right)\le \mu(X) \le \frac{1}{\alpha'} \int |f(y)|\, d\mu(y) \le \frac{2^{a^3 + 19a}}{\alpha} \int |f(y)|\, d\mu(y), \end{equation*} -which proves \eqref{eq-weak-1-1} +which proves \eqref{eq-weak-1-1}. So assume from now on that $\alpha'>\frac{1}{\mu(X)}\int |f|\,d\mu$. Using \Cref{Calderon-Zygmund-decomposition} for $f$ and $\alpha'$, we obtain the decomposition \begin{equation*} @@ -7537,7 +7536,7 @@ \section{Calder\'on-Zygmund Decomposition} T_r b_j(x)&=\int_{B_j} K(x,y) (\mathbf{1}_{X\setminus B(x,r)}(y)b_j(y)-d_j)\, dy + \int_{B_j} d_j K(x,y) \, dy \\ &= \int_{B_j} (K(x,y)-K(x,x_j)) (\mathbf{1}_{X\setminus B(x,r)}(y)b_j(y)-d_j)\, dy + \int_{B_j} d_j K(x,y) \, dy. \end{align*} -Thus, using the triangle inequality, the estimate above and \eqref{eq-dj-est}, we obtain +Thus, using the triangle inequality, the equation above and \eqref{eq-dj-est}, we obtain \begin{equation*} |T_r b_j(x)|\le \end{equation*} @@ -7560,7 +7559,7 @@ \section{Calder\'on-Zygmund Decomposition} \label{eq-J2-union-subset} A\subset B(x,3r) \setminus B(x,\frac{r}{3}). \end{equation} -Indeed, for each $j\in \mathcal{J}_2(x)$ and $y\in B_j$, +Indeed, for each $j\in \mathcal{J}_2(x)$ and $y\in B_j$, using again \eqref{eq-Om-cj}, \begin{equation*} \rho(x,x_j) < r+r_j \le r + \frac{1}{2} \rho(x,x_j) \implies \rho(x,x_j) < 2r \end{equation*} @@ -7602,10 +7601,10 @@ \section{Calder\'on-Zygmund Decomposition} \label{estimate-F-set} \uses{Calderon-Zygmund-decomposition,geometric-series-estimate} For $F$ as defined in \Cref{estimate-Tr-bad-X-minus-Omega}, we have - \begin{equation*} + \begin{equation} \label{eq-F-X-minus-Omega} \mu(\{x\in X\setminus\Omega: F(x)>\alpha/8\}) \le \frac{2^{a^3+9a+4}}{\alpha} \int |f(y)|\,d\mu(y)\,. - \end{equation*} + \end{equation} \end{lemma} \begin{proof} @@ -7757,7 +7756,7 @@ \section{The classical Carleson theorem} \begin{proof} \leanok - Most of this is part of the Lean library. + Periodicity follows directly from the definitions. The other properties are part of the Lean library. \end{proof} We prove in \Cref{10smooth}: @@ -7813,7 +7812,7 @@ \section{The classical Carleson theorem} This shows \eqref{aeconv} for the given $E$ and $N_0$. \end{proof} -Let $\kappa:\R\to \R$ be the function defined by +Let $\kappa:\R\to \C$ be the function defined by $\kappa(0)=0$ and for $0<|x|<1$ \begin{equation}\label{eq-hilker} \kappa(x)=\frac { 1-|x|}{1-e^{ix}}\, From 6ae9c490fc51c06d37431eaf3afdddef0ff3149a Mon Sep 17 00:00:00 2001 From: James Sundstrom Date: Wed, 7 Aug 2024 04:35:26 -0400 Subject: [PATCH 2/2] Prove MeasureTheory.SublinearOn.maximalFunction (#107) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - The definition of `SublinearOn` was missing the requirement `c ≥ 0`. - The statement of `MeasureTheory.SublinearOn.maximalFunction` had a spurious `p`; `MB` is defined with p=1, so there's no need for a general `p`. - The blueprint says that `𝓑` is finite, so I used that assumption even though several theorems in the file assume `𝓑` is countable instead. I also changed the assumption in `hasStrongType_MB`. --- Carleson/HardyLittlewood.lean | 103 +++++++++++++++++++++++++++---- Carleson/RealInterpolation.lean | 105 +++++++++++++++++++++++++++++++- Carleson/ToMathlib/Misc.lean | 41 +++++++++++++ 3 files changed, 236 insertions(+), 13 deletions(-) diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean index 7ca458af..3c0a3b42 100644 --- a/Carleson/HardyLittlewood.lean +++ b/Carleson/HardyLittlewood.lean @@ -30,6 +30,71 @@ M_𝓑 in the blueprint. -/ abbrev MB (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ) (u : X → E) (x : X) := maximalFunction μ 𝓑 c r 1 u x +-- We will replace the criterion `P` used in `MeasureTheory.SublinearOn.maximalFunction` with a +-- weaker criterion `P'` that is closed under addition and scalar multiplication. + +variable (μ) in +private def P (f : X → E) : Prop := Memℒp f ∞ μ ∨ Memℒp f 1 μ + +variable (μ) in +private def P' (f : X → E) : Prop := + AEStronglyMeasurable f μ ∧ ∀ (c : X) (r : ℝ), ∫⁻ (y : X) in ball c r, ‖f y‖₊ ∂μ < ⊤ + +private lemma P'_of_P {u : X → E} (hu : P μ u) : P' μ u := by + refine ⟨hu.elim Memℒp.aestronglyMeasurable Memℒp.aestronglyMeasurable, fun c r ↦ ?_⟩ + refine hu.elim (fun hu ↦ ?_) (fun hu ↦ ?_) + · have hfg : ∀ᵐ (x : X) ∂μ, x ∈ ball c r → ‖u x‖₊ ≤ snormEssSup u μ := + (coe_nnnorm_ae_le_snormEssSup u μ).mono (by tauto) + apply lt_of_le_of_lt (MeasureTheory.setLIntegral_mono_ae' measurableSet_ball hfg) + rw [MeasureTheory.setLIntegral_const (ball c r) (snormEssSup u μ)] + refine ENNReal.mul_lt_top ?_ (measure_ball_ne_top c r) + exact snorm_exponent_top (f := u) ▸ hu.snorm_lt_top |>.ne + · have := hu.snorm_lt_top + simp [snorm, one_ne_zero, reduceIte, ENNReal.one_ne_top, snorm', ENNReal.one_toReal, + ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self] at this + exact lt_of_le_of_lt (setLIntegral_le_lintegral _ _) this + +private lemma P'.add {f : X → E} {g : X → E} (hf : P' μ f) (hg : P' μ g) : P' μ (f + g) := by + constructor + · exact AEStronglyMeasurable.add hf.1 hg.1 + · intro c r + apply lt_of_le_of_lt (lintegral_mono_nnreal fun y ↦ Pi.add_apply f g y ▸ nnnorm_add_le _ _) + simp_rw [ENNReal.coe_add, lintegral_add_left' <| aemeasurable_coe_nnreal_ennreal_iff.mpr + hf.1.aemeasurable.nnnorm.restrict] + exact ENNReal.add_lt_top.mpr ⟨hf.2 c r, hg.2 c r⟩ + +private lemma P'.smul {f : X → E} (hf : P' μ f) (s : ℝ) : P' μ (s • f) := by + refine ⟨AEStronglyMeasurable.const_smul hf.1 s, fun c r ↦ ?_⟩ + simp_rw [Pi.smul_apply, nnnorm_smul, ENNReal.coe_mul, lintegral_const_mul' _ _ ENNReal.coe_ne_top] + exact ENNReal.mul_lt_top ENNReal.coe_ne_top (hf.2 c r).ne + +-- 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 lemma T.add_le (i : ι) {f g : X → E} (hf : P' μ f) (hg : P' μ 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 (laverage_lt_top (hf.2 _ _).ne).ne (laverage_lt_top (hg.2 _ _).ne).ne] + rw [ENNReal.toReal_le_toReal] + · rw [← setLaverage_add_left' hf.1.ennnorm] + exact setLaverage_mono' measurableSet_ball (fun x _ ↦ ENNNorm_add_le (f x) (g x)) + · exact (laverage_lt_top ((P'.add hf hg).2 _ _).ne).ne + · exact (ENNReal.add_lt_top.2 ⟨laverage_lt_top (hf.2 _ _).ne, (laverage_lt_top (hg.2 _ _).ne)⟩).ne + +private lemma T.smul (i : ι) : ∀ {f : X → E} {d : ℝ}, P' μ 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 [setLaverage_const_mul' ENNReal.ofReal_ne_top] + congr + ext x + simp only [nnnorm_smul, ENNReal.coe_mul, ← Real.toNNReal_eq_nnnorm_of_nonneg hd] + congr + lemma covering_separable_space (X : Type*) [PseudoMetricSpace X] [SeparableSpace X] : ∃ C : Set X, C.Countable ∧ ∀ r > 0, ⋃ c ∈ C, ball c r = univ := by simp_rw [← Metric.dense_iff_iUnion_ball, exists_countable_dense] @@ -132,14 +197,28 @@ protected theorem HasStrongType.MB_top (h𝓑 : 𝓑.Countable) : refine ENNReal.coe_toNNReal_le_self |>.trans ?_ apply MB_le_snormEssSup -/- Prove this by proving that -* suprema of sublinear maps are sublinear, -* the indicator of a sublinear map is sublinear -* constant maps are sublinear -/ -protected theorem MeasureTheory.SublinearOn.maximalFunction {p : ℝ} (hp₁ : 1 ≤ p) : +protected theorem MeasureTheory.SublinearOn.maximalFunction (h𝓑 : 𝓑.Finite) : SublinearOn (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal) - (fun f ↦ Memℒp f ∞ μ ∨ Memℒp f 1 μ) 1 := by - sorry + (fun f ↦ Memℒp f ∞ μ ∨ Memℒp f 1 μ) 1 := by + apply SublinearOn.antitone P'_of_P + simp only [MB, maximalFunction, ENNReal.rpow_one, inv_one] + apply SublinearOn.biSup 𝓑 _ _ P'.add (fun hf _ ↦ P'.smul hf _) + · 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 (SublinearOn.const (T μ c r i) (P' μ) (T.add_le i) (fun f d ↦ T.smul i)).indicator + · intro f x hf + 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 (laverage_lt_top (hf.2 (c i) (r i)).ne).ne + · simp [hx] /- The proof is roughly between (9.0.12)-(9.0.22). -/ variable (μ) in @@ -154,7 +233,7 @@ irreducible_def CMB (A p : ℝ≥0) : ℝ≥0 := sorry /- The proof is given between (9.0.12)-(9.0.34). Use the real interpolation theorem instead of following the blueprint. -/ -lemma hasStrongType_MB (h𝓑 : 𝓑.Countable) {p : ℝ≥0} +lemma hasStrongType_MB (h𝓑 : 𝓑.Finite) {p : ℝ≥0} (hp : 1 < p) {u : X → E} (hu : AEStronglyMeasurable u μ) : HasStrongType (fun (u : X → E) (x : X) ↦ MB μ 𝓑 c r u x |>.toReal) p p μ μ (CMB A p) := by @@ -165,10 +244,10 @@ lemma hasStrongType_MB (h𝓑 : 𝓑.Countable) {p : ℝ≥0} zero_lt_one (pow_pos (A_pos μ) 2) (p := p) (q := p) (A := 1) (by simp [ENNReal.coe_inv h2p.ne']) (by simp [ENNReal.coe_inv h2p.ne']) - (fun f hf ↦ AEStronglyMeasurable.maximalFunction_toReal h𝓑) - (.maximalFunction hp.le) - (HasStrongType.MB_top h𝓑 |>.hasWeakType le_top) - (HasWeakType.MB_one μ h𝓑) + (fun f hf ↦ AEStronglyMeasurable.maximalFunction_toReal h𝓑.countable) + (.maximalFunction h𝓑) + (HasStrongType.MB_top h𝓑.countable |>.hasWeakType le_top) + (HasWeakType.MB_one μ h𝓑.countable) convert this using 1 sorry -- let's deal with the constant later diff --git a/Carleson/RealInterpolation.lean b/Carleson/RealInterpolation.lean index 006c52fe..6ac1077c 100644 --- a/Carleson/RealInterpolation.lean +++ b/Carleson/RealInterpolation.lean @@ -40,9 +40,112 @@ lemma aestronglyMeasurable_trunc (hf : AEStronglyMeasurable f μ) : def SubadditiveOn (T : (α → E₁) → α' → E₂) (P : (α → E₁) → Prop) (A : ℝ) : Prop := ∀ (f g : α → E₁) (x : α'), P f → P g → ‖T (f + g) x‖ ≤ A * (‖T f x‖ + ‖T g x‖) +namespace SubadditiveOn + +def antitone {T : (α → E₁) → α' → E₂} {P P' : (α → E₁) → Prop} + (h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ} (sa : SubadditiveOn T P' A) : SubadditiveOn T P A := + fun f g x hf hg ↦ sa f g x (h hf) (h hg) + +lemma neg (P : (α → E₁) → Prop) {A : ℝ} (hA : A < 0) (h : SubadditiveOn T P A) + (f : α → E₁) (hf : P f) : T f = 0 := + funext fun x ↦ norm_le_zero_iff.mp (by nlinarith [norm_nonneg (T (f + f) x), h f f x hf hf]) + +lemma zero {P : (α → E₁) → Prop} (hP : ∀ {f g : α → E₁}, P f → P g → P (f + g)) + (A : ℝ) (h : ∀ u, P u → T u = 0) : SubadditiveOn T P A := + fun f g x hf hg ↦ by simp [h f hf, h g hg, h (f + g) (hP hf hg)] + +lemma biSup {ι : Type*} (𝓑 : Set ι) {T : ι → (α → E₁) → α' → ℝ≥0∞} + {P : (α → E₁) → Prop} (hT : ∀ (u : α → E₁) (x : α'), P u → ⨆ i ∈ 𝓑, T i u x ≠ ∞) + (hP : ∀ {f g : α → E₁}, P f → P g → P (f + g)) + (A : ℝ) (h : ∀ i ∈ 𝓑, SubadditiveOn (fun u x ↦ (T i u x).toReal) P A) : + SubadditiveOn (fun u x ↦ (⨆ i ∈ 𝓑, T i u x).toReal) P A := by + have hT' : ∀ i ∈ 𝓑, ∀ (x : α') (u : α → E₁), P u → T i u x ≠ ∞ := + fun i hi x f hf h ↦ hT f x hf <| eq_top_iff.mpr <| h ▸ le_biSup (fun i ↦ T i f x) hi + by_cases A0 : A < 0 + · refine SubadditiveOn.zero hP A (fun f hf ↦ funext fun x ↦ ?_) + suffices ⨆ i ∈ 𝓑, T i f x = 0 by simp [this] + simp only [iSup_eq_zero] + intro i hi + have := (toReal_eq_zero_iff _).mp (congr_fun ((h i hi).neg P A0 f hf) x) + exact this.resolve_right (hT' i hi x f hf) + push_neg at A0 + intro f g x hf hg + simp only [Real.norm_eq_abs, abs_toReal] + rw [← toReal_add (hT f x hf) (hT g x hg), ← toReal_ofReal A0, ← toReal_mul] + apply toReal_mono <| mul_ne_top ofReal_ne_top (add_ne_top.mpr ⟨hT f x hf, hT g x hg⟩) + simp only [iSup_le_iff] + intro i hi + specialize h i hi f g x hf hg + simp only [Real.norm_eq_abs, abs_toReal] at h + rw [← toReal_add (hT' i hi x f hf) (hT' i hi x g hg), ← toReal_ofReal A0, ← toReal_mul, + toReal_le_toReal (hT' i hi x (f + g) (hP hf hg)) <| mul_ne_top ofReal_ne_top <| + add_ne_top.mpr ⟨hT' i hi x f hf, hT' i hi x g hg⟩] at h + apply h.trans + gcongr <;> apply le_biSup _ hi + +lemma indicator {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ} + (sa : SubadditiveOn T P A) (S : Set α') : + SubadditiveOn (fun u x ↦ (S.indicator (fun y ↦ T u y) x)) P A := by + intro f g x hf hg + by_cases hx : x ∈ S <;> simp [hx, sa f g x hf hg] + +-- If `T` is constant in the second argument (but not necessarily the first) and satisfies +-- a subadditivity criterion, then `SubadditiveOn 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‖) : + SubadditiveOn (fun u (_ : α') ↦ t u) P 1 := by + intro f g x hf hg + simpa using h_add hf hg + +end SubadditiveOn + /-- The operator is sublinear on functions satisfying `P` with constant `A`. -/ def SublinearOn (T : (α → E₁) → α' → E₂) (P : (α → E₁) → Prop) (A : ℝ) : Prop := - SubadditiveOn T P A ∧ ∀ (f : α → E₁) (c : ℝ), P f → T (c • f) = c • T f + SubadditiveOn T P A ∧ ∀ (f : α → E₁) (c : ℝ), P f → c ≥ 0 → T (c • f) = c • T f + +namespace SublinearOn + +lemma antitone {T : (α → E₁) → α' → E₂} {P P' : (α → E₁) → Prop} + (h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ} (sl : SublinearOn T P' A) : SublinearOn T P A := + ⟨sl.1.antitone (fun hu ↦ h hu), fun u c hu hc ↦ sl.2 u c (h hu) hc⟩ + +lemma biSup {ι : Type*} (𝓑 : Set ι) (T : ι → (α → E₁) → α' → ℝ≥0∞) + {P : (α → E₁) → Prop} (hT : ∀ (u : α → E₁) (x : α'), P u → ⨆ 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 ∈ 𝓑, SublinearOn (fun u x ↦ (T i u x).toReal) P A) : + SublinearOn (fun u x ↦ (⨆ i ∈ 𝓑, T i u x).toReal) P A := by + have hT' : ∀ i ∈ 𝓑, ∀ (x : α') (u : α → E₁), P u → T i u x ≠ ∞ := + fun i hi x f hf h ↦ hT f x hf <| eq_top_iff.mpr <| h ▸ le_biSup (fun i ↦ T i f x) hi + refine ⟨SubadditiveOn.biSup 𝓑 hT h_add A (fun i hi ↦ (h i hi).1), ?_⟩ + intro f c hf hc + ext x + rw [Pi.smul_apply, ← ENNReal.toReal_ofReal hc, smul_eq_mul] + simp only [← toReal_mul, ENNReal.mul_iSup] + congr 1 + refine biSup_congr (fun i hi ↦ ?_) + have := congr_fun ((h i hi).2 f c hf hc) x + simp only [Pi.smul_apply, smul_eq_mul, ← toReal_ofReal_mul c (T i f x) hc] at this + rw [ENNReal.toReal_eq_toReal (hT' i hi x (c • f) (h_smul hf hc)) + (mul_lt_top ofReal_ne_top (hT' i hi x f hf)).ne] at this + rwa [toReal_ofReal hc] + +lemma indicator {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ} (S : Set α') + (sl : SublinearOn T P A) : + SublinearOn (fun u x ↦ (S.indicator (fun y ↦ T u y) x)) P A := by + refine ⟨SubadditiveOn.indicator sl.1 S, fun f c hf hc ↦ funext (fun x ↦ ?_)⟩ + by_cases hx : x ∈ S <;> simp [hx, congr_fun (sl.2 f c hf hc) x] + +-- If `T` is constant in the second argument (but not necessarily the first) and satisfies +-- certain requirements, then `SublinearOn 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) : + SublinearOn (fun u (_ : α') ↦ t u) P 1 := by + refine ⟨SubadditiveOn.const t P h_add, fun f c hf hc ↦ funext (fun x ↦ ?_)⟩ + simpa using h_smul f hf hc + +end SublinearOn /-- The constant occurring in the real interpolation theorem. -/ -- todo: remove unused variables diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean index 3e9c5be2..3fff8378 100644 --- a/Carleson/ToMathlib/Misc.lean +++ b/Carleson/ToMathlib/Misc.lean @@ -185,6 +185,27 @@ lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc Nat.Ico_succ_right_eq_insert_Ico h, Finset.sum_insert Finset.right_not_mem_Ico, add_comm (lintegral ..), ih] +/-! ## Averaging -/ + +-- Named for consistency with `lintegral_add_left'` +-- Maybe add laverage/setLaverage theorems for all the other lintegral_add statements? +lemma setLaverage_add_left' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} + {s : Set α} {f g : α → ENNReal} (hf : AEMeasurable f μ) : + ⨍⁻ x in s, (f x + g x) ∂μ = ⨍⁻ x in s, f x ∂μ + ⨍⁻ x in s, g x ∂μ := by + simp_rw [setLaverage_eq, ENNReal.div_add_div_same, lintegral_add_left' hf.restrict] + +-- Named for consistency with `setLintegral_mono'` +lemma setLaverage_mono' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} + {s : Set α} (hs : MeasurableSet s) {f g : α → ENNReal} (h : ∀ x ∈ s, f x ≤ g x) : + ⨍⁻ x in s, f x ∂μ ≤ ⨍⁻ x in s, g x ∂μ := by + simp_rw [setLaverage_eq] + exact ENNReal.div_le_div_right (setLIntegral_mono' hs h) (μ s) + +lemma setLaverage_const_mul' {α : Type*} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} + {s : Set α} {f : α → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) : + c * ⨍⁻ x in s, f x ∂μ = ⨍⁻ x in s, c * f x ∂μ := by + simp_rw [setLaverage_eq, ← mul_div_assoc c, lintegral_const_mul' c f hc] + end MeasureTheory namespace MeasureTheory @@ -299,3 +320,23 @@ lemma reprs_inj (hx : x ∈ hr.reprs) (hy : y ∈ hr.reprs) (h : r x y) : x = y exact out_inj' hx hy h end EquivalenceOn + +namespace Set.Finite + +lemma biSup_eq {α : Type*} {ι : Type*} [CompleteLinearOrder α] {s : Set ι} + (hs : s.Finite) (hs' : s.Nonempty) (f : ι → α) : + ∃ i ∈ s, ⨆ j ∈ s, f j = f i := by + induction' s, hs using dinduction_on with a s _ _ ihs hf + · simp at hs' + rw [iSup_insert] + by_cases hs : s.Nonempty + · by_cases ha : f a ⊔ ⨆ x ∈ s, f x = f a + · use a, mem_insert a s + · obtain ⟨i, hi⟩ := ihs hs + use i, Set.mem_insert_of_mem a hi.1 + rw [← hi.2, sup_eq_right] + simp only [sup_eq_left, not_le] at ha + exact ha.le + · simpa using Or.inl fun i hi ↦ (hs (nonempty_of_mem hi)).elim + +end Set.Finite