OAI/NumberTheory/DukePrimeDegree/Geometry/SeparatedQuotientNet.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Separated quotient-distance nets

Thinning the existing quantitative net retains its cardinality bound and adds separation. This is the local packing input for controlling how many covering labels can meet one small image cell.

  1. lemma OAI.DukePrimeDegree.exists_separated_quotient_subnet line 19
  2. theorem OAI.DukePrimeDegree.exists_separated_quantitative_distance_net line 60