TheoremStatement: AI-adaptedProof: AI-generatedPipeline-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.

In the standard real floating-point model, computed pivoted LU is a nearby factorisation with a pivot-growth dependent backward bound

Statement

Let $A \in M_{n} (R)$ with $n \geq 1$ , and suppose Gaussian elimination with partial pivoting is carried out in the standard relative floating-point model with unit roundoff $u$ , with every intermediate division, product, and sum in range. Let the computed factors satisfy

$\hat{P} A \approx \hat{L} \hat{U},$ where $\hat{P}$ is a permutation matrix, $\hat{L}$ is unit lower triangular, and $\hat{U}$ is upper triangular. Then there exists a matrix $Δ A$ such that $\hat{P} (A + Δ A) = \hat{L} \hat{U},$ and $∣ Δ A ∣ \leq γ_{n} {\hat{P}}^{T} (∣ \hat{L} ∣ ∣ \hat{U} ∣)$ entrywise, where $γ_{n} = n u / (1 - n u)$ . If $ρ (A)$ is the pivot-growth factor of Permutation matrices, partial pivoting, and the pivot-growth factor, then $∥ Δ A ∥_{\infty} \leq n^{2} γ_{n} ρ (A) \max_{p, q} ∣ a_{p q} ∣ .$

Facts & Assumptions

Given: A matrix $A \in M_{n} (R)$ , the standard relative floating-point model with unit roundoff $u$ and $n u < 1$ , and computed partial-pivoted factors $\hat{P}, \hat{L}, \hat{U}$ with all intermediate operations in range.

[L1]

Partial pivoting produces a permutation matrix and multipliers $∣ {\hat{ℓ}}_{i k} ∣ \leq 1$ below the diagonal (Every real or complex square matrix admits a PLU factorisation, and the first failed pivot marks the singular boundary, Permutation matrices, partial pivoting, and the pivot-growth factor).

[L2]

The floating-point model represents each in-range arithmetic operation by a relative perturbation bounded by $u$ (The standard relative floating-point model and unit roundoff).

[L3]

Products of factors $(1 + δ)$ with $∣ δ ∣ \leq u$ collapse to $1 + θ$ with $∣ θ ∣ \leq γ_{n}$ (If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n).

[L4]

A floating-point dot product of length at most $n$ equals the exact dot product of componentwise perturbed summands with relative perturbations bounded by $γ_{n}$ (The computed floating-point dot product obeys componentwise and normwise error bounds).

Proof

technique · collect the local elimination residuals into one backward perturbation

1.1

In exact arithmetic, each computed upper-triangular entry satisfies a formula of the form ${\hat{u}}_{i j} = fl ((\hat{P} A)_{i j} - \sum_{k < i} {\hat{ℓ}}_{i k} {\hat{u}}_{k j}),$ and each computed strict-lower entry satisfies ${\hat{ℓ}}_{i j} = fl (\frac{(\hat{P} A)_{i j} - \sum_{k < j} {\hat{ℓ}}_{i k} {\hat{u}}_{k j}}{{\hat{u}}_{j j}}) .$ By [L2]-[L4], each such floating-point combination is the exact relation for a perturbed entry of $\hat{P} A$ , with perturbation bounded by $γ_{n}$ times the corresponding dot-product sum. Collecting those entrywise perturbations into a matrix $E$ gives $\hat{P} A + E = \hat{L} \hat{U}$ and $∣ E_{i j} ∣ \leq γ_{n} \sum_{k \leq \min (i, j)} ∣ {\hat{ℓ}}_{i k} ∣ ∣ {\hat{u}}_{k j} ∣ .$

L2L3L4algebra

2.1

Set $Δ A : = {\hat{P}}^{T} E$ . Because $\hat{P}$ is a permutation matrix, $∣ Δ A ∣ = {\hat{P}}^{T} ∣ E ∣ \leq γ_{n} {\hat{P}}^{T} (∣ \hat{L} ∣ ∣ \hat{U} ∣)$ by step 1.1. Multiplying the identity of step 1.1 by ${\hat{P}}^{T}$ on the left gives $\hat{P} (A + Δ A) = \hat{L} \hat{U},$ which is the nearby-factorisation statement.

step 1.1L1algebra

2.2

By [L1], every row of $∣ \hat{L} ∣$ has one diagonal $1$ and at most $n - 1$ strict-lower entries of modulus at most $1$ , so its row sum is at most $n$ . Every entry of $\hat{U}$ is bounded by $ρ (A) \max_{p, q} ∣ a_{p q} ∣$ from the definition of pivot growth. Therefore each row sum of $∣ \hat{L} ∣ ∣ \hat{U} ∣$ is at most $n^{2} ρ (A) \max_{p, q} ∣ a_{p q} ∣$ , and step 1.1 yields $∥ E ∥_{\infty} \leq n^{2} γ_{n} ρ (A) \max_{p, q} ∣ a_{p q} ∣ .$ Because row permutations preserve the infinity norm, the same bound holds for $Δ A$ .

step 1.1L1algebra

3.1

Step 2.1 proves the backward-error identity, and step 2.2 gives the pivot-growth dependent bound.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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, Section 2.6.4 (standard reference, not scraped)
David Bindel, CS 4220: Numerical Analysis, Beyond linear solves + using structure (standard reference, not scraped)