OAI/MeasureTheory/Falconer/Geometry/PointBallCounts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transfer finite prefix bounds to geometric closed-ball counts. The factor 7^d is the existing bounded overlap of dyadic cubes.

  1. def OAI.Falconer.pointPrefixFiber line 11
  2. theorem OAI.Falconer.pointPrefixFiber_card_eq line 16
  3. theorem OAI.Falconer.finite_point_ball_count line 21