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

1 topic
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