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

Forest separation

forest_separation

Plain-language statement

Let uu and uu' be distinct forest tops at level (k,n,j)(k,n,j). If a tile pp belongs to the tree rooted at uu' and its spatial cube lies below the spatial cube of uu, then its phase center is quantitatively far from that of uu at the scale of pp:

2Z(n+1)<dp(Q(p),Q(u)).2^{Z(n+1)}<d_p(\mathcal Q(p),\mathcal Q(u)).

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record