ConjugationOrbit.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Conjugation maps on actual lattice orbit quotients

A matrix commuting with the lattice stabilizer defines a continuous conjugation map on the corresponding homogeneous orbit quotient. Right invariance of a measure on that quotient gives conjugation invariance of its pushforward. This is the geometric bridge used by the elementary matrix-density argument.

def OAI.DukePrimeDegree.slMatrixConjugation line 23
lemma OAI.DukePrimeDegree.slMatrixConjugation_mul line 26
lemma OAI.DukePrimeDegree.slMatrixConjugation_one line 31
lemma OAI.DukePrimeDegree.slMatrixConjugation_eq_self line 35
lemma OAI.DukePrimeDegree.continuous_slMatrixConjugation line 41
def OAI.DukePrimeDegree.pointOrbitStabilizer line 47
Source documentation
The subgroup of the orbit group fixing the lattice represented by g.
```
def pointOrbitStabilizer {n : ℕ} (g : G n) (H : Subgroup (G n)) : Subgroup H :=
…
```
abbrev OAI.DukePrimeDegree.LatticeOrbitQuotient line 50
instance OAI.DukePrimeDegree.latticeOrbitQuotientMeasurableSpace line 53
instance OAI.DukePrimeDegree.latticeOrbitQuotientBorelSpace line 56
def OAI.DukePrimeDegree.latticeOrbitInverseHomeomorph line 59
instance OAI.DukePrimeDegree.latticeOrbitQuotientSecondCountable line 69
def OAI.DukePrimeDegree.latticeOrbitRightAction line 76
lemma OAI.DukePrimeDegree.continuous_latticeOrbitRightAction line 85
lemma OAI.DukePrimeDegree.latticeOrbitRightAction_transitive line 90
theorem OAI.DukePrimeDegree.latticeOrbit_support_eq_univ line 102
Source documentation
A nonzero invariant measure on the transitive orbit quotient has full support; full support is not a separate orbit assumption.
```
theorem latticeOrbit_support_eq_univ {n : ℕ} (g : G n) (H : Subgroup (G n))
    (μ : Measure (LatticeOrbitQuotient g H)) (hμ : μ ≠ 0)
    (hinv : ∀ h : H, μ.map (fun x => latticeOrbitRightAction g H x h) = μ) :
    μ.support = Set.univ := by
…
```
Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction
def OAI.DukePrimeDegree.conjugationOrbitMap line 119
Source documentation
The conjugation orbit map exists because its value is unchanged by the actual lattice point stabilizer.
```
def conjugationOrbitMap {n : ℕ} (g : G n) (H : Subgroup (G n))
    (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : ∀ s : pointOrbitStabilizer g H, Commute M s.val.val) :
    LatticeOrbitQuotient g H → Matrix (Fin n) (Fin n) ℝ :=
…
```
Mentions: OAI.DukePrimeDegree.pointOrbitStabilizer, OAI.DukePrimeDegree.LatticeOrbitQuotient
lemma OAI.DukePrimeDegree.continuous_conjugationOrbitMap line 136
lemma OAI.DukePrimeDegree.conjugationOrbitMap_rightAction line 144
lemma OAI.DukePrimeDegree.conjugationOrbitMap_identity line 153

theorem OAI.DukePrimeDegree.conjugationOrbitMap_map_invariant line 161

Source documentation

Invariant measure on the actual orbit quotient gives a finite dimensional conjugation-invariant distribution.

theorem conjugationOrbitMap_map_invariant {n : ℕ} (g : G n) (H : Subgroup (G n))
    (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : ∀ s : pointOrbitStabilizer g H, Commute M s.val.val)
    (μ : Measure (LatticeOrbitQuotient g H))
    (hinv : ∀ h : H, μ.map (fun x => latticeOrbitRightAction g H x h) = μ) (h : H) :
    (μ.map (conjugationOrbitMap g H M hM)).map (slMatrixConjugation h.val) =
      μ.map (conjugationOrbitMap g H M hM) := by
…

Mentions: OAI.DukePrimeDegree.pointOrbitStabilizer, OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction, OAI.DukePrimeDegree.conjugationOrbitMap, OAI.DukePrimeDegree.slMatrixConjugation