Cholesky factors of positive-definite real matrices

This file constructs the lower-triangular Cholesky factor of a positive-definite real matrix from Mathlib's LDL decomposition. The diagonal of the LDL factor is positive, so taking its entrywise square root and absorbing it into the lower factor gives S = L * Lᵀ, with L lower triangular and positive on the diagonal.

Main definitions

• TauCeti.PosDiagLowerTriangular is the space of lower-triangular real matrices with positive diagonal.
• TauCeti.cholesky constructs the Cholesky factor of a positive-definite matrix, and TauCeti.cholesky_coe gives its closed form in terms of the LDL decomposition.
• TauCeti.cholesky_mul_transpose proves the Cholesky reconstruction identity.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Section 7.2.

@[reducible, inline]

abbrev TauCeti.PosDiagLowerTriangular (p : ℕ) : Type

Lower-triangular real matrices of size p whose diagonal entries are positive.

Equations

• TauCeti.PosDiagLowerTriangular p = { L : Matrix (Fin p) (Fin p) ℝ // L.IsLowerTriangular ∧ ∀ (i : Fin p), 0 < L i i }

noncomputable def TauCeti.cholesky {p : ℕ} (A : PosDefMatrix p) : PosDiagLowerTriangular p

The lower-triangular Cholesky factor of a positive-definite real symmetric matrix.

Equations

• TauCeti.cholesky A = ⟨TauCeti.Matrix.choleskyFactor✝ ⋯, ⋯⟩

theorem TauCeti.cholesky_coe {p : ℕ} (A : PosDefMatrix p) : ↑(cholesky A) = LDL.lower ⋯ * Matrix.diagonal fun (i : Fin p) => √(LDL.diagEntries ⋯ i)

The Cholesky factor of A in closed form: Mathlib's LDL lower factor of A, with the square roots of the LDL diagonal entries absorbed into its columns.

@[simp]

theorem TauCeti.cholesky_mul_transpose {p : ℕ} (A : PosDefMatrix p) : ↑(cholesky A) * (↑(cholesky A)).transpose = ↑↑A

A positive-definite matrix is the product of its Cholesky factor and its transpose.

theorem TauCeti.PosDiagLowerTriangular.vecMul_injective {p : ℕ} (L : PosDiagLowerTriangular p) : Function.Injective fun (v : Fin p → ℝ) => Matrix.vecMul v ↑L

A lower-triangular matrix with positive diagonal has linearly independent rows.

noncomputable def TauCeti.choleskyReconstruction {p : ℕ} (L : PosDiagLowerTriangular p) : PosDefMatrix p

Reconstruct a positive-definite symmetric matrix from a lower-triangular matrix with positive diagonal.

Equations

• TauCeti.choleskyReconstruction L = ⟨⟨↑L * (↑L).transpose, ⋯⟩, ⋯⟩

@[simp]

theorem TauCeti.choleskyReconstruction_coe {p : ℕ} (L : PosDiagLowerTriangular p) : ↑↑(choleskyReconstruction L) = ↑L * (↑L).transpose

The matrix underlying choleskyReconstruction L is L * Lᵀ.

@[simp]

theorem TauCeti.choleskyReconstruction_cholesky {p : ℕ} (A : PosDefMatrix p) : choleskyReconstruction (cholesky A) = A

Reconstructing a matrix from its Cholesky factor returns the original matrix.

theorem TauCeti.cholesky_injective {p : ℕ} : Function.Injective cholesky

The Cholesky construction is injective.