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

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