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

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

Overlap implies distance

TileStructure.Forest.overlap_implies_distance

Plain-language statement

Let u1u2u_1\ne u_2 be forest tops with I(u1)I(u2)\mathcal I(u_1)\le\mathcal I(u_2). If a tile pp belongs to either tree and its spatial cube overlaps I(u1)\mathcal I(u_1), then the two top frequencies are separated at the scale of pp by

2Zn/2dp(Q(u1),Q(u2)).2^{Zn/2}\le d_p(\mathcal Q(u_1),\mathcal Q(u_2)).

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Square function count

TileStructure.Forest.square_function_count

Plain-language statement

Fix a cube JJ in the forest’s remaining-cube family. Consider grid cubes II at relative scale s(J)ss(J)-s', disjoint from the top cube I(u1)\mathcal I(u_1), whose enlarged balls meet JJ. The normalized average over JJ of the square of the number of those enlarged balls containing each point is bounded by the scale-dependent constant C(a,s)C(a,s').

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record