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

1 topic

130 results

Clear filters
Project-declaredLean 4.32.0

Third tree pointwise

TileStructure.Forest.third_tree_pointwise

Plain-language statement

For a tree in the forest, a point xx in a boundary cube LL, and a bounded compactly supported function ff, the oscillatory sum of the error fapproxOnCube(f)f-\operatorname{approxOnCube}(f) over the relevant scales is bounded pointwise by a constant times the tree’s boundary operator applied to the cube-wise approximation of f|f|, evaluated at any other point xLx'\in L.

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

Two sided metric carleson has Lorentz Type

two_sided_metric_carleson_hasLorentzType

Plain-language statement

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

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Van der Corput

van_der_Corput

Plain-language statement

Let φ\varphi be KK-Lipschitz and bounded in norm by BB on (a,b)(a,b). For every integer frequency nn,

abeinxφ(x)dx2π(ba)(B+K(ba)2)(1+n(ba))1.\left\lVert\int_a^b e^{inx}\varphi(x)\,dx\right\rVert \le 2\pi(b-a)\left(B+\frac{K(b-a)}2\right)\left(1+|n|(b-a)\right)^{-1}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record