Project-declaredLean 4.32.0 · mathlib@81a5d257c8e4

Two sided metric carleson has Lorentz Type

two_sided_metric_carleson_hasLorentzType

harmonic analysis Fourier analysis measure theory restricted weak type

Plain-language statement

Assume the phase space is countable, $a\ge4$ , $1<q<2$ , and every truncated Calderón-Zygmund operator $T_r$ has the required uniform strong $L^2$ bound. Then the two-sided metric Carleson operator is bounded from Lorentz $L^{q,1}$ to weak Lorentz $L^{q,\infty}$ , with the explicit project constant $4C(a,q)/q$ .

Exact Lean statement

theorem two_sided_metric_carleson_hasLorentzType [Countable (Θ X)] (ha : 4 ≤ a)
  (hq : q ∈ Ioo 1 2)
  (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :
    HasLorentzType (carlesonOperator K) q 1 q ⊤ volume volume (4 * (C10_0_1 a q) / q)

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem two_sided_metric_carleson_hasLorentzType [Countable (Θ X)] (ha : 4 ≤ a)  (hq : q ∈ Ioo 1 2)  (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :    HasLorentzType (carlesonOperator K) q 1 q ⊤ volume volume (4 * (C10_0_1 a q) / q) := by  have hqq' := NNReal.HolderConjugate.conjExponent hq.1  rename_i m kernel cf cancel count  have : IsOneSidedKernel a K := by infer_instance  set kpd : KernelProofData a K := KernelProofData.mk d ha cf this  apply (two_sided_metric_carleson_hasRestrictedWeakType ha (mem_Ioc_of_Ioo hq) hqq' hT).hasLorentzType    (by simpa) (by simp) (by simp) (C10_0_1_pos hq.1)  · intro f hf    apply (carlesonOperator_measurable _).aestronglyMeasurable    apply (hf.memLp _).locallyIntegrable <;> simp [hq.1.le]  · intro f g hf hg    filter_upwards with x    apply carlesonOperator_add_le_add_carlesonOperator    · apply (hf.memLp _).locallyIntegrable <;> simp [hq.1.le]    · apply (hg.memLp _).locallyIntegrable <;> simp [hq.1.le]  · intro a f    filter_upwards with x    rw [carlesonOperator_const_smul']    exact le_of_eq rfl  · intro f fs hf h_meas h_norm_monotone h_lim G    have hf : LocallyIntegrable f volume := by      apply (hf.memLp _).locallyIntegrable <;> simp [hq.1.le]    have bound {n : ℕ} : ∀ᵐ (a : X), ‖fs n a‖ ≤ ‖f a‖ := by      filter_upwards with x using (h_norm_monotone x).ge_of_tendsto (h_lim x).norm _    calc _      _ ≤ eLpNorm (fun x ↦ Filter.liminf (fun n ↦ carlesonOperator K (fs n) x) Filter.atTop) 1 (volume.restrict G) := by        apply eLpNorm_mono_enorm        intro x        apply carlesonOperator_le_liminf_carlesonOperator_of_tendsto (norm ∘ f)          (Filter.Eventually.of_forall h_meas) _ hf.norm (Filter.Eventually.of_forall h_lim)        filter_upwards; simpa      _ ≤ Filter.liminf (fun n ↦ eLpNorm (carlesonOperator K (fs n)) 1 (volume.restrict G)) Filter.atTop := by        rw [eLpNorm_one_eq_lintegral_enorm]        simp_rw [eLpNorm_one_eq_lintegral_enorm, enorm_eq_self]        apply lintegral_liminf_le        intro n        exact carlesonOperator_measurable (hf.mono (h_meas _) bound)    exact Filter.liminf_le_limsup  · simp  · intro f g hfg    filter_upwards with x    rw [carlesonOperator_congr_ae hfg]

Project: Carleson formalization
License: Apache-2.0
Commit: 74ef907d6bdb
Source: Carleson/TwoSidedCarleson/RestrictedWeakType.lean:49-93

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