MautnerRootPair.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Mautner's root-pair calculation inside the actual acting subgroup

The subgroup parameter is essential: the ambient finite measure is not assumed invariant under all of SLₙ. The two opposite roots belong to its invariant block group, and the isometric action is restricted to that group. A concrete two-by-two identity supplies the diagonal fixed vector.

lemma OAI.DukePrimeDegree.root_pair_gauss_identity line 23

Source documentation

The elementary Gauss identity used in the Mautner argument.

lemma root_pair_gauss_identity {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (a s : ℝ) (ha : a ≠ 0) (hs : s ≠ 0) :
    Matrix.SpecialLinearGroup.transvection hij s *
      Matrix.SpecialLinearGroup.transvection hij.symm ((a - 1) / s) *
      Matrix.SpecialLinearGroup.transvection hij (-s / a) =
    Matrix.SpecialLinearGroup.transvection hij.symm ((a - 1) / (s * a)) *
      Matrix.SpecialLinearGroup.diag2n hij a ha := by
…

lemma OAI.DukePrimeDegree.diag2n_mem_of_opposite_roots line 45

theorem OAI.DukePrimeDegree.diag2n_fixed_of_root_fixed line 59

Source documentation

Root-fixed vectors are fixed by every nonzero root-pair diagonal. The large root parameters are never estimated directly; the isometry removes them before taking the limit.

theorem diag2n_fixed_of_root_fixed {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (H : Subgroup (G n))
    (hU : ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ H)
    (hV : ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij.symm t ∈ H)
    {Y : Type*} [MetricSpace Y] [MulAction H Y] [ContinuousSMul H Y]
    [IsIsometricSMul H Y]
    (x : Y) (hfix : ∀ t : ℝ,
      (⟨Matrix.SpecialLinearGroup.transvection hij t, hU t⟩ : H) • x = x)
    (a : ℝ) (ha : a ≠ 0) :
    (⟨Matrix.SpecialLinearGroup.diag2n hij a ha,
      diag2n_mem_of_opposite_roots hij H hU hV a ha⟩ : H) • x = x := by
…

Mentions: OAI.DukePrimeDegree.diag2n_mem_of_opposite_roots

lemma OAI.DukePrimeDegree.diag2n_conjugates_opposite_root line 104

theorem OAI.DukePrimeDegree.opposite_root_fixed_of_root_fixed line 132

Source documentation

In an isometric action of the actual root-pair subgroup, an upper root fixed vector is also fixed by the opposite root.

theorem opposite_root_fixed_of_root_fixed {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (H : Subgroup (G n))
    (hU : ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ H)
    (hV : ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij.symm t ∈ H)
    {Y : Type*} [MetricSpace Y] [MulAction H Y] [ContinuousSMul H Y]
    [IsIsometricSMul H Y]
    (x : Y) (hfix : ∀ t : ℝ,
      (⟨Matrix.SpecialLinearGroup.transvection hij t, hU t⟩ : H) • x = x)
    (t : ℝ) :
    (⟨Matrix.SpecialLinearGroup.transvection hij.symm t, hV t⟩ : H) • x = x := by
…