OAI/MeasureTheory/Falconer/Radial/RegularClassRadialBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform profile cancellation in the actual class ball bound

  1. theorem OAI.Falconer.Regularization.radialClassBallBound_le line 12
  2. theorem OAI.Falconer.Regularization.eventually_radialClassBallBound_le line 30
  3. theorem OAI.Falconer.weak_radial_reciprocal_count line 44
  4. theorem OAI.Falconer.eventually_weak_radial_reciprocal_budget line 53