OAI/NumberTheory/DukePrimeDegree/Dynamics/HorosphereIsolatingFlow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Isolating a peripheral root of the shearing horosphere

Each noncentral row or column coordinate can be left unchanged by a trace-zero diagonal flow which contracts all other horospherical coordinates. The resulting conjugates converge to that single root.

  1. def OAI.DukePrimeDegree.centerWeights line 20
  2. lemma OAI.DukePrimeDegree.centerWeights_sum line 23
  3. lemma OAI.DukePrimeDegree.centerWeights_sub line 30
  4. def OAI.DukePrimeDegree.rowIsolatingRaw line 35
  5. def OAI.DukePrimeDegree.columnIsolatingRaw line 38
  6. lemma OAI.DukePrimeDegree.rowIsolatingRaw_equal line 41
  7. lemma OAI.DukePrimeDegree.columnIsolatingRaw_equal line 45
  8. lemma OAI.DukePrimeDegree.rowIsolatingRaw_negative line 49
  9. lemma OAI.DukePrimeDegree.columnIsolatingRaw_negative line 65