RootMatrixDensity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite distributions in a root conjugation representation

Root conjugation is polynomial of degree at most two in its parameter. Recurrence first kills the lower-left coefficient and then every linear coefficient. A finite invariant matrix distribution is therefore supported on the actual root centralizer.

lemma OAI.DukePrimeDegree.linear_coefficient_zero_of_recurrence line 20
lemma OAI.DukePrimeDegree.rootMatrixConjugation_add line 42
lemma OAI.DukePrimeDegree.rootMatrixConjugation_iterate line 56
lemma OAI.DukePrimeDegree.rootMatrixConjugation_entry line 65

theorem OAI.DukePrimeDegree.ae_commute_root_of_conjugation_invariance line 84

Source documentation

Root-conjugation recurrence forces every matrix to commute with the root, almost everywhere for any finite invariant distribution.

theorem ae_commute_root_of_conjugation_invariance {n : ℕ}
    (ν : Measure (Matrix (Fin n) (Fin n) ℝ)) [IsFiniteMeasure ν]
    (i j : Fin n) (hij : i ≠ j)
    (hinv : ν.map (rootMatrixConjugation i j 1) = ν) :
    ∀ᵐ M ∂ν, Commute M (Matrix.transvection i j (1 : ℝ)) := by
…

Mentions: OAI.DukePrimeDegree.rootMatrixConjugation