mathlib3 documentation

linear_algebra.matrix.ldl

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 #

Main result #

TODO #

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
Instances for LDL.lower_inv
@[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) :
Equations
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
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
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
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

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

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
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 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.