WeakStableFactorization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Diagonal and unipotent coordinates of a weak stable displacement

theorem OAI.DukePrimeDegree.upper_triangular_positive_diagonal_factorization line 16

Source documentation

Positive upper triangular matrices split into a positive diagonal matrix and an actual ordered upper-root word.

theorem upper_triangular_positive_diagonal_factorization {n : ℕ} (g : G n)
    (htri : g.val.IsUpperTriangular) (hpos : ∀ i, 0 < g.val i i) :
    ∃ (v : Fin n → ℝ) (hv : ∑ i, v i=0) (u : UpperRootTime n),
      g=diagonalOneParameter v hv 1 * (completeRootChain n).word u := by
…

Mentions: OAI.DukePrimeDegree.UpperRootTime, OAI.DukePrimeDegree.completeRootChain

theorem OAI.DukePrimeDegree.small_weak_stable_factorization line 56

Source documentation

A sufficiently small future lift has a neutral diagonal part. Its remaining part belongs to the genuine strong stable unipotent group.

theorem small_weak_stable_factorization {n : ℕ}
    (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
    (hord : StrictMono ell) (g : G n) (hg : g ∈ matrixBall n 1)
    (hzero : ∀ i j, ell j < ell i → g.val i j=0) :
    ∃ (v : Fin n → ℝ) (hv : ∑ i, v i=0) (u : UpperRootTime n),
      g=diagonalOneParameter v hv 1 * (completeRootChain n).word u ∧
      ∀ t : ℝ, Commute (diagonalOneParameter v hv 1) (diagonalOneParameter ell hell t) := by
…

Mentions: OAI.DukePrimeDegree.UpperRootTime, OAI.DukePrimeDegree.completeRootChain