OAI/MeasureTheory/Falconer/Angular/CapNet.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A separated finite cap net with uniform local multiplicity

The cardinality maximization takes place in the natural numbers. It needs only the proved Euclidean packing bound, so no selection of infinitely many centers or measurable choice is involved.

  1. theorem OAI.Falconer.sphere_separated_card line 17
  2. theorem OAI.Falconer.finite_separated_cap_net line 34