OAI/Analysis/LipschitzHilbert/Geometry/FarGroupEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The far-group energy estimate: the actual selected family, localized by its representative's popularity projection, has total overlap at most 80 times representative length times reference width.

  1. theorem OAI.LipschitzHilbert.SelectedFarFamily.group_overlap_bound line 15