Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 60 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

60 results

Clear filters
Project-declaredLean 4.32.0

Le Carleson Operator Real

le_CarlesonOperatorReal

Plain-language statement

For x[0,2π]x\in[0,2\pi] and an interval-integrable function gg, the norm of the localized Dirichlet-kernel integral over [xπ,x+π][x-\pi,x+\pi], with cutoff max(1xy,0)\max(1-|x-y|,0), is bounded by the sum of the real Carleson operators applied to gg and to its complex conjugate.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Lebesgue differentiation

lebesgue_differentiation

Plain-language statement

For every bounded, finitely supported function ff, almost every point xx admits a sequence of balls B(ci,ri)B(c_i,r_i) that all contain xx, whose radii tend to 00 from above, and whose averages converge to f(x)f(x):

\dashintB(ci,ri)f(y)dyf(x).\dashint_{B(c_i,r_i)} f(y)\,dy\longrightarrow f(x).

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Linearized metric carleson

linearized_metric_carleson

Plain-language statement

Let 1<q21 < q \le 2 and let qq' be its Hölder conjugate. If every phase-linearized nontangential operator has the required uniform L2L^2 bound, then for measurable F,GF,G and measurable ff with f(x)1F(x)\lVert f(x)\rVert \le \mathbf{1}_F(x), the linearized Carleson operator satisfies

G+CQ,Klinf(x)dxC(a,q)μ(G)1/qμ(F)1/q.\int_G^+ \mathcal{C}^{\mathrm{lin}}_{Q,K}f(x)\,dx \le C(a,q)\,\mu(G)^{1/q'}\mu(F)^{1/q}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Lintegral enorm carleson Sum le of is Antichain subset ℭ

lintegral_enorm_carlesonSum_le_of_isAntichain_subset_ℭ

Plain-language statement

Let A\mathfrak A be an antichain contained in the tile class C(k,n)\mathfrak C(k,n), and let ff be measurable with f(x)1F(x)\lVert f(x)\rVert\le\mathbf 1_F(x). On GGG\setminus G', the Carleson sum over the selected positive tiles in A\mathfrak A has an L1L^1 bound with exponential decay in the layer index nn:

GG+ ⁣CarlesonSumf(x)dxC(a,q)μ(G)11/qμ(F)1/q2((q1)/(8a4))n.\int_{G\setminus G'}^+\!\lVert\operatorname{CarlesonSum}f(x)\rVert\,dx\le C(a,q)\,\mu(G)^{1-1/q}\mu(F)^{1/q}\,2^{-((q-1)/(8a^4))n}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Lipschitz On With of i Lip ENorm ne top

LipschitzOnWith.of_iLipENorm_ne_top

Plain-language statement

If the project’s inhomogeneous Lipschitz norm of φ\varphi on the ball B(z,R)B(z,R) is finite, then φ\varphi is Lipschitz on that ball. A valid Lipschitz constant is the finite normalized norm divided by RR.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Maximal bound antichain

maximal_bound_antichain

Plain-language statement

At every point xx, the magnitude of the Carleson sum over an antichain of tiles is bounded by a constant depending on aa times a maximal function of ff. The maximal function uses, for each tile pp, a ball centered at the tile center with radius 8Ds(p)8D^{\mathfrak{s}(p)}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record