OAI/NumberTheory/DukePrimeDegree/Geometry/SmallUpperRootAtlas.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Countably many small upper-root boxes

Both the relative group displacement and the transverse logarithmic coordinates are controlled on each box. The radius can be chosen before the atlas, as required by the height-dependent injectivity estimates.

  1. theorem OAI.DukePrimeDegree.exists_small_upperRoot_product line 19
  2. theorem OAI.DukePrimeDegree.exists_small_upperRootBox_at line 65
  3. theorem OAI.DukePrimeDegree.exists_countable_small_upperRoot_atlas line 87