LDL decomposition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the LDL-decomposition of matricies: Any positive definite matrix S can be decomposed as S = LDLᴴ where L is a lower-triangular matrix and D is a diagonal matrix.

Main definitions #

LDL.lower is the lower triangular matrix L.
LDL.lower_inv is the inverse of the lower triangular matrix L.
LDL.diag is the diagonal matrix D.

Main result #

ldl_decomposition states that any positive definite matrix can be decomposed as LDLᴴ.

TODO #

Prove that LDL.lower is lower triangular from LDL.lower_inv_triangular.

source

noncomputable def LDL.lower_inv {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) :

matrix n n 𝕜

The inverse of the lower triangular matrix L of the LDL-decomposition. It is obtained by applying Gram-Schmidt-Orthogonalization w.r.t. the inner product induced by Sᵀ on the standard basis vectors pi.basis_fun.

Equations

LDL.lower_inv hS = gram_schmidt 𝕜 ⇑(pi.basis_fun 𝕜 n)

Instances for LDL.lower_inv

LDL.invertible_lower_inv

source

theorem LDL.lower_inv_eq_gram_schmidt_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) :

LDL.lower_inv hS = ((pi.basis_fun 𝕜 n).to_matrix ⇑(gram_schmidt_basis (pi.basis_fun 𝕜 n))).transpose

source

@[protected, instance]

noncomputable def LDL.invertible_lower_inv {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) :

invertible (LDL.lower_inv hS)

Equations

LDL.invertible_lower_inv hS = _.mpr ((pi.basis_fun 𝕜 n).to_matrix ⇑(gram_schmidt_basis (pi.basis_fun 𝕜 n))).invertible_transpose

source

theorem LDL.lower_inv_orthogonal {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) {i j : n} (h₀ : i ≠ j) :

has_inner.inner (⇑((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) (LDL.lower_inv hS i)) (⇑((pi_Lp.equiv 2 (λ (i : n), 𝕜)).symm) (S.transpose.mul_vec (LDL.lower_inv hS j))) = 0

source

noncomputable def LDL.diag_entries {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) :

n → 𝕜

The entries of the diagonal matrix D of the LDL decomposition.

Equations

LDL.diag_entries hS = λ (i : n), has_inner.inner (⇑((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) (has_star.star (LDL.lower_inv hS i))) (⇑((pi_Lp.equiv 2 (λ (i : n), 𝕜)).symm) (S.mul_vec (has_star.star (LDL.lower_inv hS i))))

source

noncomputable def LDL.diag {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) :

matrix n n 𝕜

The diagonal matrix D of the LDL decomposition.

Equations

LDL.diag hS = matrix.diagonal (LDL.diag_entries hS)

source

theorem LDL.lower_inv_triangular {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) {i j : n} (hij : i < j) :

LDL.lower_inv hS i j = 0

source

theorem LDL.diag_eq_lower_inv_conj {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) :

LDL.diag hS = ((LDL.lower_inv hS).mul S).mul (LDL.lower_inv hS).conj_transpose

Inverse statement of LDL decomposition: we can conjugate a positive definite matrix by some lower triangular matrix and get a diagonal matrix.

source

noncomputable def LDL.lower {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) :

matrix n n 𝕜

The lower triangular matrix L of the LDL decomposition.

Equations

LDL.lower hS = (LDL.lower_inv hS)⁻¹

source

theorem LDL.lower_conj_diag {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] [is_well_order n has_lt.lt] [locally_finite_order_bot n] {S : matrix n n 𝕜} [fintype n] (hS : S.pos_def) :

((LDL.lower hS).mul (LDL.diag hS)).mul (LDL.lower hS).conj_transpose = S

LDL decomposition: any positive definite matrix S can be decomposed as S = LDLᴴ where L is a lower-triangular matrix and D is a diagonal matrix.