OAI/Analysis/LipschitzHilbert/Geometry/SelectedFarOverlap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The far-pair overlap estimate for an actual rectangle selection, combining popular-projection packing with the group energy bound.

  1. theorem OAI.LipschitzHilbert.selected_far_overlap line 12