TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck pass

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 successful rounded Cholesky factorization has componentwise and normwise backward error bounds

Statement

Let $n \geq 1$ and let $A = A^{*}$ be positive definite in $C^{n \times n}$ . Suppose the rounded Cholesky algorithm succeeds with $\hat{L}$ . Put $m = 20 n + 20$ and $g = γ_{m} = \frac{m u}{1 - m u}$ ; assume $m u < 1 / 5$ . For $E = \hat{L} {\hat{L}}^{*} - A$ , which is Hermitian, and with $∣ M ∣$ denoting entrywise absolute value for matrices, $∣ E ∣ \leq 100 g ∣ \hat{L} ∣ ∣ \hat{L} ∣^{*} entrywise, ∥ E ∥_{F} \leq 100 g ∥ \hat{L} ∥_{F}^{2}, ∥ E ∥_{2} \leq 100 g ∥ \hat{L} ∥_{F}^{2} .$ Thus $c_{n} (u) u = \frac{100 m u}{1 - m u}$ . If also $100 \sqrt{n} g \leq 1 / 2$ , then $∥ E ∥_{F} \leq 200 \sqrt{n} g ∥ A ∥_{F}, ∥ E ∥_{2} \leq 200 \sqrt{n} g ∥ A ∥_{F} .$ These bounds apply on success only; positive definiteness does not guarantee rounded success.

Facts & Assumptions

Given: successful rounded recurrences, the normal-range model, and the exact Cholesky convention.

[F1]

Failure-aware rounded Cholesky factorization: success supplies positive rounded pivots and rounded updates using six-real-operation complex products.

[F2]

A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique: Hermitian positive-definite input has an exact lower triangular factor with positive diagonal.

[F3]

If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n: a chain of k successful operations has the gamma_k relative bound when ku<1.

[F4]

Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison: $∥ M ∥_{2} \leq ∥ M ∥_{F}$ .

[F5]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: finite-dimensional Euclidean vectors satisfy the Cauchy-Schwarz inequality.

Proof

1.1givenF1F3algebra

For one complex product $z w$ , write its real exact products as $a c, b d, a d, b c$ . Each rounded product has error at most $u$ times its operand product; each final rounded real sum or difference contributes at most $u$ times the sum of the two operand magnitudes. Hence the real-component error is at most $(2 u + u^{2}) (∣ a c ∣ + ∣ b d ∣)$ and the imaginary-component error at most $(2 u + u^{2}) (∣ a d ∣ + ∣ b c ∣)$ . Since $u < 1 / 200$ , their Euclidean combination is at most $6 u ∣ z ∣ ∣ w ∣$ . A sequential sum of at most $n$ complex products contributes at most $γ_{n} (1 + 6 u)$ times the absolute product sum; adding product errors gives $6 u + γ_{n} (1 + 6 u) = \frac{(n + 6) u}{1 - n u} \leq γ_{n + 6} \leq g$ . Each diagonal term $∣ {\hat{l}}_{j k} ∣^{2}$ uses two rounded squares and one rounded addition; sequentially summing at most $n$ terms uses at most $4 n$ rounded real operations, so the same expansion bounds the diagonal sum error by $γ_{4 n} S_{j} \leq g S_{j}$ .

2.1step 1.1F1algebra

For $i > j$ , let $S_{i j} = \sum_{k < j} {\hat{l}}_{i k} \overline{{\hat{l}}_{j k}}$ , $T_{i j} = \sum_{k \leq j} ∣ {\hat{l}}_{i k} ∣ ∣ {\hat{l}}_{j k} ∣$ , and ${\hat{S}}_{i j}$ be the computed dot product. Step 1.1 gives $∣ {\hat{S}}_{i j} - S_{i j} ∣ \leq g T_{i j}$ and $∣ {\hat{S}}_{i j} ∣ \leq (1 + g) T_{i j}$ . The subtraction error is at most $u (∣ a_{i j} ∣ + ∣ {\hat{S}}_{i j} ∣)$ , and the two component divisions imply $∣ {\hat{l}}_{i j} {\hat{l}}_{j j} - {\hat{r}}_{i j} ∣ \leq u ∣ {\hat{r}}_{i j} ∣$ ; also $∣ {\hat{r}}_{i j} ∣ \leq (1 + u) (∣ a_{i j} ∣ + ∣ {\hat{S}}_{i j} ∣)$ . Therefore $∣ E_{i j} ∣ \leq g T_{i j} + u (2 + u) (∣ a_{i j} ∣ + (1 + g) T_{i j})$ . Since $∣ a_{i j} ∣ \leq T_{i j} + ∣ E_{i j} ∣$ , moving $u (2 + u) ∣ E_{i j} ∣$ to the left gives $∣ E_{i j} ∣ \leq \frac{g + u (2 + u) (2 + g)}{1 - u (2 + u)} T_{i j}$ . Here $u \leq g / m$ , $g < 1 / 4$ , $m \geq 40$ , and $u < 1 / 200$ , so the numerator coefficient is less than $1.12 g$ and the denominator exceeds $0.989$ . The quotient is less than $1.14 g < 100 g$ .

2.2step 1.1F1F3algebra

On the diagonal put $S_{j} = \sum_{k < j} ∣ {\hat{l}}_{j k} ∣^{2}$ . Step 1.1 and the pivot subtraction give $p_{j} = a_{j j} - S_{j} + ϵ_{j}$ with $∣ ϵ_{j} ∣ \leq u ∣ a_{j j} ∣ + (g + u (1 + g)) S_{j} \leq u ∣ a_{j j} ∣ + 1.26 g S_{j}$ . The rounded square root has ${\hat{l}}_{j j} = \sqrt{p_{j}} (1 + δ_{j})$ , $∣ δ_{j} ∣ \leq u$ , so $∣ {\hat{l}}_{j j}^{2} - p_{j} ∣ \leq (2 u + u^{2}) p_{j} \leq 3 u p_{j}$ . From $∣ a_{j j} ∣ \leq S_{j} + p_{j} + ∣ ϵ_{j} ∣$ we get $(1 - u) ∣ a_{j j} ∣ \leq (1 + 1.26 g) S_{j} + p_{j}$ . Since $u < 1 / 200$ and $g < 1 / 4$ , this implies $∣ a_{j j} ∣ \leq 1.33 S_{j} + 1.01 p_{j} \leq \frac{21}{10} (S_{j} + p_{j})$ . Also $p_{j} = {\hat{l}}_{j j}^{2} / (1 + δ_{j})^{2} \leq 1.011 {\hat{l}}_{j j}^{2}$ , so $\frac{21}{10} (S_{j} + p_{j}) \leq \frac{11}{5} (S_{j} + {\hat{l}}_{j j}^{2})$ . Thus $∣ E_{j j} ∣ \leq u ∣ a_{j j} ∣ + 1.26 g S_{j} + 3 u p_{j} \leq 1.32 g S_{j} + 0.14 g {\hat{l}}_{j j}^{2} \leq 100 g (S_{j} + {\hat{l}}_{j j}^{2})$ , using $u \leq g / 40$ . Hermitian symmetry gives the corresponding conjugate entries, proving the componentwise estimate.

3.1step 2.1step 2.2F2F4F5algebra∎

By [F5], Cauchy-Schwarz applied to each row-column inner product gives $∥ ∣ \hat{L} ∣ ∣ \hat{L} ∣^{*} ∥_{F}^{2} \leq \sum_{i, j} (\sum_{k} ∣ {\hat{l}}_{i k} ∣^{2}) (\sum_{k} ∣ {\hat{l}}_{j k} ∣^{2}) = ∥ \hat{L} ∥_{F}^{4}$ . The entrywise bound therefore yields $∥ E ∥_{F} \leq 100 g ∥ \hat{L} ∥_{F}^{2}$ , and [F4] gives the spectral bound. For the relative consequence, take traces in $\hat{L} {\hat{L}}^{*} = A + E$ : $∥ \hat{L} ∥_{F}^{2} \leq \sqrt{n} ∥ A ∥_{F} + \sqrt{n} ∥ E ∥_{F} \leq \sqrt{n} ∥ A ∥_{F} + 100 \sqrt{n} g ∥ \hat{L} ∥_{F}^{2}$ . The additional condition gives $∥ \hat{L} ∥_{F}^{2} \leq 2 \sqrt{n} ∥ A ∥_{F}$ , yielding both stated relative norm bounds.

Depends on

Used by

Dependency tree · two levels

34 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

Fundamentals of Numerical Computation, floating-point arithmetic (standard reference, not scraped)
Fundamentals of Numerical Computation, Cholesky factorization (standard reference, not scraped)
Stuart and Voss, Matrix Analysis and Algorithms, Warwick lecture notes (standard reference, not scraped)