FiniteOrbitDensity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Matrix density for finite-volume lattice orbits

The actual lattice orbit quotient carries a nonzero finite invariant measure. Conjugating any matrix which commutes with its stabilizer gives a finite invariant matrix measure. Recurrence under a regular split diagonal and the within-block root subgroups then forces the matrix into the block-scalar algebra. No homogeneous classification is assumed here.

lemma OAI.DukePrimeDegree.slMatrixConjugation_diagonal line 23
lemma OAI.DukePrimeDegree.slMatrixConjugation_root line 36

theorem OAI.DukePrimeDegree.centralizer_subset_blockScalar_of_finite_orbit line 47

Source documentation

The centralizer of the actual lattice stabilizer is contained in the block-scalar algebra whenever the finite-volume orbit group contains the split diagonal flow and the within-block roots.

theorem centralizer_subset_blockScalar_of_finite_orbit {n : ℕ}
    (g : G n) (H : Subgroup (G n))
    (μ : Measure (LatticeOrbitQuotient g H)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : H, μ.map (fun x => latticeOrbitRightAction g H x h) = μ)
    (ell : Fin n → ℝ) (hsum : ∑ i, ell i = 0) (hell : Function.Injective ell)
    (hdiag : ∀ t : ℝ, diagonalOneParameter ell hsum t ∈ H)
    (r : Setoid (Fin n))
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ H)
    (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : ∀ s : pointOrbitStabilizer g H, Commute M s.val.val) :
    M ∈ blockScalarAlgebra r := by
…

Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction, OAI.DukePrimeDegree.pointOrbitStabilizer, OAI.DukePrimeDegree.blockScalarAlgebra