OAI/MeasureTheory/Falconer/Estimates/Packing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Packing bounds for the cap centers

Disjoint Euclidean balls give a bound independent of the number of chosen centers. This supplies the bounded-overlap count needed for a separated cap partition, and a polynomial global bound on the cap count.

  1. theorem OAI.Falconer.volume_real_ball line 17
  2. theorem OAI.Falconer.separated_ball_card line 23
  3. theorem OAI.Falconer.separated_sphere_overlap line 62