OAI/MeasureTheory/Falconer/Estimates/ScalarBunchMargins.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Each discarded porous level contributes a full block of geometric separation. These bounds use the actual increasing endpoint indices.

  1. theorem OAI.Falconer.scalar_increasing_endpoint_gap line 9
  2. theorem OAI.Falconer.scalar_bunch_margin line 14
  3. theorem OAI.Falconer.scalar_bunch_long_margin line 21