LU decomposition

TheoremLU decomposition without pivoting#✓fully proved

Let \(K\) be a field and \(A\) an \(n \times n\) matrix over \(K\) whose leading principal minors are all nonzero: for every \(k \le n\), the determinant of the upper-left \(k \times k\) block of \(A\) is nonzero. Then \(A = LU\) for some \(n \times n\) matrices \(L\) and \(U\) over \(K\) such that \(L\) is lower triangular with every diagonal entry equal to \(1\) and \(U\) is upper triangular.

Proof: Induct on the dimension and extend the factorization of the leading principal block by a bordered (Schur-complement) step. The statement is the existence half of Wikipedia, "LU decomposition", section "Existence and uniqueness".

theorem exists_lu_decomposition_of_minors_ne_zero (n : ℕ)
    (A : Matrix (Fin n) (Fin n) K)
    (h : ∀ (k : ℕ) (hk : k ≤ n),
      Matrix.det (A.submatrix (Fin.castLE hk) (Fin.castLE hk)) ≠ 0) :
    ∃ L U : Matrix (Fin n) (Fin n) K,
      L.IsLowerTriangular ∧ U.IsUpperTriangular ∧ (∀ i, L i i = 1) ∧ A = L * U

Sources

• L. N. Trefethen and D. Bau, Numerical Linear Algebra, SIAM (1997), Lecture 20.

TheoremUniqueness of the LU decomposition#✓fully proved

Let \(K\) be a field and \(A\) an invertible \(n \times n\) matrix over \(K\). Suppose \(A = L_1 U_1 = L_2 U_2\), where \(L_1\) and \(L_2\) are lower triangular \(n \times n\) matrices over \(K\) with every diagonal entry equal to \(1\), and \(U_1\) and \(U_2\) are upper triangular \(n \times n\) matrices over \(K\). Then \(L_1 = L_2\) and \(U_1 = U_2\).

Proof: Move the invertible triangular factors across the equality, then use the triangular inverse and diagonal formulas to show the resulting matrix is the identity. The statement is the uniqueness half of Wikipedia, "LU decomposition", section "Existence and uniqueness".

theorem lu_decomposition_unique (n : ℕ)
    (A L₁ L₂ U₁ U₂ : Matrix (Fin n) (Fin n) K)
    (hA : IsUnit A.det)
    (hL₁ : L₁.IsLowerTriangular) (hU₁ : U₁.IsUpperTriangular) (hd₁ : ∀ i, L₁ i i = 1)
    (hL₂ : L₂.IsLowerTriangular) (hU₂ : U₂.IsUpperTriangular) (hd₂ : ∀ i, L₂ i i = 1)
    (e₁ : A = L₁ * U₁) (e₂ : A = L₂ * U₂) :
    L₁ = L₂ ∧ U₁ = U₂

Sources

• L. N. Trefethen and D. Bau, Numerical Linear Algebra, SIAM (1997), Lecture 20.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.