OAI/Analysis/LipschitzHilbert/Geometry/SourceScalePacking.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Separated-scale disjointness limits all boxes through a point to one fixed window of scales. This converts per-scale lattice counts into the uniform packing estimate used in the Bessel argument.

  1. theorem OAI.LipschitzHilbert.scale_window_packing line 15
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.length_scale_gap line 58