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

Computed augmented Tikhonov solves have certified residual and output-error bounds

Statement

Let stored $A \in F^{m \times n}$ and $y \in F^{m}$ be real or complex, $m, n \geq 1$ , and let stored real $λ > 0$ . Let $x_{λ} = (A^{*} A + λ I)^{- 1} A^{*} y$ . Compute $α = fl (\sqrt{λ}) > 0$ under the successful normal-range square-root model, and solve the stored augmented problem $\min_{x} ∥ [A; α I] x - [y; 0] ∥_{2}$ by scaled Householder QR and rounded substitution. For complex inputs use the realification described below, so the backend uses only real triangular divisions. Every operation must succeed; failed pivots, invalid operations and out-of-range nonzero intermediates return range-failure.

For any returned $\hat{x}$ , let $\hat{r}$ and $ρ \geq 0$ certify $∥ \hat{r} - r ∥_{2} \leq ρ$ for the intended residual $r = (A^{*} A + λ I) \hat{x} - A^{*} y$ . One concrete certificate is supplied by Rounded matrix products give certified linear and normal-equation residual allowances using its successful sequential-dot evaluation, exact norms or certified upper bounds, and $0 < u < 1$ with $(\max (m, n) - 1) u < 1$ . These dimension restrictions concern evaluation on the original $m \times n$ matrix, including for complex data; if evaluating on the realified $2 m \times 2 n$ matrix instead, require $(\max (2 m, 2 n) - 1) u < 1$ . Arithmetic success alone does not imply these restrictions. Then $∥ \hat{x} - x_{λ} ∥_{2} \leq \frac{∥ \hat{r} ∥_{2} + ρ}{λ} .$ This bounds returned-output roundoff relative to the exact direct-solve target $x_{s t o p} = x_{λ}$ . It also certifies the solve term in any larger analytic error chain, irrespective of the backend. The representation of $\sqrt{λ}$ contributes no hidden change of target: $∣ α^{2} - λ ∣ \leq (2 u + u^{2}) λ$ . If residual evaluation instead uses exact $α^{2}$ , add $∣ α^{2} - λ ∣ ∥ \hat{x} ∥_{2}$ to its allowance; rounding a computed $α^{2}$ needs its own scalar error as well.

The backend's nearby least-squares conclusion holds under the completed QR/solve hypotheses and nonsingularity condition of Computed reduced QR least squares is backward stable for full column rank, including $M u < 1$ and $γ_{N + 3} < 1 / 8$ in the real backend dimensions $(M, N) = (m + n, n)$ or $(2 m + 2 n, 2 n)$ , respectively. In real dimension, write $C = [A; α I]$ and $ϵ_{Q} = β_{Q} ∥ C ∥_{F}$ . A sufficient check is $ϵ_{Q} < α$ and $∥ Δ R ∥_{F} < α - ϵ_{Q}$ . An explicit certified nonsingularity check may replace this sufficient margin.

For a Hilbert-space discrete operator, supply isometries $U : F^{n} \to X$ and $V : F^{m} \to Y$ with $A_{h} = V A U^{*}$ , and return $U \hat{x}$ . With coefficient datum $y_{c} = V^{*} y_{δ}$ , the exact normal solution lies in $ran U$ and the coefficient residual lifts isometrically, so the same certificate applies to $r_{h}$ ; likewise use $V^{*} y_{h, δ}$ for $r_{h, h}$ . If a stored coefficient datum ${\hat{y}}_{c}$ differs from $V^{*} y$ by at most $ϵ_{y}$ , add $∥ A ∥_{2} ϵ_{y}$ to the residual allowance. If the returned output also has an orthogonal component $z ⊥ ran U$ of norm at most $ϵ_{⊥}$ , add $λ ϵ_{⊥}$ . Finite rank alone does not supply these coordinate or output certificates.

Facts & Assumptions

Given: The stated stored finite inputs, successful augmented solve and residual evaluation, and certified upper bounds in the residual allowance. No convergence or automatic arithmetic success is assumed.

[F1]

Rounded matrix products give certified linear and normal-equation residual allowances supplies $∥ \hat{r} - r ∥ \leq ρ$ with all multiplication, dot-product and residual-addition errors under its successful evaluation and dimension/precision hypotheses stated above. Any independently certified pair satisfying this inequality also suffices.

[F2]

Computed reduced QR least squares is backward stable for full column rank supplies successful real augmented-QR nearby-data bounds with its explicit nonsingularity check.

[F3]

Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add supplies the successful rounded square-root and no-underflow model.

[F4]

For every $λ > 0$ , the Tikhonov objective is strictly convex and has the unique minimiser $(A^{*} A + λ I)^{- 1} A^{*} b$ supplies the exact real/complex minimizer and its normal equation.

[F5]

Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs: for real or complex inner-product vectors, $∣ ⟨ v, w ⟩ ∣ \leq ∥ v ∥ ∥ w ∥$ .

[F6]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: throughout this item the matrix $2$ -norm is the induced Euclidean operator norm, $∥ M ∥_{2} = \max_{∥ z ∥_{2} = 1} ∥ M z ∥_{2}$ for a nonzero domain, with value zero on the zero domain. Rescaling gives $∥ M z ∥_{2} \leq ∥ M ∥_{2} ∥ z ∥_{2}$ ; rowwise Cauchy–Schwarz gives the useful bound $∥ M ∥_{2} \leq ∥ M ∥_{F}$ .

Proof

1.1givenF2F5F6algebra

The stored augmented matrix has full column rank, since $∥ [A; α I] z ∥_{2}^{2} = ∥ A z ∥_{2}^{2} + α^{2} ∥ z ∥_{2}^{2} \geq α^{2} ∥ z ∥_{2}^{2}$ . If $C + Δ_{Q} = \hat{Q} \hat{R}$ , then $∥ \hat{R} z ∥ = ∥ (C + Δ_{Q}) z ∥ \geq (α - ϵ_{Q}) ∥ z ∥$ . Under the sufficient margin, the further triangular perturbation preserves a positive lower bound. Thus the nonsingularity premise in [F2] holds under the stated check. The theorem still explicitly requires successful arithmetic; exact full rank alone does not ensure rounded success.

1.2givenF1F3F4F5algebra

By [F3], $α = \sqrt{λ} (1 + δ)$ , $∣ δ ∣ \leq u$ , whence $∣ α^{2} - λ ∣ \leq (2 u + u^{2}) λ$ . For any $z$ , Cauchy-Schwarz gives $∥ (A^{*} A + λ I) z ∥ ∥ z ∥ \geq ⟨ (A^{*} A + λ I) z, z ⟩ = ∥ A z ∥^{2} + λ ∥ z ∥^{2} \geq λ ∥ z ∥^{2}$ . The normal equation [F4] therefore implies $∥ \hat{x} - x_{λ} ∥ \leq ∥ r ∥ / λ \leq (∥ \hat{r} ∥ + ρ) / λ$ using the assumed residual certificate, supplied by [F1] under the stated evaluation hypotheses. Replacing the coefficient in a residual by $α^{2}$ changes that exact residual by $(α^{2} - λ) \hat{x}$ , giving the stated additional allowance.

2.1F2F6step 1.1algebra

For complex inputs identify $z = z_{R} + i z_{I}$ with $(z_{R}, z_{I}) \in R^{2 n}$ . The real matrix $A_{R} = (\begin{array}{cc} Re A & - Im A \\ Im A & Re A \end{array})$ represents exactly the same linear map, preserves vector norms, and satisfies $∥ A_{R} ∥_{2} = ∥ A ∥_{2}$ , $∥ A_{R} ∥_{F} = \sqrt{2} ∥ A ∥_{F}$ by direct component sums. Apply [F2] to $[A_{R}; α I_{2 n}]$ and datum $((Re y, Im y), 0)$ ; this is exactly the original complex objective. Mapping its output back needs only component pairing, so introduces no arithmetic error or unmodeled complex division.

3.1F2F4step 1.1step 2.1step 1.2algebra

In exact arithmetic with the intended $\sqrt{λ}$ , full-rank augmented QR returns the unique minimizer in [F4], hence $x_{s t o p} = x_{λ}$ . Step 1.2 bounds the returned computed output's difference from that target, including square-root representation and all solve error through its certified residual. For an iterative stopping target different from $x_{λ}$ , retain separate stopping and output terms rather than calling their sum pure roundoff.

4.1F5F6step 1.2algebra∎

In the supplied Hilbert representation, $U^{*} U = I$ , $V^{*} V = I$ , and $A_{h}^{*} = U A^{*} V^{*}$ . The subspaces $ran U$ and its orthogonal complement are invariant under $A_{h}^{*} A_{h} + λ I$ ; on the complement that operator is $λ I$ and its right-hand side $A_{h}^{*} y$ has zero component. Thus the exact normal solution is $U x_{λ}$ , with coefficient datum $V^{*} y$ . Direct substitution gives $r_{h} = U ((A^{*} A + λ I) \hat{x} - A^{*} V^{*} y)$ , and isometry preserves its norm. For every coefficient vector $e$ , put $w = A^{*} e$ . Then $∥ w ∥_{2}^{2} = ⟨ A w, e ⟩ \leq ∣ ⟨ A w, e ⟩ ∣ \leq ∥ A ∥_{2} ∥ w ∥_{2} ∥ e ∥_{2}$ by [F5]–[F6]; dividing for $w \neq 0$ (and checking $w = 0$ directly) gives $∥ A^{*} e ∥_{2} \leq ∥ A ∥_{2} ∥ e ∥_{2}$ . Perturbing the datum therefore adds $U A^{*} ({\hat{y}}_{c} - V^{*} y)$ of norm at most $∥ A ∥_{2} ϵ_{y}$ ; an orthogonal output component adds $λ z$ . Triangle inequality gives the stated allowances. These explicit coordinate hypotheses preserve the general Hilbert theorem while justifying its concrete finite solve.

Depends on

Used by

Tikhonov error separates bias, data noise, discretization and solve residual Theorem

Dependency tree · two levels

20 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

Stuart and Voss, Matrix Analysis and Algorithms (standard reference, not scraped)