OAI/NumberTheory/DukePrimeDegree/Geometry/ControlledRadialHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Proper radial heights with controlled boundary strips

Well-separated radial thresholds can be chosen with one common strip bound. The corresponding integer height is proper and has unit jumps under the prescribed right translation.

  1. theorem OAI.DukePrimeDegree.exists_controlled_radial_height line 19