control_approximation_effect
Carleson.Classical.ControlApproximationEffect · Carleson/Classical/ControlApproximationEffect.lean:157 to 230
Source documentation
The constant used in C_control_approximation_effect. -/
def C_control_approximation_effect (δ ε p : ℝ≥0) : ℝ≥0 :=
min (2 * (↑δ / 2) * ((2 * Real.toNNReal π) ^ (1 - p.toReal⁻¹))⁻¹)
(C_distribution_carlesonOperatorReal_le (2 * π * (↑δ / 2) / 2).toNNReal (ε / 2) p)
lemma C_control_approximation_effect_pos {δ ε p : ℝ≥0} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_control_approximation_effect δ ε p := lt_min (by positivity) (C_distribution_carlesonOperatorReal_le_pos (by positivity) (by positivity))
lemma C_control_approximation_effect_property {δ ε p : ℝ≥0} (hp : 1 ≤ p) : C_control_approximation_effect δ ε p * (2 * ENNReal.ofReal π) ^ (1 - p.toReal⁻¹) ≤ 2 * (↑δ / 2) := by calc _ _ ≤ 2 * (↑δ / 2) * ((2 * Real.toNNReal π) ^ (1 - p.toReal⁻¹))⁻¹ * (2 * ENNReal.ofReal π) ^ (1 - p.toReal⁻¹) := by gcongr norm_cast exact min_le_left _ _ _ = 2 * (↑δ / 2) := by rw [ENNReal.coe_inv (by simp [Real.pi_pos]), ENNReal.coe_rpow_of_nonneg _ (by simp only [sub_nonneg]; exact inv_le_one_of_one_le₀ hp), ENNReal.coe_mul, ENNReal.coe_ofNat, ENNReal.ofNNReal_toNNReal, ENNReal.inv_mul_cancel_right (by positivity) (ENNReal.rpow_ne_top' (by positivity) (ENNReal.mul_ne_top (by simp) (by simp)))]
lemma C_control_approximation_effect_le {δ ε p : ℝ≥0} : ENNReal.ofNNReal (C_control_approximation_effect δ ε p) ≤ (C_distribution_carlesonOperatorReal_le (2 * π * (↑δ / 2) / 2).toNNReal (ε / 2) p) := by simp only [ENNReal.coe_le_coe] exact min_le_right _ _
/- This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint.
Exact Lean statement
lemma control_approximation_effect {δ ε : ℝ≥0} (δpos : 0 < δ)
{g : ℝ → ℂ} (g_measurable : AEStronglyMeasurable g)
(g_periodic : g.Periodic (2 * π))
{p : ℝ≥0} (hp : p ∈ Set.Ioo 1 2)
(g_bound : eLpNorm g p (volume.restrict (Set.Ioc 0 (2 * π))) ≤ C_control_approximation_effect δ ε p) :
distribution (fun x ↦ ⨆ N, ‖S_ N g x‖ₑ) δ (volume.restrict (Set.Ioc 0 (2 * π))) ≤ εComplete declaration
Lean source
lemma control_approximation_effect {δ ε : ℝ≥0} (δpos : 0 < δ) {g : ℝ → ℂ} (g_measurable : AEStronglyMeasurable g) (g_periodic : g.Periodic (2 * π)) {p : ℝ≥0} (hp : p ∈ Set.Ioo 1 2) (g_bound : eLpNorm g p (volume.restrict (Set.Ioc 0 (2 * π))) ≤ C_control_approximation_effect δ ε p) : distribution (fun x ↦ ⨆ N, ‖S_ N g x‖ₑ) δ (volume.restrict (Set.Ioc 0 (2 * π))) ≤ ε := by calc _ _ ≤ distribution (operatorBound g) δ (volume.restrict (Set.Ioc 0 (2 * π))) := by apply distribution_mono_left rw [ae_restrict_iff' (measurableSet_Ioc)] filter_upwards with x hx simp only [enorm_eq_self, iSup_le_iff] intro N apply partialFourierSum_bound g_periodic _ (Set.Ioc_subset_Icc_self hx) rw [intervalIntegrable_iff_integrableOn_Ioc_of_le Real.two_pi_pos.le, IntegrableOn] apply MemLp.integrable (q := p) (by simp [hp.1.le]) use g_measurable.restrict exact g_bound.trans_lt (by simp) _ = distribution (operatorBound g) (δ / 2 + δ / 2) (volume.restrict (Set.Ioc 0 (2 * π))) := by congr simp _ ≤ distribution (fun x ↦ (T g x + T (conj ∘ g) x) / ENNReal.ofReal (2 * π)) (δ / 2) (volume.restrict (Set.Ioc 0 (2 * π))) + distribution (fun x ↦ eLpNorm g 1 (volume.restrict (Set.Ioc 0 (2 * π))) / 2) (δ / 2) (volume.restrict (Set.Ioc 0 (2 * π))) := by apply distribution_add_le _ ≤ ε + 0 := by gcongr · rw [← distribution_mul (by left; exact ENNReal.ofReal_ne_top) (by left; simp [Real.pi_pos])] calc _ _ ≤ distribution (T g) (ENNReal.ofReal (2 * π) * (↑δ / 2) / 2) (volume.restrict (Set.Ioc 0 (2 * π))) + distribution (T (conj ∘ g)) (ENNReal.ofReal (2 * π) * (↑δ / 2) / 2) (volume.restrict (Set.Ioc 0 (2 * π))) := by apply distribution_add_le.trans' gcongr · simp rw [← two_mul, ENNReal.mul_div_cancel (by simp) (by simp)] _ ≤ ENNReal.ofNNReal (ε / 2) + ENNReal.ofNNReal (ε / 2) := by have : ENNReal.ofReal (2 * π) * (↑δ / 2) / 2 = ENNReal.ofReal ((2 * π) * (↑δ / 2) / 2) := by rw [ENNReal.ofReal_div_of_pos (by simp), ENNReal.ofReal_mul (by simp), ENNReal.ofReal_mul Real.two_pi_pos.le, ENNReal.ofReal_mul (by simp), ENNReal.ofReal_ofNat, ENNReal.ofReal_div_of_pos (by simp), ENNReal.ofReal_ofNat] simp rw [this] gcongr · apply distribution_carlesonOperatorReal_le (by positivity) hp g_periodic g_measurable exact g_bound.trans C_control_approximation_effect_le · have conj_g_periodic : (conj ∘ g).Periodic (2 * π) := by intro x simp only [Function.comp_apply] congr 1 apply g_periodic have conj_g_measurable : AEStronglyMeasurable (conj ∘ g) := by fun_prop have conj_g_bound : eLpNorm (conj ∘ g) p (volume.restrict (Set.Ioc 0 (2 * π))) ≤ C_control_approximation_effect δ ε p := by convert g_bound using 1 apply eLpNorm_congr_norm_ae simp apply distribution_carlesonOperatorReal_le (by positivity) hp conj_g_periodic conj_g_measurable exact conj_g_bound.trans C_control_approximation_effect_le _ = ε := by simp · rw [← distribution_mul (by simp) (by simp)] simp only [nonpos_iff_eq_zero] rw [Function.const_def, distribution_const, Set.indicator_of_notMem] simp only [enorm_eq_self, Set.mem_Iio, not_lt] have hp' : (1 : ENNReal) ≤ p := by simp [hp.1.le] apply (eLpNorm_le_eLpNorm_mul_rpow_measure_univ hp' g_measurable.restrict).trans rw [Measure.restrict_apply_univ, Real.volume_Ioc] simp only [sub_zero, Nat.ofNat_nonneg, ENNReal.ofReal_mul, ENNReal.ofReal_ofNat, ENNReal.toReal_one, ne_eq, one_ne_zero, not_false_eq_true, div_self, ENNReal.coe_toReal, one_div] apply (C_control_approximation_effect_property hp.1.le).trans' gcongr _ = ε := by simp