OAI/MeasureTheory/Falconer/Geometry/BallTruncation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Enforcing ball bounds by deleting points of excessive local mass

  1. theorem OAI.Falconer.measurable_ball_mass line 14
  2. theorem OAI.Falconer.ball_mass_pair_integral line 25
  3. theorem OAI.Falconer.excessive_ball_mass line 34
  4. theorem OAI.Falconer.restricted_good_ball_bound line 50