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.

All topics

60 results

Clear filters
Project-declaredLean 4.32.0

Measurable lco Convergent

measurable_lcoConvergent

Plain-language statement

For measurable ff with f(x)1\lVert f(x)\rVert\le1, the scale-nn quantity lcoConvergent, which records a supremum of truncated linearized Carleson integrals over rational radii, is a measurable function of xx.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Metric carleson

metric_carleson

Plain-language statement

Let 1<q21 < q \le 2 and let qq' be its Hölder conjugate. In the project’s cancellative metric-space setting, assume the associated nontangential operators satisfy the required uniform L2L^2 bound. 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 Carleson operator obeys the restricted estimate

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
Project-declaredLean 4.32.0

Near 1 geometric bound

near_1_geometric_bound

Plain-language statement

For 0t10\le t\le1, the reciprocal of 12t1-2^{-t} is controlled in the extended nonnegative reals by

(12t)12t1.(1-2^{-t})^{-1}\le 2t^{-1}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Partial Fourier Sum L2 norm

partialFourierSumL2_norm

Plain-language statement

For an L2L^2 function on a circle of period TT, the squared L2L^2 norm of its NNth partial Fourier sum equals the sum of the squared magnitudes of its Fourier coefficients from N-N through NN:

SNf22=n=NNf^(n)2.\lVert S_Nf\rVert_2^2=\sum_{n=-N}^{N}|\widehat f(n)|^2.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Rcarleson general

rcarleson_general

Plain-language statement

Let 1<q21<q\le2 and let qq' be its Hölder conjugate. For measurable sets F,GRF,G\subseteq\mathbb{R} and measurable ff with f(x)1F(x)\lVert f(x)\rVert\le\mathbf{1}_F(x), the real-line Carleson operator satisfies

G+Tf(x)dxC(q)μ(G)1/qμ(F)1/q.\int_G^+ T f(x)\,dx \le C(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

Right Continuous integral annulus

rightContinuous_integral_annulus

Plain-language statement

If ff is integrable on the open annulus {y:R1<d(x,y)<R2}\{y:R_1<d(x,y)<R_2\}, then varying the inner radius from the right changes the annular integral continuously at R1R_1:

RR<d(x,y)<R2f(y)dyR\longmapsto\int_{R<d(x,y)<R_2}f(y)\,dy

is right-continuous at R=R1R=R_1.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record