OAI/NumberTheory/DukePrimeDegree/Geometry/HorosphereDiagonal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Diagonal normalization and contraction of the root horosphere

The closed group of shearing limits is normalized by the diagonal group, and the two-coordinate shearing diagonal contracts it. These are the group facts needed to construct its conditional measures.

  1. theorem OAI.DukePrimeDegree.rootHorosphereShape_diagonal_conjugate line 21
  2. theorem OAI.DukePrimeDegree.rootHorosphereShape_transvection line 33
  3. theorem OAI.DukePrimeDegree.rootHorosphere_tendsto_one line 46