Documentation

Mathlib.LinearAlgebra.Matrix.LDL

LDL decomposition #

This file proves the LDL-decomposition of matrices: 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.lowerInv {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) :
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.basisFun.

Equations
Instances For
    theorem LDL.lowerInv_eq_gramSchmidtBasis {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) :
    LDL.lowerInv hS = ((Pi.basisFun ๐•œ n).toMatrix โ‡‘(gramSchmidtBasis (Pi.basisFun ๐•œ n))).transpose
    noncomputable instance LDL.invertibleLowerInv {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) :
    Equations
    theorem LDL.lowerInv_orthogonal {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) {i : n} {j : n} (hโ‚€ : i โ‰  j) :
    inner ((WithLp.equiv 2 (n โ†’ ๐•œ)).symm (LDL.lowerInv hS i)) ((WithLp.equiv 2 (n โ†’ ๐•œ)).symm (S.transpose.mulVec (LDL.lowerInv hS j))) = 0
    noncomputable def LDL.diagEntries {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) :
    n โ†’ ๐•œ

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

    Equations
    Instances For
      noncomputable def LDL.diag {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) :
      Matrix n n ๐•œ

      The diagonal matrix D of the LDL decomposition.

      Equations
      Instances For
        theorem LDL.lowerInv_triangular {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) {i : n} {j : n} (hij : i < j) :
        LDL.lowerInv hS i j = 0
        theorem LDL.diag_eq_lowerInv_conj {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) :
        LDL.diag hS = LDL.lowerInv hS * S * (LDL.lowerInv hS).conjTranspose

        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} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) :
        Matrix n n ๐•œ

        The lower triangular matrix L of the LDL decomposition.

        Equations
        Instances For
          theorem LDL.lower_conj_diag {๐•œ : Type u_1} [RCLike ๐•œ] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] [LocallyFiniteOrderBot n] {S : Matrix n n ๐•œ} [Fintype n] (hS : S.PosDef) :
          LDL.lower hS * LDL.diag hS * (LDL.lower hS).conjTranspose = 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.