OAI/MeasureTheory/Falconer/Shells/DecayEndgame.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The monotone original-law endgame with bounds at the same scale

  1. theorem OAI.Falconer.summable_shift_one line 12
  2. theorem OAI.Falconer.positive_volume_of_same_scale_summable line 15
  3. theorem OAI.Falconer.positive_volume_of_same_scale_decay line 33