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.
Computed reduced QR least squares is backward stable for full column rank
Statement
Let , , have full column rank. Successful scaled Householder QR gives the exactly orthonormal reduced representative and computed triangular with where is the proved local-step coefficient. Apply the stored reflectors to by rounded rank-one updates and let be the first coordinates. Set . Alternatively, if an explicitly supplied exactly orthonormal has entries admissible as arithmetic inputs and uses sequential rounded dots, set . Solve by successful rounded back substitution. Suppose and . There exist and upper triangular with If is nonsingular, is the unique least-squares solution for and . The relative matrix perturbation is at most ; the right-hand perturbation is at most . For fixed , both perturbation coefficients are . If additionally and , both relative data perturbation bounds are at most . These two coefficient comparisons are additional checks; they do not follow from and alone. Success and nonsingularity are explicit hypotheses.
Facts & Assumptions
Given: The stated successful QR, right-hand-side evaluation, and triangular solve; all nonzero exact intermediates are normal.
The scaled Householder QR implementation is backward stable supplies the proved QR bound and the stored-reflector application bound.
Rounded triangular substitution has a componentwise matrix backward error supplies the rounded triangular matrix perturbation, including the zero-solution branch.
Reduced QR over the reals solves full-column-rank least squares without squaring the condition number identifies exact full-rank reduced-QR least squares.
If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n bounds the coefficient errors of sequential real dots.
Cauchy–Schwarz: , with equality exactly for dependent pairs: for real Euclidean vectors, .
Proof
For stored-reflector evaluation, [F1] bounds by . In the explicit admissible-input alternative, dot expansion by [F4] gives coordinate errors at most by Cauchy-Schwarz and unit column norms; combining coordinates gives . In either case put and . Exact orthonormality gives and .
Apply [F2] to the actual rounded back substitution. It supplies upper triangular with and the displayed Frobenius estimate. This holds also when , since the same row identities force . Combined with step 1.1 this proves the perturbed normal-coordinate equation.
Under the stated nonsingularity hypothesis, has full column rank, and [F3] identifies as its unique least-squares minimizer for . Finally , and gives the stated relative matrix bound. At fixed dimensions, [F1] gives , and gives in either right-hand-side branch, so the displayed coefficients are . Under the additional coefficient checks, write ; then , while the assumed gives the right-hand bound. No comparison between and is inferred from arithmetic success alone.
Depends on
- The scaled Householder QR implementation is backward stable
- Rounded triangular substitution has a componentwise matrix backward error
- Reduced QR over the reals solves full-column-rank least squares without squaring the condition number
- If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n
- Cauchy–Schwarz: $|\langle x,y\rangle|\le\|x\|\,\|y\|$, with equality exactly for dependent pairs
Used by
- Finite-budget primal-dual Newton methods for LP, convex QP, and symmetric cones Algorithm
- Finite-precision reduced-QR KKT solve with certified residual status Algorithm
- Gauss-Newton linearized least-squares step with QR/SVD rank safeguards Algorithm
- Revised-simplex basis QR recomputation with finite residual and pivot statuses Algorithm
- A full rank least squares problem where rounded normal equations lose the pivot Example
- An ill conditioned design with large forward sensitivity Example
- Computed augmented Tikhonov solves have certified residual and output-error bounds Lemma
- Finite QR basis recomputation has sound residual and stored-data audit statuses Theorem
- The computed KKT residual certificate bounds the exact linear-system residual Theorem
Dependency tree · two levels
27 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, Householder triangularization (standard reference, not scraped)
- Fundamentals of Numerical Computation, QR factorization and least squares (standard reference, not scraped)
- Stuart and Voss, Matrix Analysis and Algorithms, Warwick lecture notes (standard reference, not scraped)