OAI/Analysis/LipschitzHilbert/Geometry/SelectedCountingEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual selected rectangle count has the Lacey--Li second moment bound. Both near and far overlaps have been proved from non-removal.

  1. theorem OAI.LipschitzHilbert.selected_counting_energy line 13