TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique

Statement

Let $n \geq 1$ and let $A \in M_{n} (C)$ , with the real case obtained by restricting scalars to $R$ . Then the following are equivalent:

$A$ has a Cholesky factorisation $A = L L^{*}$ with $L$ lower triangular and positive real diagonal.
$A$ is Hermitian positive definite.

When these conditions hold, the factor $L$ is unique.

Facts & Assumptions

Given: A matrix $A \in M_{n} (C)$ .

[L1]

Hermitian positive-definite matrices and Cholesky factorisations with positive diagonal are defined in Hermitian positive-definite matrices and Cholesky factorisation A = LL* with positive diagonal.

[L2]

The determinant of a triangular matrix is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).

[L3]

Determinants are multiplicative (For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ ).

[L4]

Matrix multiplication uses the convention of Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes.

Proof

technique · block induction with a quotient comparison for uniqueness

1.1

Suppose $A = L L^{*}$ as in [L1]. Then $A^{*} = L L^{*} = A$ , so $A$ is Hermitian. For any nonzero $x$ , one has $x^{*} A x = x^{*} L L^{*} x = (L^{*} x)^{*} (L^{*} x) = ∥ L^{*} x ∥_{2}^{2} .$ The diagonal of $L$ is positive, hence nonzero; [L2] and [L3] give $\det L \neq 0$ , so $L$ is invertible and $L^{*} x \neq 0$ when $x \neq 0$ . Therefore $x^{*} A x > 0$ .

L1L2L3L4algebra

1.2

For the converse, use induction on $n$ . The case $n = 1$ is immediate: $A = [a]$ is Hermitian positive definite exactly when $a > 0$ , in which case $A = [\sqrt{a}] [\sqrt{a}]^{*}$ .

baseL1algebra

1.3

Assume $n > 1$ and the converse for size $n - 1$ . Write $A = (\begin{array}{cc} a & r^{*} \\ r & C \end{array}) .$ Positive definiteness of $A$ at $x = e_{0}$ gives $a > 0$ . Set $ℓ : = r / \sqrt{a}$ and $S : = C - ℓ ℓ^{*}$ . For nonzero $y \in C^{n - 1}$ , apply positive definiteness to $x = (\binom{- a^{- 1} r^{*} y}{y})$ : $0 < x^{*} A x = y^{*} S y .$ Thus $S$ is Hermitian positive definite. By the induction hypothesis, $S = \tilde{L} {\tilde{L}}^{*}$ with $\tilde{L}$ lower triangular and positive diagonal.

ihL1algebra

2.1

Define $L : = (\begin{array}{cc} \sqrt{a} & 0 \\ ℓ & \tilde{L} \end{array}) .$ Direct multiplication gives $L L^{*} = (\begin{array}{cc} a & r^{*} \\ r & ℓ ℓ^{*} + \tilde{L} {\tilde{L}}^{*} \end{array}) = (\begin{array}{cc} a & r^{*} \\ r & C \end{array}) = A .$ The matrix $L$ is lower triangular and its diagonal is positive real, so this is a Cholesky factorisation.

step 1.3L1L4algebra

3.1

For uniqueness, suppose $A = L_{1} L_{1}^{*} = L_{2} L_{2}^{*}$ are two such factorizations. Then $M : = L_{2}^{- 1} L_{1}$ is lower triangular, and $M M^{*} = I$ because $L_{2} M M^{*} L_{2}^{*} = L_{1} L_{1}^{*} = L_{2} L_{2}^{*}$ . A lower-triangular unitary matrix has zero strict-lower entries and diagonal entries of modulus $1$ ; since the diagonal of $M$ is the ratio of two positive real diagonals, each diagonal entry is also positive real, hence equals $1$ . Therefore $M = I$ and $L_{1} = L_{2}$ .

step 1.1step 2.1L2L3algebra

4.1

Step 1.1 proves that a Cholesky factorisation implies Hermitian positive definiteness. Steps 1.2-2.1 prove the converse by induction, and step 3.1 gives uniqueness.

step 1.1step 1.2step 2.1step 3.1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Theorem 2.9.3 (standard reference, not scraped)
David Bindel, CS 4220: Numerical Analysis, Blocked LU and Cholesky (standard reference, not scraped)