OAI/MeasureTheory/Falconer/Shells/PositiveTerminal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Terminal bounds for the actual positive distance states

The profile is evaluated at integer depths in the recursive state. The regularized class stores its profile on [0,1], so the final theorem explicitly uses u ↦ m (u / N) when passing to that state.

  1. theorem OAI.Falconer.testedCellDistance_mass_le line 18
  2. theorem OAI.Falconer.positiveCollisionCount_mass_bound line 23
  3. theorem OAI.Falconer.positiveCollisionCount_regularized line 54
  4. theorem OAI.Falconer.positiveCollisionCount_terminal line 78