LatticeSpace.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The homogeneous space and diagonal flow

We use the column-lattice convention SL(n,ℝ) / SL(n,ℤ). Inversion identifies this with the manuscript's row-lattice convention SL(n,ℤ) \ SL(n,ℝ) and turns right diagonal translations into left translations by the inverse. No packet or Haar probability is assumed to have been constructed by these definitions.

abbrev OAI.DukePrimeDegree.RealSL line 25
instance OAI.DukePrimeDegree.(instance at line 27) line 27
def OAI.DukePrimeDegree.integralSL line 33
Source documentation
The integer special linear group inside the real group.
```
def integralSL (n : ℕ) : Subgroup (RealSL n) :=
…
```
Mentions: OAI.DukePrimeDegree.RealSL
instance OAI.DukePrimeDegree.integralSL_closed line 36
abbrev OAI.DukePrimeDegree.LatticeSpace line 41
Source documentation
The unimodular lattice space, with its quotient topology.
```
abbrev LatticeSpace (n : ℕ) := RealSL n ⧸ integralSL n
```
Mentions: OAI.DukePrimeDegree.RealSL, OAI.DukePrimeDegree.integralSL
instance OAI.DukePrimeDegree.(instance at line 43) line 43
instance OAI.DukePrimeDegree.(instance at line 45) line 45
instance OAI.DukePrimeDegree.(instance at line 47) line 47
instance OAI.DukePrimeDegree.(instance at line 49) line 49
def OAI.DukePrimeDegree.diagonalParameters line 52
Source documentation
Deleted-log-coordinate-free parametrization of the positive diagonal group.
```
def diagonalParameters (n : ℕ) : Submodule ℝ (Fin n → ℝ) where
…
```
def OAI.DukePrimeDegree.diagonalExp line 65
Source documentation
The determinant-one exponential diagonal matrix.
```
noncomputable def diagonalExp {n : ℕ} (u : diagonalParameters n) : RealSL n :=
…
```
Mentions: OAI.DukePrimeDegree.diagonalParameters, OAI.DukePrimeDegree.RealSL
lemma OAI.DukePrimeDegree.diagonalExp_zero line 69
lemma OAI.DukePrimeDegree.diagonalExp_add line 74
def OAI.DukePrimeDegree.diagonalHom line 86
Source documentation
The positive diagonal action, encoded as a homomorphism to the ambient group.
```
noncomputable def diagonalHom (n : ℕ) :
    Multiplicative (diagonalParameters n) →* RealSL n where
…
```
Mentions: OAI.DukePrimeDegree.diagonalParameters, OAI.DukePrimeDegree.RealSL
instance OAI.DukePrimeDegree.(instance at line 92) line 92
def OAI.DukePrimeDegree.diagonalFlow line 97
Source documentation
Time t of the one-parameter diagonal flow associated with u.
```
noncomputable def diagonalFlow {n : ℕ} (u : diagonalParameters n)
    (t : ℝ) (x : LatticeSpace n) : LatticeSpace n :=
…
```
Mentions: OAI.DukePrimeDegree.diagonalParameters, OAI.DukePrimeDegree.LatticeSpace
lemma OAI.DukePrimeDegree.diagonalFlow_zero line 101
lemma OAI.DukePrimeDegree.diagonalFlow_add line 105
lemma OAI.DukePrimeDegree.continuous_diagonalFlow line 110
lemma OAI.DukePrimeDegree.measurable_diagonalFlow line 113