Schur triangulation

Schur triangulation is more commonly known as Schur decomposition or Schur triangularization, but "triangulation" makes the API more readable. It states that a square matrix over an algebraically closed field, e.g., ℂ, is unitarily similar to an upper triangular matrix.

Main definitions

• Matrix.schur_triangulation : a matrix A : Matrix n n 𝕜 with 𝕜 being algebraically closed can be decomposed as A = U * T * star U where U is unitary and T is upper triangular.
• Matrix.schurTriangulationUnitary : the unitary matrix U as previously stated.
• Matrix.schurTriangulation : the upper triangular matrix T as previously stated.
• Some auxiliary definitions are not meant to be used directly, but LinearMap.SchurTriangulationAux.of contains the main algorithm for the triangulation procedure.

@[inline]

def Fin.subNat' {m n : ℕ} (i : Fin (m + n)) (h : ¬↑i < m) : Fin n

subNat' i h subtracts m from i. This is an alternative form of Fin.subNat.

Equations

• i.subNat' h = Fin.subNat m (Fin.cast ⋯ i) ⋯

def Equiv.sumEquivSigmalCond {m n : ℕ} : Fin m ⊕ Fin n ≃ (b : Bool) × bif b then Fin m else Fin n

An alternative form of Equiv.sumEquivSigmaBool where Bool.casesOn is replaced by cond.

Equations

• One or more equations did not get rendered due to their size.

def Equiv.finAddEquivSigmaCond {m n : ℕ} : Fin (m + n) ≃ (b : Bool) × bif b then Fin m else Fin n

The composition of finSumFinEquiv and Equiv.sumEquivSigmalCond used by LinearMap.SchurTriangulationAux.of.

Equations

• Equiv.finAddEquivSigmaCond = finSumFinEquiv.symm.trans Equiv.sumEquivSigmalCond

theorem Equiv.finAddEquivSigmaCond_true {m n : ℕ} {i : Fin (m + n)} (h : ↑i < m) : finAddEquivSigmaCond i = ⟨true, ⟨↑i, h⟩⟩

theorem Equiv.finAddEquivSigmaCond_false {m n : ℕ} {i : Fin (m + n)} (h : ¬↑i < m) : finAddEquivSigmaCond i = ⟨false, i.subNat' h⟩

instance instFintypeCond_physLean {m n : Type u_1} [M : Fintype m] [N : Fintype n] (b : Bool) : Fintype (bif b then m else n)

The type family parameterized by Bool is finite if each type variant is finite.

Equations

• instFintypeCond_physLean b = Bool.rec N M b

instance instDecidableEqSigmaBoolCond_physLean {m n : Type u_1} [DecidableEq m] [DecidableEq n] : DecidableEq ((b : Bool) × bif b then m else n)

The type family parameterized by Bool has decidable equality if each type variant is decidable.

Equations

• instDecidableEqSigmaBoolCond_physLean ⟨true, snd⟩ ⟨false, snd_1⟩ = isFalse ⋯
• instDecidableEqSigmaBoolCond_physLean ⟨false, snd⟩ ⟨true, snd_1⟩ = isFalse ⋯
• instDecidableEqSigmaBoolCond_physLean ⟨false, i⟩ ⟨false, j⟩ = if h : i = j then isTrue ⋯ else isFalse ⋯
• instDecidableEqSigmaBoolCond_physLean ⟨true, i⟩ ⟨true, j⟩ = if h : i = j then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Matrix.IsUpperTriangular {n : Type u_1} {R : Type u_2} [LT n] [CommRing R] (A : Matrix n n R) : Prop

The property of a matrix being upper triangular. See also Matrix.det_of_upperTriangular.

Equations

• A.IsUpperTriangular = A.BlockTriangular id

@[reducible, inline]

abbrev Matrix.UpperTriangular (n : Type u_1) (R : Type u_2) [LT n] [CommRing R] : Type (max 0 u_1 u_2)

The subtype of upper triangular matrices.

Equations

• Matrix.UpperTriangular n R = { A : Matrix n n R // A.IsUpperTriangular }

structure LinearMap.SchurTriangulationAux {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : Module.End 𝕜 E) : Type (max u_1 u_2)

Don't use this definition directly. Instead, use Matrix.schurTriangulationBasis, Matrix.schurTriangulationUnitary, and Matrix.schurTriangulation. See also LinearMap.SchurTriangulationAux.of and Matrix.schurTriangulationAux.

• dim : ℕ

  The dimension of the inner product space E.

• hdim : Module.finrank 𝕜 E = self.dim
• basis : OrthonormalBasis (Fin self.dim) 𝕜 E

  An orthonormal basis of E that induces an upper triangular form for f.

• upperTriangular : ((toMatrix self.basis.toBasis self.basis.toBasis) f).IsUpperTriangular

Schur's recursive triangulation procedure

Given a linear endomorphism f on a non-trivial finite-dimensional vector space E over an algebraically closed field 𝕜, one can always pick an eigenvalue μ of f whose corresponding eigenspace V is non-trivial. Given that E is also an inner product space, let bV and bW be orthonormal bases for V and Vᗮ respectively. Then, the collection of vectors in bV and bW forms an orthonormal basis bE for E, as the direct sum of V and Vᗮ is an internal decomposition of E. The matrix representation of f with respect to bE satisfies $$ \sideset{_\mathrm{bE}}{_\mathrm{bE}}{[f]} = \begin{bmatrix} \sideset{_\mathrm{bV}}{_\mathrm{bV}}{[f]} & \sideset{_\mathrm{bW}}{_\mathrm{bV}}{[f]} \\ \sideset{_\mathrm{bV}}{_\mathrm{bW}}{[f]} & \sideset{_\mathrm{bW}}{_\mathrm{bW}}{[f]} \end{bmatrix} = \begin{bmatrix} \mu I & □ \\ 0 & \sideset{_\mathrm{bW}}{_\mathrm{bW}}{[f]} \end{bmatrix}, $$ which is upper triangular as long as $\sideset{_\mathrm{bW}}{_\mathrm{bW}}{[f]}$ is. Finally, one observes that the recursion from $\sideset{_\mathrm{bE}}{_\mathrm{bE}}{[f]}$ to $\sideset{_\mathrm{bW}}{_\mathrm{bW}}{[f]}$ is well-founded, as the dimension of bW is smaller than that of bE because bV is non-trivial.

However, in order to leverage DirectSum.IsInternal.collectedOrthonormalBasis, the type Σ b, cond b (Fin m) (Fin n) has to be used instead of the more natural Fin m ⊕ Fin n while their equivalence is propositionally established by Equiv.sumEquivSigmalCond.

@[irreducible]

noncomputable def LinearMap.SchurTriangulationAux.of {𝕜 : Type u_1} [RCLike 𝕜] [IsAlgClosed 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f : Module.End 𝕜 E) : SchurTriangulationAux f

Don't use this definition directly. This is the key algorithm behind Matrix.schur_triangulation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Matrix.schurTriangulationAux {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [IsAlgClosed 𝕜] [Fintype n] [DecidableEq n] [LinearOrder n] (A : Matrix n n 𝕜) : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n) × UpperTriangular n 𝕜

Don't use this definition directly. Instead, use Matrix.schurTriangulationBasis, Matrix.schurTriangulationUnitary, and Matrix.schurTriangulation for which this is their simultaneous definition. This is LinearMap.SchurTriangulationAux adapted for matrices in the Euclidean space.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Matrix.schurTriangulationBasis {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [IsAlgClosed 𝕜] [Fintype n] [DecidableEq n] [LinearOrder n] (A : Matrix n n 𝕜) : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)

The change of basis that induces the upper triangular form A.schurTriangulation of a matrix A over an algebraically closed field.

Equations

• A.schurTriangulationBasis = A.schurTriangulationAux.1

noncomputable def Matrix.schurTriangulationUnitary {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [IsAlgClosed 𝕜] [Fintype n] [DecidableEq n] [LinearOrder n] (A : Matrix n n 𝕜) : ↥(unitaryGroup n 𝕜)

The unitary matrix that induces the upper triangular form A.schurTriangulation to which a matrix A over an algebraically closed field is unitarily similar.

Equations

• A.schurTriangulationUnitary = ⟨(EuclideanSpace.basisFun n 𝕜).toBasis.toMatrix ⇑A.schurTriangulationBasis, ⋯⟩

noncomputable def Matrix.schurTriangulation {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [IsAlgClosed 𝕜] [Fintype n] [DecidableEq n] [LinearOrder n] (A : Matrix n n 𝕜) : UpperTriangular n 𝕜

The upper triangular form induced by A.schurTriangulationUnitary to which a matrix A over an algebraically closed field is unitarily similar.

Equations

• A.schurTriangulation = A.schurTriangulationAux.2

theorem Matrix.schur_triangulation {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [IsAlgClosed 𝕜] [Fintype n] [DecidableEq n] [LinearOrder n] (A : Matrix n n 𝕜) : A = ↑A.schurTriangulationUnitary * ↑A.schurTriangulation * ↑(star A.schurTriangulationUnitary)

Schur triangulation, Schur decomposition for matrices over an algebraically closed field. In particular, a complex matrix can be converted to upper-triangular form by a change of basis. In other words, any complex matrix is unitarily similar to an upper triangular matrix.