OAI/NumberTheory/DukePrimeDegree/Geometry/RadialHeightContinuity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local constancy of controlled radial heights

Only the adjacent radial cuts determine the height. Avoiding all cuts up to the current height therefore makes the entire height itinerary locally constant along uniformly contracting perturbations.

  1. lemma OAI.DukePrimeDegree.cut_le_agrees_of_abs_sub_le line 18
  2. lemma OAI.DukePrimeDegree.height_eq_of_threshold_agreement line 30
  3. lemma OAI.DukePrimeDegree.eventually_radial_height_eq line 47
  4. theorem OAI.DukePrimeDegree.eventually_radial_height_itinerary_eq line 63