Project-declaredLean 4.32.0
Forest separation
forest_separation
Plain-language statement
Let and be distinct forest tops at level . If a tile belongs to the tree rooted at and its spatial cube lies below the spatial cube of , then its phase center is quantitatively far from that of at the scale of :
harmonic analysisFourier analysismeasure theory
Source project: Carleson formalization
Person-level attribution pending.