Source indexedlemma · leanprover/lean4:v4.32.0

control_approximation_effect'

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:177 to 249

Source documentation

The constant used in C_control_approximation_effect'. -/ def C_control_approximation_effect' (δ ε : ℝ≥0) : ℝ≥0 := min (δ / toNNReal (2 * π)) (C_distribution_carlesonOperatorReal_le' (2 * π * (↑δ / 2) / 2).toNNReal (ε / 2))

--TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx lemma C_control_approximation_effect'_pos {δ ε : ℝ≥0} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_control_approximation_effect' δ ε := lt_min (by positivity) (C_distribution_carlesonOperatorReal_le'_pos (by positivity) (by positivity))

--TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx lemma C_control_approximation_effect'_property {δ ε : ℝ≥0} : C_control_approximation_effect' δ ε * ENNReal.ofReal (2 * π) ≤ δ := by unfold C_control_approximation_effect' rw [ENNReal.coe_min, min_mul, ENNReal.coe_div (by positivity), ENNReal.ofReal, ENNReal.div_mul_cancel (by positivity) (by simp)] exact min_le_left _ _

--TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx lemma C_control_approximation_effect'_le {δ ε : ℝ≥0} : C_control_approximation_effect' δ ε ≤ C_distribution_carlesonOperatorReal_le' (2 * π * (↑δ / 2) / 2).toNNReal (ε / 2) := by exact min_le_right _ _

--TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx /- This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint.

Exact Lean statement

lemma control_approximation_effect' {δ ε : ℝ≥0} (δpos : 0 < δ) (εpos : 0 < ε)
  {g : ℝ → ℂ} (g_measurable : Measurable g)
  (g_periodic : g.Periodic (2 * π))
  (g_bound : ∀ x, ‖g x‖ ≤ C_control_approximation_effect' δ ε) :
    distribution (fun x ↦ ⨆ N, ‖S_ N g x‖ₑ) δ (volume.restrict (Set.Ioc 0 (2 * π))) ≤ ε

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma control_approximation_effect' {δ ε : ℝ≥0} (δpos : 0 < δ) (εpos : 0 < ε)  {g : ℝ → ℂ} (g_measurable : Measurable g)  (g_periodic : g.Periodic (2 * π))  (g_bound : ∀ x, ‖g x‖ ≤ C_control_approximation_effect' δ ε) :    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)      exact intervalIntegrable_of_bdd g_measurable g_bound    _ = 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 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) (by positivity)                g_measurable              intro x              exact (g_bound x).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 : Measurable (conj ∘ g) := by fun_prop              have conj_g_bound :  ∀ (x : ℝ), ‖(conj ∘ g) x‖ ≤ ↑(C_control_approximation_effect' δ ε) := by                simpa              apply distribution_carlesonOperatorReal_le' (by positivity) (by positivity)                conj_g_measurable              intro x              exact (conj_g_bound x).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]        rw [eLpNorm_one_eq_lintegral_enorm]        calc _          _ ≤ ∫⁻ (x : ℝ) in Set.Ioc 0 (2 * π), ↑(C_control_approximation_effect' δ ε) := by            apply setLIntegral_mono measurable_const            intro x _            rw [← ofReal_norm, ENNReal.ofReal_le_coe]            exact g_bound x          _ ≤ ↑(C_control_approximation_effect' δ ε) * ENNReal.ofReal (2 * π) := by            rw [setLIntegral_const, Real.volume_Ioc, sub_zero]          _ ≤ δ := C_control_approximation_effect'_property          _ = 2 * (δ / 2) := by            rw [ENNReal.mul_div_cancel (by simp) (by simp)]    _ = ε := by simp