LatticeGroupDecomposition.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The lattice group action and its ergodic components

Taking inverses writes the right lattice action as a left action. Measurable ergodic decomposition gives probability components for each closed matrix subgroup preserving the measure. Adjoining an invariant subgroup to the diagonal action preserves invariance and ergodicity of a diagonal-ergodic probability, as required by Margulis--Tomanov.

instance OAI.DukePrimeDegree.latticeSubgroupInverseAction line 24
Source documentation
The left action corresponding to the actual right lattice action.
```
instance latticeSubgroupInverseAction {n : ℕ} (H : Subgroup (G n)) :
    MulAction H (X n) where
…
```
instance OAI.DukePrimeDegree.latticeSubgroupInverseAction_continuous line 35
lemma OAI.DukePrimeDegree.latticeSubgroup_preserving line 42

theorem OAI.DukePrimeDegree.lattice_subgroup_ergodic_decomposition line 49

Source documentation

Measurable ergodic decomposition for the lattice action of a closed subgroup preserving the probability measure.

theorem lattice_subgroup_ergodic_decomposition {n : ℕ}
    (H : Subgroup (G n)) (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (hH : H ≤ invariantRightSubgroup μ) :
    ∃ (m : MeasurableSpace (X n)) (hm : m ≤ xMeasurableSpace n),
      letI : MeasurableSpace (X n) := xMeasurableSpace n
…

def OAI.DukePrimeDegree.diagonalAdjoinedGroup line 61
Source documentation
The subgroup generated by A and a prescribed invariant subgroup.
```
def diagonalAdjoinedGroup (d : ℕ) (H : Subgroup (G (d + 1))) : Subgroup (G (d + 1)) :=
…
```
lemma OAI.DukePrimeDegree.diagonal_mem_diagonalAdjoinedGroup line 64
lemma OAI.DukePrimeDegree.subgroup_le_diagonalAdjoinedGroup line 68
lemma OAI.DukePrimeDegree.diagonalAdjoinedGroup_preserves line 72

theorem OAI.DukePrimeDegree.diagonalAdjoinedGroup_ergodic line 84

Source documentation

Diagonal ergodicity implies ergodicity for the group generated by the diagonal group and an invariant subgroup.

theorem diagonalAdjoinedGroup_ergodic (d : ℕ) (H : Subgroup (G (d + 1)))
    (μ : Measure (X (d + 1)))
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (hH : H ≤ invariantRightSubgroup μ) :
    ErgodicSMul (diagonalAdjoinedGroup d H) (X (d + 1)) μ := by
…

Mentions: OAI.DukePrimeDegree.diagonalAdjoinedGroup