VelocityRootProjection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Root projection inside an invariant velocity space

The extreme weight of a split diagonal isolates an off-diagonal matrix coefficient inside a closed invariant vector space. For the actual velocity space of a closed measure stabilizer, the isolated direction then gives an actual full real root group by the power approximation. This is the linear step after, rather than a substitute for, proving diagonal invariance of the component velocity spaces by recurrence.

lemma OAI.DukePrimeDegree.diagonal_matrix_conjugation_entry line 24
theorem OAI.DukePrimeDegree.tendsto_diagonal_matrix_root_projection line 37

theorem OAI.DukePrimeDegree.single_mem_of_diagonal_invariant_submodule line 80

Source documentation

Closedness is automatic for finite-dimensional real submodules. Every off-diagonal coefficient projects to a pure root direction.

theorem single_mem_of_diagonal_invariant_submodule {n : ℕ}
    (W : Submodule ℝ (Matrix (Fin n) (Fin n) ℝ))
    (hW : ∀ (ell : Fin n → ℝ) (hell : ∑ a, ell a = 0) (t : ℝ),
      ∀ V ∈ W, (diagonalOneParameter ell hell t).val * V *
        (diagonalOneParameter ell hell (-t)).val ∈ W)
    {V : Matrix (Fin n) (Fin n) ℝ} (hV : V ∈ W)
    (i j : Fin n) (hij : i ≠ j) : Matrix.single i j (V i j) ∈ W := by
…

theorem OAI.DukePrimeDegree.full_root_of_nonzero_component_velocity line 94

Source documentation

Diagonal invariance of the subgroup velocity space projects every nonzero off-diagonal velocity onto a full invariant root group.

theorem full_root_of_nonzero_component_velocity {n : ℕ}
    (L : Subgroup (G n)) (hclosed : IsClosed (L : Set (G n)))
    (hW : ∀ (ell : Fin n → ℝ) (hell : ∑ a, ell a = 0) (t : ℝ),
      ∀ V ∈ matrixVelocitySpace L, (diagonalOneParameter ell hell t).val * V *
        (diagonalOneParameter ell hell (-t)).val ∈ matrixVelocitySpace L)
    {V : Matrix (Fin n) (Fin n) ℝ} (hV : V ∈ matrixVelocitySpace L)
    (i j : Fin n) (hij : i ≠ j) (hijV : V i j ≠ 0) :
    ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ L := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace

theorem OAI.DukePrimeDegree.velocity_cross_entry_zero_of_no_new_roots line 111