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

S truncation

S_truncation

Plain-language statement

Let 1<q21<q\le2, let qq' be its Hölder conjugate, and suppose the linearized nontangential operators have the required uniform L2L^2 bound. For bounded measurable F,GF,G and measurable ff with f(x)1F(x)\lVert f(x)\rVert\le\mathbf 1_F(x), the supremum over all truncated scale intervals Bs1s2B-B\le s_1\le s_2\le B satisfies

G+sups1s2Ts1,s2f(x)dxC(a,q)μ(G)1/qμ(F)1/q.\int_G^+\sup_{s_1\le s_2}\lVert T_{s_1,s_2}f(x)\rVert\,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

Tile sum operator

tile_sum_operator

Plain-language statement

For xGGx\in G\setminus G', summing the localized Carleson contribution over all tiles is exactly the same as summing the corresponding oscillatory kernel integral over the integer scales from σ1(x)\sigma_1(x) to σ2(x)\sigma_2(x). This is the identity that converts the discrete tile model back into the finitary operator.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Uncertainty

Tile.uncertainty'

Plain-language statement

Consider two tiles p1,p2p_1,p_2 with s(p1)s(p2)\mathfrak s(p_1)\le\mathfrak s(p_2) whose enlarged spatial balls overlap. If xix_i lies in the active set E(pi)E(p_i), then the separation of the two tile frequencies, measured at the scale of p1p_1, is controlled by the separation of the selected phases Q(x1)Q(x_1) and Q(x2)Q(x_2):

1+dp1(Q(p1),Q(p2))C(a)(1+dx1,Ds(p1)(Q(x1),Q(x2))).1+d_{p_1}(\mathcal Q(p_1),\mathcal Q(p_2))\le C(a)\bigl(1+d_{x_1,D^{\mathfrak s(p_1)}}(Q(x_1),Q(x_2))\bigr).

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Dist χ le

TileStructure.Forest.dist_χ_le

Plain-language statement

For two distinct forest tops u1,u2u_1,u_2 with nested spatial cubes, and for a comparison cube JJ, the cutoff function χu1,u2,J\chi_{u_1,u_2,J} is Lipschitz on I(u1)\mathcal I(u_1) at the scale of JJ:

d(χ(x),χ(x))C(a)d(x,x)Ds(J).d\bigl(\chi(x),\chi(x')\bigr)\le C(a)\,\frac{d(x,x')}{D^{s(J)}}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

E728

TileStructure.Forest.e728

Plain-language statement

The pairing of a tree boundary operator applied to ff with a test function gg is bounded by a sum over boundary cubes JJ. Each term integrates f|f| times a maximal function of gg over JJ, multiplied by a scale-decaying sum over grid cubes II whose enlarged balls contain JJ and whose scale is at least that of JJ.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Local dens1 tree bound

TileStructure.Forest.local_dens1_tree_bound

Plain-language statement

For a tree t(u)t(u) and one of its boundary cubes LL, the measure of the part of LGL\cap G covered by the active sets EpE_p of tiles in the tree is at most

C(a)dens1(t(u))μ(L).C(a)\,\mathrm{dens}_1(t(u))\,\mu(L).

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record