OAI/MeasureTheory/Falconer/Radial/UniformOuterRadial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A common outer-radial cutoff for all contact exponents above a fixed positive floor

  1. theorem OAI.Falconer.eventually_radial_mean_coefficient_uniform line 12
  2. theorem OAI.Falconer.eventually_radial_collision_mean_uniform line 44
  3. theorem OAI.Falconer.outer_radial_interval_pruning_uniform line 68