OAI/NumberTheory/DukePrimeDegree/Geometry/HorosphereSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Horospherical support and leaf separation

The horospherical support property of EKL (2006), Lemma 4.4(1), together with separation along a root orbit gives Lemma 4.4(2). The support property follows from the root product theorem, Proposition 8.3 of Einsiedler--Katok (2003).

  1. theorem OAI.DukePrimeDegree.exists_horospherical_leaf_separation_of_root_support line 22