MautnerBlock.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A root fixed vector is fixed by its whole coordinate block

The ambient acting group is still the specified measure stabilizer. It only needs to contain the root groups inside the chosen coordinate set. The root-pair diagonal contracts every root touching its first pivot; commutators then supply the remaining roots of that coordinate block. This is the fixed-vector step for using a genuine unipotent ergodic flow on a component of one block group, without a diagonal-ergodicity premise.

lemma OAI.DukePrimeDegree.diagonalOneParameter_rootPair_eq line 24

theorem OAI.DukePrimeDegree.root_fixed_of_diagonal_fixed line 41

Source documentation

A diagonal group that fixes a vector also fixes each root with nonzero weight. The contracting times are chosen explicitly.

theorem root_fixed_of_diagonal_fixed {n : ℕ}
    (H : Subgroup (G n)) (ell : Fin n → ℝ) (hell : ∑ i, ell i = 0)
    (hD : ∀ t, diagonalOneParameter ell hell t ∈ H)
    {Y : Type*} [MetricSpace Y] [MulAction H Y] [ContinuousSMul H Y]
    [IsIsometricSMul H Y] (x : Y)
    (hfix : ∀ t : ℝ, (⟨diagonalOneParameter ell hell t, hD t⟩ : H) • x = x)
    {p q : Fin n} (hpq : p ≠ q)
    (hU : ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hpq t ∈ H)
    (hw : ell p ≠ ell q) (s : ℝ) :
    (⟨Matrix.SpecialLinearGroup.transvection hpq s, hU s⟩ : H) • x = x := by
…

theorem OAI.DukePrimeDegree.block_roots_fixed_of_one_root_fixed line 77

Source documentation

Only the roots with both endpoints in S are used. In particular, the theorem does not assert ergodicity of a root across distinct blocks.

theorem block_roots_fixed_of_one_root_fixed {n : ℕ}
    (S : Set (Fin n)) {i j : Fin n} (hij : i ≠ j) (hi : i ∈ S) (hj : j ∈ S)
    (H : Subgroup (G n))
    (hroot : ∀ p ∈ S, ∀ q ∈ S, ∀ (hpq : p ≠ q) (t : ℝ),
      Matrix.SpecialLinearGroup.transvection hpq t ∈ H)
    {Y : Type*} [MetricSpace Y] [MulAction H Y] [ContinuousSMul H Y]
    [IsIsometricSMul H Y] (x : Y)
    (hfix : ∀ t : ℝ,
      (⟨Matrix.SpecialLinearGroup.transvection hij t, hroot i hi j hj hij t⟩ : H) • x = x)
    (p : Fin n) (hp : p ∈ S) (q : Fin n) (hq : q ∈ S)
    (hpq : p ≠ q) (t : ℝ) :
    (⟨Matrix.SpecialLinearGroup.transvection hpq t, hroot p hp q hq hpq t⟩ : H) • x = x := by
…