Project-declaredLean 4.32.0 · mathlib@81a5d257c8e4

Two sided metric carleson

two_sided_metric_carleson

harmonic analysis Fourier analysis measure theory main theorem

Plain-language statement

Let $1<q\le2$ and let $q'$ be its Hölder conjugate. Assume $a\ge4$ and that the truncated Calderón-Zygmund operators $T_r$ satisfy the required uniform strong $L^2$ estimate for every $r>0$ . If $F$ and $G$ are measurable and $f$ is measurable with $\lVert f(x)\rVert\le\mathbf{1}_F(x)$ , then the two-sided metric Carleson operator satisfies

$\int_G^+ \mathcal C_K f(x)\,dx\le C(a,q)\,\mu(G)^{1/q'}\mu(F)^{1/q}.$

Exact Lean statement

theorem two_sided_metric_carleson (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
    (hF : MeasurableSet F) (hG : MeasurableSet G)
    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a))
    {f : X → ℂ} (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
    ∫⁻ x in G, carlesonOperator K f x ≤
    C10_0_1 a q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem two_sided_metric_carleson (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')    (hF : MeasurableSet F) (hG : MeasurableSet G)    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a))    {f : X → ℂ} (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :    ∫⁻ x in G, carlesonOperator K f x ≤    C10_0_1 a q * (volume G) ^ (q' : ℝ)⁻¹ * (volume F) ^ (q : ℝ)⁻¹ := by  let c := (2 : ℝ) ^ (-2 * (a : ℝ) ^ 3)  have c_pos : 0 < c := Real.rpow_pos_of_pos two_pos _  have : IsOneSidedKernel a (c • K) := by    apply isOneSidedKernel_const_smul    unfold c    rw [neg_mul, Real.abs_rpow_of_nonneg two_pos.le, abs_two]    exact Real.rpow_le_one_of_one_le_of_nonpos one_le_two (by norm_num)  let : KernelProofData a (c • K) := by constructor <;> assumption  have : nontangentialOperator (c • K) = ‖c‖ₑ • nontangentialOperator K := by    convert! nontangentialOperator_const_smul (c : ℂ)    rw [← ofReal_norm, ← ofReal_norm, Complex.norm_real]  have HBST : HasBoundedStrongType (nontangentialOperator (c • K)) 2 2 volume volume (C_Ts a) := by    rw [this, ← ofReal_norm]    convert! HasBoundedStrongType.const_smul (nontangential_from_simple ha hT) ‖c‖.toNNReal    rw [C_Ts, C10_0_2_def, coe_pow, coe_ofNat, ← rpow_natCast, Nat.cast_pow, ENNReal.smul_def,      Real.norm_eq_abs, ofNNReal_toNNReal, abs_of_pos c_pos, ← ofReal_rpow_of_pos two_pos,      coe_pow, coe_ofNat, ← rpow_natCast, Nat.cast_mul, Nat.cast_ofNat, Nat.cast_pow,      ofReal_ofNat 2, smul_eq_mul, ← rpow_add _ _ (NeZero.ne 2) ENNReal.ofNat_ne_top]    ring_nf  rw [← ENNReal.mul_le_mul_iff_right (enorm_ne_zero.mpr c_pos.ne') enorm_ne_top,    ← lintegral_const_mul' _ _ enorm_ne_top, mul_assoc, ← mul_assoc, ← mul_assoc]  convert metric_carleson hq hqq' hF hG hmf hf HBST  · convert! congrFun (carlesonOperator_const_smul K f (c : ℂ)) _ |>.symm; simp  rw [C10_0_1, C_K, coe_mul, ← mul_assoc, ← ofReal_coe_nnreal, Real.enorm_eq_ofReal c_pos.le,    ← ofReal_mul c_pos.le, NNReal.coe_pow, NNReal.coe_rpow, NNReal.coe_ofNat,    ← Real.rpow_mul_natCast two_pos.le, ← Real.rpow_add two_pos,    ofReal_eq_one.mpr (by ring_nf; exact Real.rpow_zero 2), one_mul]

Project: Carleson formalization
License: Apache-2.0
Commit: 74ef907d6bdb
Source: Carleson/TwoSidedCarleson/MainTheorem.lean:30-62

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