Project-declaredLean 4.32.0 · mathlib@81a5d257c8e4

Control approximation effect

control_approximation_effect

harmonic analysis Fourier analysis measure theory control approximation effect

Plain-language statement

Fix $1<p<2$ , an error threshold $\delta>0$ , and a measure tolerance $\varepsilon\ge0$ . There is an explicit bound $C(\delta,\varepsilon,p)$ such that, whenever a measurable $2\pi$ -periodic function $g$ satisfies $\lVert g\rVert_{L^p((0,2\pi])}\le C(\delta,\varepsilon,p)$ , the set where the maximal partial Fourier sum $\sup_N\lVert S_Ng(x)\rVert$ exceeds $\delta$ has measure at most $\varepsilon$ .

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 * π))) ≤ ε

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

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

Project: Carleson formalization
License: Apache-2.0
Commit: 74ef907d6bdb
Source: Carleson/Classical/ControlApproximationEffect.lean:157-230

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.0

Adjoint Carleson adjoint

adjointCarleson_adjoint

Plain-language statement

adjointCarleson is the adjoint of carlesonOn.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Ae tendsto zero of distribution le

ae_tendsto_zero_of_distribution_le

Plain-language statement

Suppose that, for every error threshold $\delta>0$ and every measure tolerance $\varepsilon>0$ , one can choose $N_0$ so that the set where $\sup_{N>N_0}\lVert f(x)-F_N(x)\rVert$ exceeds $\delta$ has measure at most $\varepsilon$ . Then $F_N(x)$ converges to $f(x)$ for almost every $x$ .

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Antichain operator

antichain_operator

Plain-language statement

For an antichain $\mathfrak{A}$ of pairwise incomparable tiles, and measurable functions $f$ and $g$ bounded by the indicators of $F$ and $G$ , the pairing of $g$ with the Carleson sum over $\mathfrak{A}$ is controlled by the $L^2$ norms of $f$ and $g$ and by positive powers of the two tile-density parameters. Concretely, the bound is

$C(a,q)\,\mathrm{dens}_1(\mathfrak{A})^{(q-1)/(8a^4)}\,\mathrm{dens}_2(\mathfrak{A})^{1/q-1/2}\,\lVert f\rVert_2\lVert g\rVert_2.$

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record