Project-declaredLean 4.32.0
Overlap implies distance
TileStructure.Forest.overlap_implies_distance
Plain-language statement
Let be forest tops with . If a tile belongs to either tree and its spatial cube overlaps , then the two top frequencies are separated at the scale of by
harmonic analysisFourier analysismeasure theory
Source project: Carleson formalization
Person-level attribution pending.