OAI/NumberTheory/DukePrimeDegree/Geometry/HorosphereChart.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Global coordinates on the contracting horosphere

The shared (i,j) entry belongs to the row coordinate. The remaining column coordinates vanish at both i and j. This gives an actual homeomorphism, with polynomial inverse, rather than only a parametrization.

  1. instance OAI.DukePrimeDegree.rootHorosphereTopology line 20
  2. abbrev OAI.DukePrimeDegree.HorosphereRow line 24
  3. abbrev OAI.DukePrimeDegree.HorosphereColumn line 25
  4. def OAI.DukePrimeDegree.horosphereCoordinates line 28
  5. def OAI.DukePrimeDegree.horosphereFromCoordinates line 34
  6. lemma OAI.DukePrimeDegree.horosphereFromCoordinates_coordinates line 40
  7. lemma OAI.DukePrimeDegree.horosphereCoordinates_fromCoordinates line 46
  8. lemma OAI.DukePrimeDegree.continuous_horosphereCoordinates line 67
  9. lemma OAI.DukePrimeDegree.continuous_horosphereFromCoordinates line 89
  10. def OAI.DukePrimeDegree.horosphereHomeomorph line 113