OAI/NumberTheory/DukePrimeDegree/Geometry/LocalQuotientPacking.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform local packing after rescaling a quotient chart

The number of separated points in a fixed multiple of a sufficiently small chart is bounded independently of the chart radius and base point. The proof uses the existing finite matrix grid and actual right lifts.

  1. def OAI.DukePrimeDegree.localQuotientPackingBound line 19
  2. theorem OAI.DukePrimeDegree.local_quotient_packing_bound line 22
  3. lemma OAI.DukePrimeDegree.local_quotient_packing_finset_bound line 108
  4. lemma OAI.DukePrimeDegree.local_quotient_distance_packing_bound line 126