Project-declaredLean 4.32.0 · mathlib@81a5d257c8e4

Adjoint Carleson adjoint

adjointCarleson_adjoint

harmonic analysis Fourier analysis measure theory operators

Plain-language statement

adjointCarleson is the adjoint of carlesonOn.

Exact Lean statement

lemma adjointCarleson_adjoint
    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (p : 𝔓 X) :
    ∫ x, conj (g x) * carlesonOn p f x = ∫ y, conj (adjointCarleson p g y) * f y

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma adjointCarleson_adjoint    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (p : 𝔓 X) :    ∫ x, conj (g x) * carlesonOn p f x = ∫ y, conj (adjointCarleson p g y) * f y := by  let H := fun x ↦ fun y ↦ conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y * f y  have hH : Integrable (uncurry H) := by    let H₀ := fun x y ↦ ‖g x‖ * ‖f y‖    obtain ⟨M₀, hM₀nn, hM₀⟩ := hg.hasCompactSupport.isBounded.exists_bound_of_norm_Ks (𝔰 p)    have hHleH₀ x y : ‖H x y‖ ≤ M₀ * ‖g x‖ * ‖f y‖ := by      by_cases h : x ∈ tsupport g      · unfold H        rw [norm_mul, norm_mul, norm_mul, norm_conj]        nth_rw 2 [mul_assoc, mul_comm]        gcongr        apply mul_le_mul (norm_indicator_one_le ..) norm_MKD_le_norm_Ks (by simp) (by simp) |>.trans        linarith [hM₀ x y h]      · suffices hz : H x y = 0 by rw [hz]; simp only [norm_zero, ge_iff_le]; positivity        unfold H; simp [image_eq_zero_of_notMem_tsupport h]    have : Integrable (fun z : X × X ↦ M₀ * ‖g z.1‖ * ‖f z.2‖) :=      (hg.norm.const_mul _).integrable.mul_prod hf.norm.integrable    apply this.mono    · refine .mul ?_ hf.aestronglyMeasurable.comp_snd      refine .mul ?_ ?_      · refine .mul ?_ ?_        · exact RCLike.continuous_conj.comp_aestronglyMeasurable hg.aestronglyMeasurable.comp_fst        · exact aestronglyMeasurable_const.indicator measurableSet_E |>.comp_fst      · unfold MKD        fun_prop    · apply ae_of_all      exact fun z ↦ (hHleH₀ z.1 z.2).trans <| Real.le_norm_self _  calc    _ = ∫ x, conj (g x) * ∫ y, (E p).indicator 1 x * MKD (𝔰 p) x y * f y := by      congr 1; ext x; congr 1      rw [carlesonOn, indicator_eq_indicator_one_mul, ← smul_eq_mul, ← integral_smul]      congr 1; ext y; unfold MKD; simp [smul_eq_mul]; ring    _ = ∫ x, ∫ y, H x y := by      unfold H; congr 1; ext x      calc conj (g x) * ∫ y, (E p).indicator 1 x * MKD (𝔰 p) x y * f y          = ∫ y, conj (g x) * ((E p).indicator 1 x * MKD (𝔰 p) x y * f y) :=            (integral_const_mul _ _).symm        _ = ∫ y, conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y * f y := by            congr 1; ext y; ring    _ = ∫ y, ∫ x, H x y := integral_integral_swap hH    _ = ∫ y, (∫ x, conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y) * f y := by      simp_rw [H]; congr 1; ext y      exact integral_mul_const _ _    _ = ∫ y, conj (∫ x, g x * (E p).indicator 1 x * conj (MKD (𝔰 p) x y)) * f y := by      congr 1; ext y; congr 1      have h : ∀ x, conj (g x) * (E p).indicator 1 x * MKD (𝔰 p) x y =          conj (g x * (E p).indicator 1 x * conj (MKD (𝔰 p) x y)) :=        fun x => by rw [map_mul, conj_conj, map_mul, conj_indicator, map_one]      simp_rw [h]      exact integral_conj    _ = _ := by      congr! with y      simp_rw [mul_comm (g _) _]      calc        _ = ∫ x, (E p).indicator (fun x ↦ g x * conj (MKD (𝔰 p) x y)) x := by          congr with x; simp only [indicator]; split_ifs <;> simp        _ = ∫ x in E p, g x * conj (MKD (𝔰 p) x y) := integral_indicator measurableSet_E        _ = ∫ x in E p, conj (MKD (𝔰 p) x y) * g x := by congr; funext; rw [mul_comm]        _ = _ := by          unfold adjointCarleson MKD          congr; funext; rw [map_mul, ← exp_conj, mul_comm (cexp _)]          congr; simp; ring

Project: Carleson formalization
License: Apache-2.0
Commit: 74ef907d6bdb
Source: Carleson/Operators.lean:337-400

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

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

Project-declaredLean 4.32.0

Antichain operator

antichain_operator'

Plain-language statement

For an antichain $\mathfrak A$ , a measurable set $A\subseteq G$ , and measurable $f$ bounded by $\mathbf 1_F$ , the norm of the Carleson sum has the integral estimate

$\int_A^+\lVert\operatorname{CarlesonSum}_{\mathfrak A}f(x)\rVert\,dx\le 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\,\mu(G)^{1/2}.$

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record