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 2 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

2 results

Clear filters
Project-declaredLean 4.32.0

Discrete carleson

discrete_carleson

Plain-language statement

There is a measurable exceptional set GGG'\subseteq G with 2μ(G)μ(G)2\mu(G')\le\mu(G) such that every measurable ff bounded by 1F\mathbf{1}_F satisfies

GG+CarlesonSumf(x)dxC(a,q)μ(G)11/qμ(F)1/q.\int_{G\setminus G'}^+\lVert\operatorname{CarlesonSum}f(x)\rVert\,dx\le C(a,q)\mu(G)^{1-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

Two sided metric carleson

two_sided_metric_carleson

Plain-language statement

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

G+CKf(x)dxC(a,q)μ(G)1/qμ(F)1/q.\int_G^+ \mathcal C_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