From 823dd5fb8ec3bce93bcef6a41cb9315f1710a8d8 Mon Sep 17 00:00:00 2001 From: ldiedering <129694072+ldiedering@users.noreply.github.com> Date: Sun, 9 Jun 2024 13:28:24 +0200 Subject: [PATCH] Update blueprint section 10 (#22) --- Carleson/Theorem1_1/Approximation.lean | 21 +- Carleson/Theorem1_1/Basic.lean | 83 ++-- .../Theorem1_1/Carleson_on_the_real_line.lean | 4 +- Carleson/Theorem1_1/ClassicalCarleson.lean | 13 +- .../Control_Approximation_Effect.lean | 57 ++- Carleson/Theorem1_1/Hilbert_kernel.lean | 107 ++-- blueprint/src/chapter/main.tex | 468 +++++------------- blueprint/src/preamble/common.tex | 1 + 8 files changed, 279 insertions(+), 475 deletions(-) diff --git a/Carleson/Theorem1_1/Approximation.lean b/Carleson/Theorem1_1/Approximation.lean index 56a05bc6..1997e912 100644 --- a/Carleson/Theorem1_1/Approximation.lean +++ b/Carleson/Theorem1_1/Approximation.lean @@ -37,7 +37,6 @@ lemma uniformContinuous_iff_bounded [PseudoMetricSpace α] [PseudoMetricSpace β . intro h ε εpos obtain ⟨δ, δpos, _, hδ⟩ := h ε εpos use δ - end section /- TODO: might be generalized. -/ @@ -296,7 +295,7 @@ lemma int_sum_nat {β : Type} [AddCommGroup β] [TopologicalSpace β] [Continuou /-TODO: Weaken statement to pointwise convergence to simplify proof?-/ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function.Periodic f (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) : - ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Ico 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε := by + ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε := by have fact_two_pi_pos : Fact (0 < 2 * Real.pi) := by rw [fact_iff] exact Real.two_pi_pos @@ -343,11 +342,19 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function. simp only [ContinuousMap.coe_sum, sum_apply] at this convert this.le using 2 congr 1 - . rw [g_def] - simp only [ContinuousMap.coe_mk] - rw [AddCircle.liftIco_coe_apply] - rw [zero_add] - exact hx + . rw [g_def, ContinuousMap.coe_mk] + by_cases h : x = 2 * Real.pi + . conv => lhs; rw [h, ← zero_add (2 * Real.pi), periodicf] + have := AddCircle.coe_add_period (2 * Real.pi) 0 + rw [zero_add] at this + rw [h, this, AddCircle.liftIco_coe_apply] + simp [Real.pi_pos] + . have : x ∈ Set.Ico 0 (2 * Real.pi) := by + use hx.1 + apply lt_of_le_of_ne hx.2 h + rw [AddCircle.liftIco_coe_apply] + rw [zero_add] + exact this . rw [partialFourierSum] congr ext n diff --git a/Carleson/Theorem1_1/Basic.lean b/Carleson/Theorem1_1/Basic.lean index c7ebc998..b4e05efe 100644 --- a/Carleson/Theorem1_1/Basic.lean +++ b/Carleson/Theorem1_1/Basic.lean @@ -102,12 +102,17 @@ lemma partialFourierSum_uniformContinuous {f : ℝ → ℂ} {N : ℕ} : UniformC sorry -/-Slightly different and stronger version of Lemma 10.11 (lower secant bound). -/ +theorem strictConvexOn_cos_Icc : StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)) Real.cos := by + apply strictConvexOn_of_deriv2_pos (convex_Icc _ _) Real.continuousOn_cos fun x hx => ?_ + rw [interior_Icc] at hx + simp [Real.cos_neg_of_pi_div_two_lt_of_lt hx.1 hx.2] + +/- Lemma 10.11 (lower secant bound) from the paper. -/ lemma lower_secant_bound' {η : ℝ} {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le : |x| ≤ 2 * Real.pi - η) : - η / 4 ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by + (2 / Real.pi) * η ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by by_cases ηpos : η ≤ 0 - . calc η / 4 - _ ≤ 0 := by linarith + . calc (2 / Real.pi) * η + _ ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (div_nonneg zero_le_two Real.pi_pos.le) ηpos _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg push_neg at ηpos wlog x_nonneg : 0 ≤ x generalizing x @@ -125,13 +130,7 @@ lemma lower_secant_bound' {η : ℝ} {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_l rw [mul_sub, Complex.conj_ofReal, Complex.exp_sub, mul_comm Complex.I (2 * Real.pi), Complex.exp_two_pi_mul_I, ←inv_eq_one_div, ←Complex.exp_neg] all_goals linarith by_cases h : x ≤ Real.pi / 2 - . calc η / 4 - _ ≤ (2 / Real.pi) * η := by - rw [div_le_iff (by norm_num)] - field_simp - rw [le_div_iff Real.pi_pos, mul_comm 2, mul_assoc] - gcongr - linarith [Real.pi_le_four] + . calc (2 / Real.pi) * η _ ≤ (2 / Real.pi) * x := by gcongr _ = (1 - (2 / Real.pi) * x) * Real.sin 0 + ((2 / Real.pi) * x) * Real.sin (Real.pi / 2) := by simp _ ≤ Real.sin ((1 - (2 / Real.pi) * x) * 0 + ((2 / Real.pi) * x) * (Real.pi / 2)) := by @@ -156,30 +155,52 @@ 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)] . push_neg at h - calc η / 4 - _ ≤ 1 := by - rw [div_le_iff (by norm_num), one_mul] - exact (le_abs_x.trans x_le_pi).trans Real.pi_le_four - _ ≤ |(1 - Complex.exp (Complex.I * ↑x)).re| := by - rw [mul_comm, Complex.exp_mul_I] - simp - rw [Complex.cos_ofReal_re, le_abs] - left - simp - apply Real.cos_nonpos_of_pi_div_two_le_of_le h.le - linarith + calc (2 / Real.pi) * η + _ ≤ (2 / Real.pi) * x := by gcongr + _ = 1 - ((1 - (2 / Real.pi) * (x - Real.pi / 2)) * Real.cos (Real.pi / 2) + ((2 / Real.pi) * (x - Real.pi / 2)) * Real.cos (Real.pi)) := by + field_simp + ring + _ ≤ 1 - (Real.cos ((1 - (2 / Real.pi) * (x - Real.pi / 2)) * (Real.pi / 2) + (((2 / Real.pi) * (x - Real.pi / 2)) * (Real.pi)))) := by + gcongr + apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [Real.pi_nonneg]) + . simp + constructor <;> linarith [Real.pi_nonneg] + . rw [sub_nonneg, mul_comm] + apply mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) Real.pi_nonneg) (by simpa) + . exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) (by linarith [h]) + . simp + _ = 1 - Real.cos x := by + congr + field_simp + ring + _ ≤ Real.sqrt ((1 - Real.cos x) ^ 2) := by + rw [Real.sqrt_sq_eq_abs] + apply le_abs_self _ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by - rw [Complex.norm_eq_abs] - apply Complex.abs_re_le_abs + rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq] + simp + rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re] + apply (Real.sqrt_le_sqrt_iff _).mpr + . simp [pow_two_nonneg] + . linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)] -/- Lemma 10.11 (lower secant bound) from the paper. -/ -lemma lower_secant_bound {η : ℝ} (ηpos : η > 0) {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)) (xAbs : η ≤ |x|) : - η / 8 ≤ Complex.abs (1 - Complex.exp (Complex.I * x)) := by - calc η / 8 - _ ≤ η / 4 := by + +/-Slightly weaker version of Lemma 10.11 (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 + . calc η / 2 + _ ≤ 0 := by linarith + _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg + push_neg at ηpos + calc η / 2 + _ ≤ (2 / Real.pi) * η := by ring_nf + rw [mul_assoc] gcongr - norm_num + field_simp + rw [div_le_div_iff (by norm_num) Real.pi_pos] + linarith [Real.pi_le_four] _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply lower_secant_bound' xAbs rw [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul] diff --git a/Carleson/Theorem1_1/Carleson_on_the_real_line.lean b/Carleson/Theorem1_1/Carleson_on_the_real_line.lean index 6bf7f3f5..d7624f85 100644 --- a/Carleson/Theorem1_1/Carleson_on_the_real_line.lean +++ b/Carleson/Theorem1_1/Carleson_on_the_real_line.lean @@ -430,14 +430,14 @@ instance h6 : IsCZKernel 4 K where 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)])] calc Complex.abs (K x y) - _ ≤ 2 ^ (4 : ℝ) / (2 * |x - y|) := by apply Hilbert_kernel_bound + _ ≤ 2 ^ (2 : ℝ) / (2 * |x - y|) := by apply Hilbert_kernel_bound _ ≤ 2 ^ (4 : ℝ) ^ 3 / (2 * |x - y|) := by gcongr <;> norm_num /- uses Hilbert_kernel_regularity -/ norm_sub_le := by intro x y y' h rw [Real.dist_eq, Real.dist_eq] at * calc ‖K x y - K x y'‖ - _ ≤ 2 ^ 10 * (1 / |x - y|) * (|y - y'| / |x - y|) := by + _ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|) := by apply Hilbert_kernel_regularity linarith [abs_nonneg (x-y)] _ ≤ (|y - y'| / |x - y|) ^ (4 : ℝ)⁻¹ * (2 ^ (4 : ℝ) ^ 3 / Real.vol x y) := by diff --git a/Carleson/Theorem1_1/ClassicalCarleson.lean b/Carleson/Theorem1_1/ClassicalCarleson.lean index 54cc6c3c..27642049 100644 --- a/Carleson/Theorem1_1/ClassicalCarleson.lean +++ b/Carleson/Theorem1_1/ClassicalCarleson.lean @@ -53,16 +53,7 @@ theorem classical_carleson {f : ℝ → ℂ} _ ≤ ε' + (ε / 4) + (ε / 4) := by gcongr . exact hf₀ x - . by_cases h : x = 2 * Real.pi - . rw [h, ←zero_add (2 * Real.pi), periodic_f₀, partialFourierSum_periodic] - apply hN₀ N NgtN₀ 0 - simp [Real.pi_pos] - . have : x ∈ Set.Ico 0 (2 * Real.pi) := by - simp - simp at hx - use hx.1.1 - apply lt_of_le_of_ne hx.1.2 h - convert hN₀ N NgtN₀ x this + . exact hN₀ N NgtN₀ x hx.1 . have := hE x hx N rw [hdef, partialFourierSum_sub (contDiff_f₀.continuous.intervalIntegrable 0 (2 * Real.pi)) (unicontf.continuous.intervalIntegrable 0 (2 * Real.pi))] at this apply le_trans this @@ -72,5 +63,5 @@ theorem classical_carleson {f : ℝ → ℂ} rw [ε'def, div_div] apply div_le_div_of_nonneg_left εpos.le (by norm_num) rw [← div_le_iff' (by norm_num)] - apply le_trans' (lt_C_control_approximation_effect εpos).le (by norm_num) + apply le_trans' (lt_C_control_approximation_effect εpos).le (by linarith [Real.two_le_pi]) _ ≤ ε := by linarith diff --git a/Carleson/Theorem1_1/Control_Approximation_Effect.lean b/Carleson/Theorem1_1/Control_Approximation_Effect.lean index cd58960f..691e4b85 100644 --- a/Carleson/Theorem1_1/Control_Approximation_Effect.lean +++ b/Carleson/Theorem1_1/Control_Approximation_Effect.lean @@ -302,11 +302,11 @@ lemma le_CarlesonOperatorReal' {f : ℝ → ℂ} (hf : IntervalIntegrable f Meas apply Measurable.of_uncurry_left exact Hilbert_kernel_measurable measurability - have boundedness₁ {y : ℝ} (h : r ≤ dist x y) : ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖ ≤ (2 ^ (4 : ℝ) / (2 * r)) := by + have boundedness₁ {y : ℝ} (h : r ≤ dist x y) : ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖ ≤ (2 ^ (2 : ℝ) / (2 * r)) := by calc ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖ _ = ‖(I * (-↑n * ↑x)).exp‖ * ‖K x y‖ * ‖(I * ↑n * ↑y).exp‖ := by rw [norm_mul, norm_mul] - _ ≤ 1 * (2 ^ (4 : ℝ) / (2 * |x - y|)) * 1 := by + _ ≤ 1 * (2 ^ (2 : ℝ) / (2 * |x - y|)) * 1 := by gcongr . rw [norm_eq_abs, mul_comm] norm_cast @@ -315,7 +315,7 @@ lemma le_CarlesonOperatorReal' {f : ℝ → ℂ} (hf : IntervalIntegrable f Meas . rw [norm_eq_abs, mul_assoc, mul_comm] norm_cast rw [abs_exp_ofReal_mul_I] - _ ≤ (2 ^ (4 : ℝ) / (2 * r)) := by + _ ≤ (2 ^ (2 : ℝ) / (2 * r)) := by rw [one_mul, mul_one, ← Real.dist_eq] gcongr have integrable₁ := (integrable_annulus hx hf rpos.le rle1) @@ -405,9 +405,9 @@ theorem rcarleson_exceptional_set_estimate_specific {δ : ℝ} (δpos : 0 < δ) ring_nf -def C_control_approximation_effect (ε : ℝ) := (((C1_2 4 2 * (8 / (Real.pi * ε)) ^ (2 : ℝ)⁻¹)) + 8) +def C_control_approximation_effect (ε : ℝ) := (C1_2 4 2 * (8 / (Real.pi * ε)) ^ (2 : ℝ)⁻¹) + Real.pi -lemma lt_C_control_approximation_effect {ε : ℝ} (εpos : 0 < ε) : 8 < C_control_approximation_effect ε := by +lemma lt_C_control_approximation_effect {ε : ℝ} (εpos : 0 < ε) : Real.pi < C_control_approximation_effect ε := by rw [C_control_approximation_effect] apply lt_add_of_pos_of_le _ (by rfl) apply mul_pos (C1_2_pos (by norm_num)) @@ -415,9 +415,9 @@ lemma lt_C_control_approximation_effect {ε : ℝ} (εpos : 0 < ε) : 8 < C_cont apply div_pos (by norm_num) apply mul_pos Real.pi_pos εpos -lemma C_control_approximation_effect_pos {ε : ℝ} (εpos : 0 < ε) : 0 < C_control_approximation_effect ε := lt_trans' (lt_C_control_approximation_effect εpos) (by norm_num) +lemma C_control_approximation_effect_pos {ε : ℝ} (εpos : 0 < ε) : 0 < C_control_approximation_effect ε := lt_trans' (lt_C_control_approximation_effect εpos) Real.pi_pos -lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ ε) : C_control_approximation_effect ε * δ = ((δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ * (2 / ε) ^ (2 : ℝ)⁻¹) / Real.pi) + 8 * δ := by +lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ ε) : C_control_approximation_effect ε * δ = ((δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ * (2 / ε) ^ (2 : ℝ)⁻¹) / Real.pi) + Real.pi * δ := by symm rw [C_control_approximation_effect, mul_comm, mul_div_right_comm, mul_comm δ, mul_assoc, mul_comm δ, ← mul_assoc, ← mul_assoc, ← add_mul] congr 2 @@ -509,7 +509,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real rfl intro _ norm_num - have le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - 8 * δ) * (2 * Real.pi)) ≤ T' f x + T' ((starRingEnd ℂ) ∘ f) x := by + have le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) ≤ T' f x + T' ((starRingEnd ℂ) ∘ f) x := by have h_intervalIntegrable' : IntervalIntegrable h MeasureTheory.volume 0 (2 * Real.pi) := by apply h_intervalIntegrable.mono_set rw [Set.uIcc_of_le (by linarith [Real.pi_pos]), Set.uIcc_of_le (by linarith [Real.pi_pos])] @@ -520,9 +520,9 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real --set S := Set.Ioo (x - Real.pi) (x + Real.pi) with Sdef obtain ⟨xIcc, N, hN⟩ := hx rw [partialFourierSum_eq_conv_dirichletKernel' h_intervalIntegrable'] at hN - have : ENNReal.ofReal (8 * δ * (2 * Real.pi)) ≠ ⊤ := ENNReal.ofReal_ne_top + have : ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) ≠ ⊤ := ENNReal.ofReal_ne_top rw [← (ENNReal.add_le_add_iff_right this)] - calc ENNReal.ofReal ((ε' - 8 * δ) * (2 * Real.pi)) + ENNReal.ofReal (8 * δ * (2 * Real.pi)) + calc ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) _ = ENNReal.ofReal ((2 * Real.pi) * ε') := by rw [← ENNReal.ofReal_add] . congr @@ -538,8 +538,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real apply Real.rpow_nonneg linarith [Real.pi_pos] . apply Real.rpow_nonneg (div_nonneg (by norm_num) hε.1.le) - . apply mul_nonneg _ Real.two_pi_pos.le - linarith + . apply mul_nonneg (mul_nonneg Real.pi_pos.le hδ.le) Real.two_pi_pos.le _ ≤ ENNReal.ofReal ((2 * Real.pi) * abs (1 / (2 * Real.pi) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), h y * dirichletKernel' N (x - y))) := by gcongr _ = ‖∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), h y * dirichletKernel' N (x - y)‖₊ := by rw [map_mul, map_div₀, ←mul_assoc] @@ -587,7 +586,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real --apply abs.isAbsoluteValue.abv_add norm_cast apply nnnorm_add_le - _ ≤ (T' f x + T' ((starRingEnd ℂ) ∘ f) x) + ENNReal.ofReal (8 * δ * (2 * Real.pi)) := by + _ ≤ (T' f x + T' ((starRingEnd ℂ) ∘ f) x) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) := by --Estimate the two parts gcongr . --first part @@ -669,7 +668,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real apply NNReal.le_toNNReal_of_coe_le rw [coe_nnnorm] calc ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), h y * (min |x - y| 1) * dirichletKernel' N (x - y)‖ - _ ≤ (δ * 8) * |(x + Real.pi) - (x - Real.pi)| := by + _ ≤ (δ * Real.pi) * |(x + Real.pi) - (x - Real.pi)| := by apply intervalIntegral.norm_integral_le_of_norm_le_const intro y hy rw [Set.uIoc_of_le (by linarith)] at hy @@ -702,13 +701,13 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real norm_cast rw [abs_exp_ofReal_mul_I, one_div] _ = 2 * (min |z| 1 / ‖1 - exp (I * z)‖) := by ring - _ ≤ 2 * 4 := by - gcongr + _ ≤ 2 * (Real.pi / 2) := by + gcongr 2 * ?_ + --. apply min_le_right . by_cases h : (1 - exp (I * z)) = 0 - . rw [h] - simp - simp - rw [div_le_iff', ←div_le_iff, ←norm_eq_abs] + . rw [h, norm_zero, div_zero] + linarith [Real.pi_pos] + rw [div_le_iff', ←div_le_iff, div_div_eq_mul_div, mul_div_assoc, mul_comm] apply lower_secant_bound' . apply min_le_left . have : |z| ≤ Real.pi := by @@ -717,10 +716,10 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real constructor <;> linarith [hy.1, hy.2] rw [min_def] split_ifs <;> linarith - . norm_num - . rwa [←norm_eq_abs, norm_pos_iff] - _ = 8 := by norm_num - _ = 8 * δ * (2 * Real.pi) := by + . linarith [Real.pi_pos] + . rwa [norm_pos_iff] + _ = Real.pi := by ring + _ = Real.pi * δ * (2 * Real.pi) := by simp rw [←two_mul, _root_.abs_of_nonneg Real.two_pi_pos.le] ring @@ -735,9 +734,9 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real _ < ⊤ := ENNReal.ofReal_lt_top obtain ⟨E', E'subset, measurableSetE', E'measure, h⟩ := ENNReal.le_on_subset MeasureTheory.volume measurableSetE (CarlesonOperatorReal'_measurable f_measurable) (CarlesonOperatorReal'_measurable (Measurable.comp continuous_star.measurable f_measurable)) le_operator_add have E'volume : MeasureTheory.volume E' < ⊤ := lt_of_le_of_lt (MeasureTheory.measure_mono E'subset) Evolume - have : ENNReal.ofReal (Real.pi * (ε' - 8 * δ)) * MeasureTheory.volume E' ≤ ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by - calc ENNReal.ofReal (Real.pi * (ε' - 8 * δ)) * MeasureTheory.volume E' - _ = ENNReal.ofReal ((ε' - 8 * δ) * (2 * Real.pi)) / 2 * MeasureTheory.volume E' := by + have : ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' ≤ ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by + calc ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' + _ = ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 * MeasureTheory.volume E' := by congr rw [← ENNReal.ofReal_ofNat, ← ENNReal.ofReal_div_of_pos (by norm_num)] ring_nf @@ -760,7 +759,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real apply mul_pos hδ (by rw [C1_2]; norm_num) apply Real.rpow_pos_of_pos linarith [Real.two_pi_pos] - have ε'_δ_expression_pos : 0 < Real.pi * (ε' - 8 * δ) := by + have ε'_δ_expression_pos : 0 < Real.pi * (ε' - Real.pi * δ) := by rw [ε'def, C_control_approximation_effect_eq hε.1.le, add_sub_cancel_right, mul_div_cancel₀ _ Real.pi_pos.ne.symm] apply mul_pos δ_mul_const_pos apply Real.rpow_pos_of_pos @@ -775,7 +774,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real conv => lhs; rw [←Real.rpow_one (MeasureTheory.volume.real E')] congr norm_num - _ ≤ 2 * (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - 8 * δ))) ^ (2 : ℝ) := by + _ ≤ 2 * (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - Real.pi * δ))) ^ (2 : ℝ) := by gcongr rw [Real.rpow_mul MeasureTheory.measureReal_nonneg] gcongr diff --git a/Carleson/Theorem1_1/Hilbert_kernel.lean b/Carleson/Theorem1_1/Hilbert_kernel.lean index 6ace1692..6eab3f7c 100644 --- a/Carleson/Theorem1_1/Hilbert_kernel.lean +++ b/Carleson/Theorem1_1/Hilbert_kernel.lean @@ -34,49 +34,45 @@ def K (x y : ℝ) : ℂ := k (x - y) lemma Hilbert_kernel_measurable : Measurable (Function.uncurry K) := k_measurable.comp measurable_sub /- Lemma 10.13 (Hilbert kernel bound) -/ -lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (4 : ℝ) / (2 * |x - y|) := by - --intro x y +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‖ _ ≤ 1 / ‖1 - Complex.exp (Complex.I * ↑(x - y))‖ := by rw [K, k, norm_div] gcongr rw [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg] - . apply max_le + . apply max_le _ zero_le_one linarith [abs_nonneg (x-y)] - linarith . apply le_max_right - _ ≤ 1 / (|x - y| / 8) := by + _ ≤ 1 / (|x - y| / 2) := by gcongr . linarith - . apply lower_secant_bound - . exact h.1 - . rw [Set.mem_Icc] - --TODO : improve calculations - constructor - . simp only [neg_mul, neg_add_le_iff_le_add] - calc |x - y| - _ ≤ 1 := h.2.le - _ ≤ 2 * Real.pi - 1 := by - rw [le_sub_iff_add_le] - linarith [Real.two_le_pi] - _ ≤ 2 * Real.pi + (x - y) := by - rw [sub_eq_add_neg] - gcongr - exact (abs_le.mp h.2.le).1 - . calc x - y - _ ≤ |x - y| := le_abs_self (x - y) - _ ≤ 1 := h.2.le - _ ≤ 2 * Real.pi - 1 := by - rw [le_sub_iff_add_le] - linarith [Real.two_le_pi] - _ ≤ 2 * Real.pi - |x - y| := by - gcongr - exact h.2.le - . trivial - _ = 8 / |x - y| := by + . apply lower_secant_bound _ (by rfl) + rw [Set.mem_Icc] + --TODO : improve calculations + constructor + . simp + calc |x - y| + _ ≤ 1 := h.2.le + _ ≤ 2 * Real.pi - 1 := by + rw [le_sub_iff_add_le] + linarith [Real.two_le_pi] + _ ≤ 2 * Real.pi + (x - y) := by + rw [sub_eq_add_neg] + gcongr + exact (abs_le.mp h.2.le).1 + . calc x - y + _ ≤ |x - y| := le_abs_self (x - y) + _ ≤ 1 := h.2.le + _ ≤ 2 * Real.pi - 1 := by + rw [le_sub_iff_add_le] + linarith [Real.two_le_pi] + _ ≤ 2 * Real.pi - |x - y| := by + gcongr + exact h.2.le + _ = 2 / |x - y| := by field_simp - _ ≤ (2 : ℝ) ^ (4 : ℝ) / (2 * |x - y|) := by + _ ≤ (2 : ℝ) ^ (2 : ℝ) / (2 * |x - y|) := by ring_nf trivial . push_neg at h @@ -102,7 +98,7 @@ theorem Real.volume_uIoc {a b : ℝ} : MeasureTheory.volume (Set.uIoc a b) = ENN /-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 ^ 10 * (1 / |y|) * (|y - y'| / |y|) := by + ‖k (-y) - k (-y')‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by rw [k_of_abs_le_one, k_of_abs_le_one] . simp only [abs_neg, Complex.ofReal_neg, mul_neg, ge_iff_le] rw [abs_of_nonneg yy'nonneg.1, abs_of_nonneg yy'nonneg.2] @@ -199,7 +195,7 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ apply intervalIntegral.norm_intervalIntegral_eq _ ≤ ∫ (t : ℝ) in Ι y' y, ‖f' t‖ := by apply MeasureTheory.norm_integral_le_integral_norm - _ ≤ ∫ (t : ℝ) in Ι y' y, 3 / ((y / 2) / 8) ^ 2 := by + _ ≤ ∫ (t : ℝ) in Ι y' y, 3 / ((y / 2) / 2) ^ 2 := by apply MeasureTheory.setIntegral_mono_on . apply f'_cont.norm.integrableOn_uIcc.mono_set apply Set.Ioc_subset_Icc_self @@ -241,20 +237,20 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ . rw [mul_comm, ←neg_mul, mul_comm] norm_cast apply lower_secant_bound - . linarith - . simp + . simp only [neg_mul, Set.mem_Icc, neg_add_le_iff_le_add, le_add_neg_iff_add_le, + neg_le_sub_iff_le_add] constructor <;> linarith [Real.two_le_pi, Real.two_pi_pos] . rw [abs_neg, le_abs] left rcases ht with ht | ht <;> linarith [ht.1] - _ = (MeasureTheory.volume (Ι y' y)).toReal * (3 / ((y / 2) / 8) ^ 2) := by + _ = (MeasureTheory.volume (Ι y' y)).toReal * (3 / ((y / 2) / 2) ^ 2) := by apply MeasureTheory.setIntegral_const - _ = |y - y'| * (3 / ((y / 2) / 8) ^ 2) := by + _ = |y - y'| * (3 / ((y / 2) / 2) ^ 2) := by congr rw [Real.volume_uIoc, ENNReal.toReal_ofReal (abs_nonneg (y - y'))] - _ = (3 * (8 * 2) ^ 2) * (1 / y) * (|y - y'| / y) := by + _ = (3 * (2 * 2) ^ 2) * (1 / y) * (|y - y'| / y) := by ring - _ ≤ 2 ^ 10 * (1 / y) * (|y - y'| / y) := by + _ ≤ 2 ^ 6 * (1 / y) * (|y - y'| / y) := by gcongr norm_num . rw [abs_neg, abs_of_nonneg yy'nonneg.2] @@ -264,7 +260,7 @@ lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ /- Lemma 10.14 (Hilbert kernel regularity) -/ lemma Hilbert_kernel_regularity {x y y' : ℝ} : - 2 * |y - y'| ≤ |x - y| → ‖K x y - K x y'‖ ≤ 2 ^ 10 * (1 / |x - y|) * (|y - y'| / |x - y|) := by + 2 * |y - y'| ≤ |x - y| → ‖K x y - K x y'‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|) := by rw [K, K] wlog x_eq_zero : x = 0 generalizing x y y' . intro h @@ -333,23 +329,25 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} : _ = y' * 2 := by ring /- Distinguish four cases. -/ rcases le_or_gt y 1, le_or_gt y' 1 with ⟨hy | hy, hy' | hy'⟩ - . exact Hilbert_kernel_regularity_main_part yy'nonneg ypos y2ley' hy hy' + . apply le_trans (Hilbert_kernel_regularity_main_part yy'nonneg ypos y2ley' hy hy') + gcongr <;> norm_num . rw [@k_of_one_le_abs (-y')] . calc ‖k (-y) - 0‖ _ = ‖k (-y) - k (-1)‖ := by congr apply (k_of_one_le_abs _).symm simp - _ ≤ 2 ^ 10 * (1 / |y|) * (|y - 1| / |y|) := by + _ ≤ 2 ^ 6 * (1 / |y|) * (|y - 1| / |y|) := by apply Hilbert_kernel_regularity_main_part constructor all_goals linarith - _ ≤ 2 ^ 10 * (1 / |y|) * (|y - y'| / |y|) := by - gcongr 2 ^ 10 * (1 / |y|) * (?_ / |y|) + _ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by + gcongr 2 ^ 6 * (1 / |y|) * (?_ / |y|) rw [abs_sub_comm, abs_of_nonneg, abs_sub_comm, abs_of_nonneg] <;> linarith + _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by + gcongr <;> norm_num . rw [abs_neg, abs_of_nonneg] <;> linarith . rw [@k_of_one_le_abs (-y)] - /-TODO: This case does not seem to function as in the paper. Maybe the constant must be increased. -/ . calc ‖0 - k (-y')‖ _ = ‖k (-1) - k (-y')‖ := by congr @@ -357,11 +355,11 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} : simp _ = ‖k (-y') - k (-1)‖ := by rw [norm_sub_rev] - _ ≤ 2 ^ 10 * (1 / |y'|) * (|y' - 1| / |y'|) := by + _ ≤ 2 ^ 6 * (1 / |y'|) * (|y' - 1| / |y'|) := by apply Hilbert_kernel_regularity_main_part constructor all_goals linarith - _ = 2 ^ 10 * (1 / y') * ((1 - y') / y') := by + _ = 2 ^ 6 * (1 / y') * ((1 - y') / y') := by congr . rw [abs_of_nonneg] exact yy'nonneg.2 @@ -370,29 +368,28 @@ lemma Hilbert_kernel_regularity {x y y' : ℝ} : linarith . rw [abs_of_nonneg] exact yy'nonneg.2 - _ ≤ 2 ^ 10 * (1 / (y / 2)) * ((1 - y') / (y / 2)) := by + _ ≤ 2 ^ 6 * (1 / (y / 2)) * ((1 - y') / (y / 2)) := by gcongr . apply div_nonneg <;> linarith . linarith - _ = (2 ^ 10 * 2 * 2) * (1 / y) * ((1 - y') / y) := by + _ = (2 ^ 6 * 2 * 2) * (1 / y) * ((1 - y') / y) := by ring - _ ≤ (2 ^ 10 * 2 * 2) * (1 / |y|) * (|y - y'| / |y|) := by + _ ≤ (2 ^ 6 * 2 * 2) * (1 / |y|) * (|y - y'| / |y|) := by gcongr apply div_nonneg <;> linarith rw [abs_of_nonneg yy'nonneg.1] rw [abs_of_nonneg] <;> linarith rw [abs_of_nonneg yy'nonneg.1] - _ ≤ 2 ^ 10 * (1 / |y|) * (|y - y'| / |y|) := by + _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by gcongr - /-TODO: not possible because constant is too small-/ - sorry + norm_num . rw [abs_neg, abs_of_nonneg] <;> linarith . calc ‖k (-y) - k (-y')‖ _ = 0 := by simp rw [k_of_one_le_abs, k_of_one_le_abs] <;> (rw [abs_neg, abs_of_nonneg] <;> linarith) - _ ≤ 2 ^ 10 * (1 / |y|) * (|y - y'| / |y|) := by + _ ≤ 2 ^ 8 * (1 / |y|) * (|y - y'| / |y|) := by apply mul_nonneg apply mul_nonneg . norm_num diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 826fd481..c1d72412 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -39,7 +39,7 @@ \chapter{Introduction} \begin{theorem}[classical Carleson] \label{classical-Carleson} \leanok -\uses{piecewise-constant-approximation, convergence-for-piecewise-constant, +\uses{smooth-approximation, convergence-for-smooth, control-approximation-effect} Let $f$ be a $2\pi$-periodic complex-valued uniformly continuous function on $\mathbb{R}$ satisfying the bound $|f(x)|\le 1$ for all $x\in \mathbb{R}$. For all $0<\epsilon<1$, there exists a Borel set $E\subset [0,2\pi]$ with Lebesgue measure $|E|\le \epsilon$ and a positive integer $N_0$ such that for all $x\in [0,2\pi]\setminus E$ and all integers $N>N_0$, we have \begin{equation}\label{aeconv} @@ -6315,7 +6315,7 @@ \chapter{Proof of The Classical Carleson Theorem} The convergence of partial Fourier sums is proved in \Cref{10classical} in two steps. In the first step, -we establish convergence on a suitable dense subclass of functions. We choose piece-wise constant functions as subclass, the convergence is stated in \Cref{convergence-for-piecewise-constant} and proved in \Cref{10piecewise}. +we establish convergence on a suitable dense subclass of functions. We choose smooth functions as subclass, the convergence is stated in \Cref{convergence-for-smooth} and proved in \Cref{10smooth}. In the second step, one controls the relevant error of approximating a general function by a function in the subclass. This is stated in \Cref{control-approximation-effect} and proved in \Cref{10difference}. @@ -6340,111 +6340,48 @@ \chapter{Proof of The Classical Carleson Theorem} \section{The classical Carleson theorem} \label{10classical} -Let a uniformly continuous $2\pi$-periodic function $f:\R\to \mathbb{C}$, bounded in absolute value by $1$, be given. Let $0<\epsilon<1$ be given. - +Let a uniformly continuous $2\pi$-periodic function $f:\R\to \mathbb{C}$ and $0<\epsilon<1$ be given. +Let +\begin{equation} + C_{a,q} := \frac{2^{450a^3}}{(q-1)^5} +\end{equation} +denote the constant from \Cref{metric-space-Carleson}. +Define +\begin{equation} + \epsilon' := \frac \epsilon {4 (C_{4,2} \cdot (8 / (\pi\epsilon))^{\frac 1 2} + \pi)}. +\end{equation} By uniform continuity of $f$, there is a $0<\delta<\pi$ such that for all $x,x' \in \R$ with $|x-x'|\le \delta$ we have \begin{equation}\label{uniconbound} -|f(x)-f(x')|\le 2^{-2^{50}}\epsilon^2\, . -\end{equation} -Let $K$ be the Gaussian bracket of $\frac{2\pi}\delta+1$, that is the unique integer with -\begin{equation} - K\le \frac{2\pi}{\delta} +1< K+1\,, -\end{equation} -and note that $K>2$ by assumption on $\delta$. -For each $x\in \R$, let $k(x)$ be the Gaussian bracket of $Kx/2\pi$, that is the unique integer such that -\begin{equation}\label{definekx} -k(x)\le \frac{Kx}{2\pi}1$, -\begin{equation} - |E_1|\le \sum_{k=0}^{K}\frac {\epsilon}{4K}= \frac{\epsilon}{4}\left(1+\frac 1K\right)\le \frac \epsilon 2\, \, . -\end{equation} - -We prove in \Cref{10piecewise}: -\begin{lemma}[convergence for piecewise constant] -\label{convergence-for-piecewise-constant} -\uses{constant-function,flat-interval-partial-sum} - For all $N>\frac {2^{25} K^2}{\epsilon ^3}$ and - \begin{equation} - x\in [0,2\pi)\setminus E_1 - \end{equation} -we have +We prove in \Cref{10smooth}: +\begin{lemma}[convergence for smooth] +\leanok +\label{convergence-for-smooth} +\uses{convergence-for-twice-contdiff} + There exists some $N_0 \in \N$ such that for all $N>N_0$ and $x\in [0,2\pi]$ we have \begin{equation} |S_N f_0 (x)- f_0(x)|\le \frac \epsilon 4\, . \end{equation} @@ -6453,12 +6390,13 @@ \section{The classical Carleson theorem} We prove in \Cref{10difference}: \begin{lemma}[control approximation effect] +\leanok \label{control-approximation-effect} -\uses{real-Carleson} - There is a set $E_2 \subset \R$ with Lebesgue measure - $|E_2|\le \frac \epsilon 2$ such that for all +\uses{real-Carleson,dirichlet-kernel,lower-secant-bound} + There is a set $E \subset \R$ with Lebesgue measure + $|E|\le \epsilon$ such that for all \begin{equation} - x\in [0,2\pi)\setminus E_2 + x\in [0,2\pi)\setminus E \end{equation} we have \begin{equation} @@ -6467,22 +6405,14 @@ \section{The classical Carleson theorem} \le \frac \epsilon 4\,. \end{equation} \end{lemma} - -Define -\begin{equation} - E:=E_1\cup E_2\, . -\end{equation} -Then -\begin{equation} - |E|\le |E_1|+|E_2|\le \frac \epsilon 2 +\frac \epsilon 2 \le \epsilon\, . -\end{equation} -Let $N_0$ be the unique integer such that -\begin{equation} - N_0- 1\le {2^{25} K^2}{\epsilon ^{-3}}N_0$ we have by the triangle inequality \begin{equation*} @@ -6491,14 +6421,12 @@ \section{The classical Carleson theorem} \begin{equation}\label{epsilonthird} \le |f(x)-f_0(x)|+ |f_0(x)-S_Nf_0(x)|+|S_Nf_0(x)-S_N f(x)|\, . \end{equation} -Using \eqref{uniconbound} and Lemmas \ref{convergence-for-piecewise-constant} -and \ref{control-approximation-effect}, we estimate \eqref{epsilonthird} by +Using \Cref{smooth-approximation,convergence-for-smooth,control-approximation-effect}, we estimate \eqref{epsilonthird} by \begin{equation} - \le 2^{-2^{50}} \epsilon^2 +\frac \epsilon 4 +\frac \epsilon 4\le \epsilon\, . + \le \epsilon' +\frac \epsilon 4 +\frac \epsilon 4\le \epsilon\, . \end{equation} -This shows \eqref{aeconv} for the given $E$ and $N_0$ -and completes the proof of \Cref{classical-Carleson}. - +This shows \eqref{aeconv} for the given $E$ and $N_0$. +\end{proof} Let $\kappa:\R\to \R$ be the function defined by $\kappa(0)=0$ and for $0<|x|<1$ @@ -6516,10 +6444,11 @@ \section{The classical Carleson theorem} in \Cref{10carleson} as an application of \Cref{metric-space-Carleson}. \begin{lemma}[real Carleson]\label{real-Carleson} +\leanok \uses{metric-space-Carleson,real-line-metric,real-line-measure,real-line-doubling,oscillation-control,frequency-monotone,frequency-ball-doubling,frequency-ball-growth,integer-ball-cover,real-van-der-Corput,nontangential-Hilbert} Let $F,G$ be Borel subsets of $\R$ with finite measure. Let $f$ be a bounded measurable function on $\R$ with $|f|\le \mathbf{1}_F$. Then \begin{equation} - \left|\int _G Tf(x) \, dx\right| \le 2^{2^{40}}|F|^{\frac 12} |G|^{\frac 12} \, , + \left|\int _G Tf(x) \, dx\right| \le C_{4,2} |F|^{\frac 12} |G|^{\frac 12} \, , \end{equation} where \begin{equation} @@ -6638,7 +6567,6 @@ \section{The classical Carleson theorem} \begin{proof} -\proves{dirichlet-kernel} \leanok We have by definitions and interchanging sum and integral \begin{equation*} @@ -6672,11 +6600,10 @@ \section{The classical Carleson theorem} \leanok Let $\eta>0$ and $-2\pi +\eta \le x\le 2\pi-\eta$ with $|x|\ge \eta$. Then \begin{equation} - |1-e^{ix}|\ge \frac {\eta} 4 + |1-e^{ix}|\ge \frac{2}{\pi} \eta \end{equation} \end{lemma} \begin{proof} -\proves{lower-secant-bound} \leanok We have $$ @@ -6706,12 +6633,11 @@ \section{The classical Carleson theorem} \uses{lower-secant-bound} For $x,y\in \R$ with $x\neq y$ we have \begin{equation}\label{eqcarl30} - |\kappa(x-y)|\le 2^4(2|x-y|)^{-1}\, . + |\kappa(x-y)|\le 2^2(2|x-y|)^{-1}\, . \end{equation} \end{lemma} \begin{proof} \leanok -\proves{Hilbert-kernel-bound} Fix $x\neq y$. If $\kappa(x-y)$ is zero, then \eqref{eqcarl30} is evident. Assume $\kappa(x-y)$ is not zero, then $0<|x-y|<1$. We have \begin{equation}\label{eqcarl31} @@ -6720,13 +6646,14 @@ \section{The classical Carleson theorem} We estimate with \Cref{lower-secant-bound} \begin{equation}\label{eqcarl311} -|\kappa(x-y)|\le \frac {1}{|1-e^{i(x-y)}|}\le \frac 8{|x-y|}\, . +|\kappa(x-y)|\le \frac {1}{|1-e^{i(x-y)}|}\le \frac 2{|x-y|}\, . \end{equation} This proves \eqref{eqcarl30} in the given case and completes the proof of the lemma. \end{proof} \begin{lemma}[Hilbert kernel regularity] \label{Hilbert-kernel-regularity} +\leanok \uses{lower-secant-bound} For $x,y,y'\in \R$ with $x\neq y,y'$ and \begin{equation} @@ -6735,11 +6662,12 @@ \section{The classical Carleson theorem} \end{equation} we have \begin{equation}\label{eqcarl301} - |\kappa(x-y) - \kappa(x-y')|\le 2^{10}\frac{1}{|x-y|} \frac{|y-y'|}{|x-y|}\, . + |\kappa(x-y) - \kappa(x-y')|\le 2^{8}\frac{1}{|x-y|} \frac{|y-y'|}{|x-y|}\, . \end{equation} \end{lemma} \begin{proof} +\leanok Upon replacing $y$ by $y-x$ and $y'$ by $y'-x$ on the left-hand side of \eqref{eq-close-hoelder}, we can assume that $x = 0$. Then the assumption \eqref{eq-close-hoelder} implies that $y$ and $y'$ have the same sign. Since $\kappa(y) = \bar \kappa(-y)$ we can assume that they are both positive. Then it follows from \eqref{eq-close-hoelder} that $$ \frac{y}{2} \le y' \,. @@ -6754,19 +6682,23 @@ \section{The classical Carleson theorem} $$ Using $y' \ge \frac{y}{2}$ and \Cref{lower-secant-bound}, we bound this by $$ - \le |y - y'| \sup_{\frac{y}{2} \le t \le 1} \frac{3}{|1 - e^{-it}|^2} \le 3 |y-y'| (8 \frac{2}{y})^2 \le 2^{10} \frac{|y-y'|}{|y|^2}\,. + \le |y - y'| \sup_{\frac{y}{2} \le t \le 1} \frac{3}{|1 - e^{-it}|^2} \le 3 |y-y'| (2 \frac{2}{y})^2 \le 2^{6} \frac{|y-y'|}{|y|^2}\,. $$ If $y \le 1$ and $y' > 1$, then $\kappa(-y') = 0$ and we have from the first case $$ - |\kappa(-y) - \kappa(-y')| = |\kappa(-y) - \kappa(-1)| \le 2^{10} \frac{|y-1|}{|y|^2} \le 2^{10} \frac{|y-y'|}{|y|^2}\,. + |\kappa(-y) - \kappa(-y')| = |\kappa(-y) - \kappa(-1)| \le 2^{6} \frac{|y-1|}{|y|^2} \le 2^{6} \frac{|y-y'|}{|y|^2}\,. + $$ + Similarly, if $y > 1$ and $y' \le 1$, then $\kappa(-y) = 0$ and we have from the first case $$ - Similarly, if $y > 1$ and $y' \le 1$, then $\kappa(-y) = 0$ and we have by the same computation as for the first case + |\kappa(-y) - \kappa(-y')| = |\kappa(-y') - \kappa(-1)| \le 2^{6} \frac{|y'-1|}{|y'|^2} \le 2^{6} \frac{|y-y'|}{|y'|^2}\,. $$ - |\kappa(-y) - \kappa(-y')| = |\kappa(-y') - \kappa(-1)| \le 2^{10} \frac{|y-1|}{|y|^2} \le 2^{10} \frac{|y-y'|}{|y|^2}\,. + Using again $y' \ge \frac{y}{2}$, we bound this by + $$ + \le 2^{6} \frac{|y-y'|}{|y / 2|^2} = 2^{8} \frac{|y-y'|}{|y|^2} $$ Finally, if $y, y' > 1$ then $$ - |\kappa(-y) - \kappa(-y')| = 0 \le 2^{10} \frac{|y-y'|}{|y|^2}\,. + |\kappa(-y) - \kappa(-y')| = 0 \le 2^{8} \frac{|y-y'|}{|y|^2}\,. $$ \end{proof} @@ -6775,215 +6707,66 @@ \section{The classical Carleson theorem} - - - -\section{Piecewise constant functions.} -\label{10piecewise} - - - - - - - - - -We first compute the partial Fourier sums for constant functions. - - -\begin{lemma}[constant function] -\label{constant-function} -\uses{mean-zero-oscillation} -If $h$ satisfies $h(x)=h(0)$ for all $x\in \R$, then for all $N\ge 0$ we have $S_Nh=h$. - \end{lemma} -\begin{proof} - We compute with \Cref{mean-zero-oscillation} for $n\in \mathbb{Z}$ with $n\neq 0$, - \begin{equation} - \widehat{h}_n=\frac 1{2\pi}\int_0^{2\pi}h(y)e^{-iny}\, dy=\frac {h(0)}{2\pi}\int_0^{2\pi}e^{-iny}\, dy=0\, . - \end{equation} -hence for $N\ge 0$ +\section{Smooth functions.} +\label{10smooth} +\begin{lemma} +\label{fourier-coeff-derivative} +\leanok +Let $f:\R \to \C$ be $2\pi$-periodic and differentiable, and let $n \in \Z \setminus \{0\}$. Then \begin{equation} - S_nh(x)=\sum_{n=-N}^N \widehat{h}_n e^{inx}=\widehat{h_0}=\frac{1}{2\pi}\int_0^{2\pi}h(y)\, dy - =\frac{h(0)}{2\pi}\int_0^{2\pi}\, dy=h(x)\, . + \widehat{f}_n = \frac{1}{i n} \widehat{f'}_n. \end{equation} -This proves the lemma. +\end{lemma} +\begin{proof} +\leanok +This is part of the Lean library. \end{proof} -\begin{lemma}[Dirichlet kernel bound] -\label{dirichlet-kernel-bound} -\uses{lower-secant-bound} -Let $\eta>0$. Let +\begin{lemma} +\label{convergence-of-coeffs-summable} +\leanok +Let $f:\R \to \C$ such that \begin{equation} - -2\pi +\eta \le \alpha < \beta \le 2\pi-\eta -\end{equation} -and assume -\begin{equation}\label{eq-abdelta} - [\alpha,\beta]\cap [-\eta,\eta]=\emptyset \, . + \sum_{n\in \Z} |\widehat{f}_n| < \infty. \end{equation} Then - \begin{equation}\label{dirichletint} - \left|\int_\alpha^\beta -\frac {e^{iNx}} {1-e^{-ix}} -dx\right| \le \frac{64}N(\frac{|\beta-\alpha|}{\eta^2}+\frac 1{\eta}). +\begin{equation} + \sup_{x\in [0,2\pi]} |f(x) - S_Nf(x)| \rightarrow 0 \end{equation} +as $N \rightarrow \infty$. \end{lemma} + \begin{proof} - Note first that the integral in \eqref{dirichletint} - is well defined as the denominator of the integrand is bounded away from zero by \Cref{lower-secant-bound} - and thus the integrand is continuous. - We have with partial integration -\begin{equation*} - \int_\alpha^\beta -\frac {e^{-iNx}} {1-e^{ix}}\, -dx -\end{equation*} -\begin{equation}\label{eq-part-int} -=\frac 1{-iN}\int_\alpha^\beta -{e^{-iNx}}\frac {ie^{ix}} {(1-e^{ix})^2}\, dx -+\left[ \frac 1{-iN} -\frac {e^{-iNx}} {1-e^{ix}}\right]_\alpha^\beta\, . -\end{equation} -We estimate the two summands in -\eqref{eq-part-int} separately. We have -for the first summand in \eqref{eq-part-int} -with \Cref{lower-secant-bound}, -\begin{equation*} -\left| \frac 1 {-iN}\int_\alpha^\beta -{e^{-iNx}}\frac{ie^{ix}} -{(1-e^{ix})^2}\, -dx \right| -\end{equation*} -\begin{equation}\label{firstpi} - \le \frac 1N \int_\alpha^\beta|1-e^{-ix}|^{-2} \, dx \le \frac {|\beta-\alpha|}N\sup_{x\in [\alpha,\beta]}|1-e^{-ix}|^{-2} -\end{equation} -\begin{equation} - \le \frac {64|\beta-\alpha|}{\eta^2N} -\end{equation} -We have for the second summand in \eqref{eq-part-int} -with \Cref{lower-secant-bound} again -\begin{equation*} - \left|\left[ \frac 1{-iN} - \frac {e^{-iNx}} {1-e^{ix}}\right]_\alpha^\beta\right| -\end{equation*} -\begin{equation}\label{secondpi} - \le \frac 1N (|1-e^{i\alpha}|^{-1}+|1-e^{i\beta}|^{-1}) - \le \frac {16}{\eta N}\, . -\end{equation} -Using the triangle inequality in \eqref{eq-part-int} -and applying the estimates \eqref{firstpi} and \eqref{secondpi} proves the lemma. +\leanok + This is part of the Lean library. \end{proof} - - -Let $\mathcal{G}$ be the class of $2\pi$-periodic measurable functions $g$ which satisfy for all $x\in \R$ -\begin{equation} - g(\frac{2\pi k(x)}K)=g(x) -\end{equation} -and +\begin{lemma} +\label{convergence-for-twice-contdiff} +\uses{convergence-of-coeffs-summable} +\leanok +Let $f:\R \to \C$ be $2\pi$-periodic and twice continuously differentiable. Then \begin{equation} - |g(x)|\le 2\, . -\end{equation} - - - -\begin{lemma}[flat interval partial sum] -\label{flat-interval-partial-sum} -\uses{dirichlet-kernel,dirichlet-kernel-bound} -Let $g\in \mathcal{G}$. Assume -$x\in [0,2\pi)\setminus E_1 $ and $g(x)=0$. -Then for all $N>\frac {2^{25} K^2}{\epsilon^3}$ -\begin{equation}\label{single-char-f} -|S_Ng(x)|\le \frac \epsilon 4\, , + \sup_{x\in [0,2\pi]} |f(x) - S_Nf(x)| \rightarrow 0 \end{equation} +as $N \rightarrow \infty$. \end{lemma} \begin{proof} - - - - - - - With \Cref{dirichlet-kernel}, breaking up the domain of integration into a - partition of subintervals, - \begin{equation*} - |S_N(g)|= \frac{1}{2\pi} \left|\int_{-\pi}^{\pi} g(y)K_N(x-y)\, dy\right| - \end{equation*} - \begin{equation}\label{eqcf1} - = \frac{1}{2\pi} \left|\sum_{k=0}^{K-1}\int_{\frac{2\pi k}K}^{\frac{2\pi (k+1)}K} g(y)K_N(x-y)\, dy\right|\, . - \end{equation} -Using $g\in \mathcal{G}$ and that $ k(y)=k$ for each -\begin{equation} - y\in [\frac {2\pi k}K, \frac{2\pi (k+1)}K)\, , -\end{equation} -and then applying the triangle inequality with the upper bound on $|g|$ and the identity $g(x)=g(2\pi k(x)/K)=0$, we estimate \eqref{eqcf1} by - \begin{equation*} - = \frac{1}{2\pi} \left|\sum_{k=0}^{K-1} g(\frac{2\pi k}K) \int_{\frac{2\pi k}K}^{\frac{2\pi (k+1)}K} K_N(x-y)\, dy\right| - \end{equation*} - \begin{equation}\label{eqcf3} - \le \frac{1}{\pi} \sum_{0\le k x$ and as $x\not \in E_1$ also -$2\pi k-\eta \ge x$. Hence $\beta \le -\eta $. If $\beta \ge 0$, then $2\pi k/K\le x$. As $k\neq k(x)$, we also have -$2\pi (k+1)/K\le x$. As $x\not \in E_1$, we have -$2\pi (k+1)/K+\eta \le x$. It follows that -$0<\alpha$. In both cases, we have seen -\eqref{eq-abdelta}. - - - -With \Cref{dirichlet-kernel} and the triangle inequality, -it follows that -\begin{equation} - \left|\int_{x-2\pi (k+1)/K}^{x-2\pi k/K} K_N(y)\, dy\right| - \le \left|\int_{\alpha}^{\beta} - \frac{e^{iNy}}{1-e^{-iy}}\, dy\right|+ - \left|\int_{\alpha}^{\beta} - \frac{e^{-iNy}}{1-e^{iy}}\, dy\right| -\end{equation} -Using that the two integrals on the right-hand side are complex conjugates of each other, and using \Cref{dirichlet-kernel-bound} and $\epsilon <2\pi$, this is bounded by -\begin{equation} - \le 2\left|\int_{\alpha}^{\beta} - \frac{e^{iNy}}{1-e^{-iy}}\, dy\right| - \le \frac{128}N(\frac{|\beta-\alpha|}{\eta^2}+\frac 1{\eta}) - \le \frac{2^{20}K}{N\epsilon^2 }\le 2^{-3}\epsilon K^{-1}\, . -\end{equation} -Inserting this in \eqref{eqcf3} and adding up proves -the lemma. +\leanok +By \Cref{convergence-of-coeffs-summable}, it suffices to show that the Fourier coefficients $\widehat{f}_n$ are summable. +Applying \Cref{fourier-coeff-derivative} twice and using the fact that $f''$ is continuous and thus bounded on $[0,2\pi]$ , we compute +\begin{equation*} + \sum_{n\in \Z} |\widehat{f}_n| = |\widehat{f}_0| + \sum_{n\in \Z \setminus \{0\}} \frac {1}{n^2} |\widehat{f''}_n| + \le |\widehat{f}_0| + \left(\sup_{x\in [0,2\pi]} |f(x)| \right) \cdot \sum_{n\in \Z \setminus \{0\}} \frac {1}{n^2} + < \infty. +\end{equation*} \end{proof} -We now prove \Cref{convergence-for-piecewise-constant}. - -Let $x\in [0,2\pi)\setminus E_1 $ and $N>\frac {2^{25} K^2}{\epsilon ^3}$. -Let $h$ be the function which is constant equal to $f_0(x)$ and let $g=f_0-h$. -By the bound on $f$ and the triangle inequality, -$|g|$ is bounded by $2$. Hence $g$ is in the class $\mathcal{G}$. We also have $g(x)=0$. -Using \Cref{constant-function}, we obtain -\begin{equation} - S_Nf_0(x)- f_0(x)=S_N(g+h)(x)- S_Nh(x)=S_Ng(x)\, . -\end{equation} -\Cref{convergence-for-piecewise-constant} -now follows by \Cref{flat-interval-partial-sum}. +\begin{proof} +\leanok +\proves{convergence-for-smooth} + \Cref{convergence-for-smooth} now follows directly from the previous \Cref{convergence-for-twice-contdiff}. +\end{proof} \section{Proof of Cotlar's Inequality} \label{subsec-cotlar} @@ -8382,13 +8165,21 @@ \section{Partial sums as orthogonal projections} \section{The error bound} \label{10difference} -We prove \Cref{control-approximation-effect}. Define + +%\begin{lemma} +%\label{control-approximation-effect} +%Let $h : \R \to \C$ be measurable, $2\pi$-periodic and +%\end{lemma} + +\begin{proof}[Proof of \Cref{control-approximation-effect}] +\leanok +Define $$ - E_2 := \{x \in [0, 2\pi) \ : \ \sup_{N > 0} |S_N f(x) - S_N f_0(x)| > \frac{\epsilon}{4} \}\,. + E := \{x \in [0, 2\pi) \ : \ \sup_{N > 0} |S_N f(x) - S_N f_0(x)| > \frac{\epsilon}{4} \}\,. $$ -Then \eqref{eq-max-partial-sum-diff} clearly holds, and it remains to show that $|E_2| \le \frac{\epsilon}{2}$. This will follow from \Cref{real-Carleson}. +Then \eqref{eq-max-partial-sum-diff} clearly holds, and it remains to show that $|E| \le \frac{\epsilon}{2}$. This will follow from \Cref{real-Carleson}. -Let $x \in E_2$. Then there exists $N > 0$ with +Let $x \in E$. Then there exists $N > 0$ with $$ |S_N f(x) - S_N f_0(x)| > \frac{\epsilon}{4}\,, $$ @@ -8419,19 +8210,19 @@ \section{The error bound} \end{equation} By \Cref{lower-secant-bound} with $\eta = |y|$, we have for $-1 \le y \le 1$ $$ - |e^{iNy}\frac{\min\{|y|, 1\} }{1 - e^{-iy}}| = \frac{|y|}{|1 - e^{iy}|} \le 8\,. + |e^{iNy}\frac{\min\{|y|, 1\} }{1 - e^{-iy}}| = \frac{|y|}{|1 - e^{iy}|} \le \frac \pi 2 \,. $$ By \Cref{lower-secant-bound} with $\eta = 1$, we have for $1 \le |y| \le \pi$ $$ - |e^{iNy}\frac{\min\{|y|, 1\} }{1 - e^{-iy}}| = \frac{1}{|1 - e^{iy}|} \le 8\,. + |e^{iNy}\frac{\min\{|y|, 1\} }{1 - e^{-iy}}| = \frac{1}{|1 - e^{iy}|} \le \frac \pi 2 \,. $$ Thus we obtain using the triangle inequality and \eqref{eq-ffzero} $$ - \eqref{eq-diff-integrable} \le \frac{16}{2\pi} \int_{-\pi}^{\pi} |f(x-y) - f_0(x-y)| \, dy \le 2^{4-2^{50}} \epsilon^2\,. + \eqref{eq-diff-integrable} \le \frac{1}{2} \int_{-\pi}^{\pi} |f(x-y) - f_0(x-y)| \, dy \le \pi\epsilon'. $$ Consequently, we have that $$ - \frac{\epsilon}{8} \le \frac{1}{2\pi} \left| \int_{-\pi}^{\pi} (f(x-y) - f_0(x-y)) (e^{iNy} \overline{\kappa}(y) + e^{-iNy}\kappa(y)) \, dy\right|\,. + \frac{\epsilon}{4} - \pi\epsilon' \le \frac{1}{2\pi} \left| \int_{-\pi}^{\pi} (f(x-y) - f_0(x-y)) (e^{iNy} \overline{\kappa}(y) + e^{-iNy}\kappa(y)) \, dy\right|\,. $$ By dominated convergence and since $\kappa(y) = 0$ for $|y| > 1$, this equals $$ @@ -8448,20 +8239,20 @@ \section{The error bound} $$ \le \frac{1}{2\pi} (Th(x) + T\bar{h}(x))\,. $$ -Thus for each $x \in E_2$, at least one of $Th(x)$ and $T\bar h(x)$ is larger than $\frac{\epsilon}{16}$. -Thus at least one of $Th$ and $T\bar h$ is $\ge \frac{\epsilon}{16}$ on a subset $E_2'$ of $E_2$ with $2|E_2'| \ge |E_2|$. Without loss of generality this is $Th$. By assumption \eqref{eq-ffzero}, we have $|2^{2^{50}}\epsilon^{-2} h| \le \mathbf{1}_{[-\pi, 3\pi]}$. Applying \Cref{real-Carleson} with $F = [-\pi, 3\pi]$ and $G = E_2'$, it follows that +Thus for each $x \in E$, at least one of $Th(x)$ and $T\bar h(x)$ is larger than $\frac{\pi(\epsilon - 4 \pi\epsilon')}{4}$. +Thus at least one of $Th$ and $T\bar h$ is $\ge \frac{\pi(\epsilon - 4 \pi\epsilon')}{4}$ on a subset $E'$ of $E$ with $2|E'| \ge |E|$. Without loss of generality this is $Th$. By assumption \eqref{eq-ffzero}, we have $|2^{2^{50}}\epsilon^{-2} h| \le \mathbf{1}_{[-\pi, 3\pi]}$. Applying \Cref{real-Carleson} with $F = [-\pi, 3\pi]$ and $G = E'$, it follows that $$ - \frac{\epsilon}{16} |E_2'| \le \int_{E_2'} Th(x) \, dx = 2^{-2^{50}}\epsilon^2 \int_{E_2'} T(2^{2^{50}}\epsilon^{-2} h)(x) \, dx + \frac{\pi(\epsilon - 4 \pi\epsilon')}{4} |E'| \le \int_{E'} Th(x) \, dx = \epsilon' \int_{E'} T(\epsilon'^{-1} h)(x) \, dx $$ $$ - \le 2^{-2^{50}} \epsilon^2 \cdot 2^{2^{40}} |F|^{\frac{1}{2}} |E_2'|^{\frac{1}{2}} \le 2^{-2^{40}} \frac{\epsilon^2}{16} |E_2'|^{\frac{1}{2}}\,. + \le \epsilon' \cdot C_{4,2} |F|^{\frac{1}{2}} |E'|^{\frac{1}{2}} \le (4\pi)^\frac{1}{2} C_{4,2} \epsilon' \cdot |E'|^{\frac{1}{2}}\,. $$ Rearranging, we obtain $$ - |E_2'| \le 2^{-2^{41}}\epsilon^2 \le \frac{\epsilon}{4}\,. + |E'| \le \left(\frac{4 (4\pi)^\frac{1}{2} C_{4,2} \epsilon'}{\pi(\epsilon - 4 \pi\epsilon')}\right)^2 = \frac{\epsilon}{2}\,. $$ -This completes the proof using $|E_2| \le 2|E_2'|$. - +This completes the proof using $|E| \le 2|E'|$. +\end{proof} @@ -8652,10 +8443,10 @@ \section{Carleson on the real line} \begin{proof} Let $m_1$ be the largest integer smaller than or equal to -$n-R'/2$. +$n- \frac {R'} {2R}$. Let $m_2=n$. Let $m_3$ be the smallest integer larger than -or equal to $n+R'/2$. +or equal to $n+ \frac {R'} {2R}$. Let $\mfa_{n'}\in B'$, then with \eqref{eqcarl4}, we have @@ -8663,8 +8454,7 @@ \section{Carleson on the real line} 2R|n-n'|< 2R'\, . \end{equation} -Assume first $n'\le n-R'/2$. By definition of $m_1$, -we have $n'\le m_1$. With \eqref{eqcarl6} +Assume first $n'\le m_1$. With \eqref{eqcarl6} we have \begin{equation*} R|m_1-n'|=R(m_1-n')=R(m_1-n)+R(n-n') @@ -8674,12 +8464,10 @@ \section{Carleson on the real line} \end{equation} We conclude $\mfa_{n'}\in B_1$. -Assume next $n-R'/2