TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Real threshold sparse LU has a backward residual bound with actual growth

Statement

Let $A \in R^{n \times n}$ be nonsingular, $n \geq 1$ , and run Threshold partial-pivot sparse LU with explicit fill and failure statuses with $θ \in (0, 1]$ . Assume a successful run under the real operation model of Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add, with unit roundoff $u < 1$ and every exact intermediate either zero or normal. Let $M = \max_{i, j} ∣ a_{i j} ∣ > 0$ , let $S^{(k)}$ be the active matrix at stage $k$ including its current pivot row, and define the actual growth of this run by

ρ = \frac{\max_{k, i, j} ∣ S_{i j}^{(k)} ∣}{M} \geq 1.

For its computed factors and accumulated row permutation, there is a residual $Δ A$ such that $\hat{Q} P A P^{T} + Δ A = \hat{L} \hat{U}, \max_{i, j} ∣ Δ A_{i j} ∣ \leq \frac{8 n u}{θ} ρ M, ∥ Δ A ∥_{\infty} \leq \frac{8 n^{2} u}{θ} ρ M, ∥ X ∥_{\infty} : = \max_{i} \sum_{j} ∣ X_{i j} ∣ .$ The bound retains this run's actual growth $ρ$ and makes no uniform small-growth claim. This residual theorem is for real arithmetic; the local operation model used here does not specify a general complex division primitive.

Facts & Assumptions

Given: A successful real threshold-pivoted elimination run, the stated real relative operation model, and the no-range-failure hypothesis.

[F1]

Threshold partial-pivot sparse LU with explicit fill and failure statuses: At stage $k$ , use the diagonal only if its modulus is at least $θ$ times the active column maximum; otherwise swap a maximum-modulus row into the pivot position. The algorithm swaps previously stored entries of the same rows of $L$ and updates each active entry by one product and one subtraction.

[F2]

Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: Each real add, subtract, multiply, or divide is one rounded operation; on a successful in-range real operation, the computed result is the exact result times $1 + δ$ with $∣ δ ∣ \leq u$ , and exact zero is returned exactly.

Proof

1.1givenF1F2algebra

The initial active matrix is $P A P^{T}$ , whose entrywise maximum is $M$ because $P$ only permutes rows and columns; hence $ρ \geq 1$ . Let $c = S_{i k}^{(k)}$ and $p = S_{k k}^{(k)}$ at a successful pivot. If the diagonal is accepted, [F1] gives $∣ c / p ∣ \leq θ^{- 1}$ . If a maximum-modulus entry is selected, $∣ c / p ∣ \leq 1 \leq θ^{- 1}$ . The rounded division therefore gives $∣ {\hat{l}}_{i k} ∣ \leq (1 + u) / θ \leq 2 / θ$ . Also every pivot-row entry and every active entry has modulus at most $ρ M$ .

2.1step 1.1F1F2algebra

For a trailing update, write $p_{i j} = fl ({\hat{l}}_{i k} {\hat{u}}_{k j})$ and $S_{i j}^{(k + 1)} = fl (S_{i j}^{(k)} - p_{i j})$ . Define $e_{i j k} = S_{i j}^{(k + 1)} - (S_{i j}^{(k)} - {\hat{l}}_{i k} {\hat{u}}_{k j})$ . By [F2], $∣ p_{i j} - {\hat{l}}_{i k} {\hat{u}}_{k j} ∣ \leq u ∣ {\hat{l}}_{i k} {\hat{u}}_{k j} ∣, ∣ S_{i j}^{(k + 1)} - (S_{i j}^{(k)} - p_{i j}) ∣ \leq u ∣ S_{i j}^{(k)} - p_{i j} ∣ .$ The triangle inequality and $∣ p_{i j} ∣ \leq (1 + u) ∣ {\hat{l}}_{i k} {\hat{u}}_{k j} ∣$ yield $∣ e_{i j k} ∣ \leq u ∣ S_{i j}^{(k)} ∣ + u (2 + u) ∣ {\hat{l}}_{i k} {\hat{u}}_{k j} ∣ \leq u ρ M (1 + \frac{(2 + u) (1 + u)}{θ}) \leq \frac{7 u ρ M}{θ},$ using $u < 1$ and $θ \leq 1$ .

2.2step 1.1F2algebra

For a computed multiplier, ${\hat{l}}_{i k} = fl (c / p)$ , so [F2] gives a division residual $e_{i k}^{d i v} : = c - {\hat{l}}_{i k} p$ with $∣ e_{i k}^{d i v} ∣ \leq u ∣ c ∣ \leq u ρ M$ .

3.1F1step 2.1step 2.2inductionalgebra

Track each active row together with its previously stored entries of $\hat{L}$ and its accumulated update residuals. Before stage $k$ , for every active row $i$ and active column $j \geq k$ , maintain $(Q_{k} P A P^{T})_{i j} = \sum_{r < k} {\hat{l}}_{i r} {\hat{u}}_{r j} + S_{i j}^{(k)} - \sum_{r < k} e_{i j r},$ where $Q_{k}$ is the row permutation accumulated so far. At $k = 0$ this is $S^{(0)} = P A P^{T}$ . Swapping two active rows also swaps their earlier $L$ entries and residual histories, so it preserves the invariant. After the pivot, ${\hat{u}}_{k j} = S_{k j}^{(k)}$ ; each lower-row update is $S_{i j}^{(k + 1)} = S_{i j}^{(k)} - {\hat{l}}_{i k} {\hat{u}}_{k j} + e_{i j k}$ , so substitution gives the same invariant at stage $k + 1$ . For the pivot column, $S_{i k}^{(k)} = {\hat{l}}_{i k} {\hat{u}}_{k k} + e_{i k}^{d i v}$ by definition of the division residual. Thus after all stages, for $i \leq j$ , $(\hat{Q} P A P^{T})_{i j} - (\hat{L} \hat{U})_{i j} = - \sum_{k < i} e_{i j k},$ and for $i > j$ , $(\hat{Q} P A P^{T})_{i j} - (\hat{L} \hat{U})_{i j} = e_{i j}^{d i v} - \sum_{k < j} e_{i j k} .$ These identities define $Δ A = \hat{L} \hat{U} - \hat{Q} P A P^{T}$ . Each entry contains at most $n$ update residuals and at most one division residual.

4.1step 2.1step 2.2step 3.1algebra

By steps 2.1–2.2, every residual entry is bounded by $n \frac{7 u ρ M}{θ} + u ρ M \leq \frac{8 n u}{θ} ρ M,$ since $n \geq 1$ and $θ \leq 1$ . Summing at most $n$ such bounds in any row gives $∥ Δ A ∥_{\infty} \leq 8 n^{2} u ρ M / θ$ .

5.1step 3.1step 4.1∎

The definition of $Δ A$ in step 3.1 gives the displayed nearby-factorization identity, and step 4.1 gives both residual bounds. The only growth quantity in the estimate is the maximum active-entry magnitude of this executed run.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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

Jennifer Scott and Miroslav Tůma, Algorithms for Sparse Linear Systems, Chapter 7, §7.3.1 (standard reference, not scraped)
Timothy A. Davis, Siva Rajamanickam, and Wissam M. Sid-Lakhdar, A survey of direct methods for sparse linear systems, §6 (standard reference, not scraped)