OAI/NumberTheory/DukePrimeDegree/Geometry/QuantitativeDistanceNet.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative distance nets on logarithmic quotient balls

Finite matrix grids give nets for the intrinsic quotient distance. In the other direction a small quotient distance gives a small actual right lift, which is what the future-fiber construction needs.

  1. def OAI.DukePrimeDegree.quotientNetBound line 19
  2. theorem OAI.DukePrimeDegree.exists_quantitative_distance_net line 23
  3. theorem OAI.DukePrimeDegree.exists_matrix_lift_of_logDistance_lt line 53