PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

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.

Regularized output error splits into source-specific terms

Statement

Assume Countable Choice, meaning every sequence of nonempty sets has a choice function. Let $X, Y$ be real or complex Hilbert spaces over the same scalar field, let $A : X \to Y$ be compact and linear (the closure of $A (B)$ is compact in $Y$ for every bounded set $B \subseteq X$ ), and let $A_{h} : X \to Y$ be bounded and linear with finite-dimensional range. Let $A^{*} : Y \to X$ and $A_{h}^{*} : Y \to X$ be their Hilbert adjoints, characterized by $⟨ A x, z ⟩_{Y} = ⟨ x, A^{*} z ⟩_{X}$ and $⟨ A_{h} x, z ⟩_{Y} = ⟨ x, A_{h}^{*} z ⟩_{X}$ , with both inner products linear in the first argument. Let $λ > 0$ , $x^{†} \in X$ , $e \in Y$ , $δ \geq 0$ with $∥ e ∥_{Y} \leq δ$ , and ${\tilde{x}}_{h} \in X$ . Put $y = A x^{†}, y_{δ} = y + e, y_{h, δ} = A_{h} x^{†} + e, d_{h} = (A - A_{h}) x^{†} = y_{δ} - y_{h, δ} .$ $R_{λ} = (A^{*} A + λ I_{X})^{- 1} A^{*}, R_{λ, h} = (A_{h}^{*} A_{h} + λ I_{X})^{- 1} A_{h}^{*},$ where $I_{X}$ is the identity operator on $X$ , and $r_{h, h} = (A_{h}^{*} A_{h} + λ I_{X}) {\tilde{x}}_{h} - A_{h}^{*} y_{h, δ} .$ Define $\begin{aligned} b_{b i a s} & = x^{†} - R_{λ} y, & b_{d a t a} & = R_{λ} y - R_{λ} y_{δ}, \\ b_{o p e r a t o r} & = (R_{λ} - R_{λ, h}) y_{h, δ}, & b_{p r e} & = R_{λ} d_{h}, \\ b_{s o l v e} & = R_{λ, h} y_{h, δ} - {\tilde{x}}_{h} . \end{aligned}$ Then the exact error identity and its triangle bound are $x^{†} - {\tilde{x}}_{h} = b_{b i a s} + b_{d a t a} + b_{p r e} + b_{o p e r a t o r} + b_{s o l v e},$ $∥ x^{†} - {\tilde{x}}_{h} ∥ \leq ∥ b_{b i a s} ∥ + ∥ b_{d a t a} ∥ + ∥ b_{p r e} ∥ + ∥ b_{o p e r a t o r} ∥ + ∥ b_{s o l v e} ∥,$ and the four displayed term estimates give $∥ x^{†} - {\tilde{x}}_{h} ∥ \leq ∥ b_{b i a s} ∥ + \frac{δ}{2 \sqrt{λ}} + \frac{∥ d_{h} ∥}{2 \sqrt{λ}} + ∥ b_{o p e r a t o r} ∥ + \frac{∥ r_{h, h} ∥}{λ} .$ If $∥ R_{λ} - R_{λ, h} ∥_{Y \to X} \leq η_{λ, h}$ , where the induced operator norm for a bounded linear map $T : Y \to X$ is $∥ T ∥_{Y \to X} : = \sup_{u \in Y, ∥ u ∥_{Y} \leq 1} ∥ T u ∥_{X},$ then $∥ b_{o p e r a t o r} ∥ \leq η_{λ, h} ∥ y_{h, δ} ∥_{Y}$ . If a residual evaluation separately supplies ${\hat{r}}_{h, h} \in X$ and $ρ_{h, h} \geq 0$ with $∥ {\hat{r}}_{h, h} - r_{h, h} ∥_{X} \leq ρ_{h, h}$ , then the final solve term is at most $(∥ {\hat{r}}_{h, h} ∥_{X} + ρ_{h, h}) / λ$ . These pointwise bounds assert no convergence rate as the data, regularization parameter, or discretization changes.

Statement references

Compact Hilbert-space inverse model

Hilbert adjoint and inner-product convention

Countable Choice hypothesis

Induced operator norm

Five-channel Tikhonov error budget

Exact telescoping chain and conditional error bounds

Finite-matrix residual certificate and returned-output bound

Additional sequence hypotheses for convergence

Clason, Regularization of Inverse Problems, Chapter 8

Hansen, Introduction to Inverse Problems, Chapter 5

Van Leeuwen and Brune, 10 Lectures on Inverse Problems and Imaging, Chapter 3

Facts & Assumptions

Given: Countable Choice, real or complex Hilbert spaces $X, Y$ , compact $A : X \to Y$ , bounded finite-dimensional-range $A_{h} : X \to Y$ , $λ > 0$ , $x^{†} \in X$ , $e \in Y$ with $∥ e ∥ \leq δ$ , $δ \geq 0$ , a returned ${\tilde{x}}_{h}$ , and its exact normal-equation residual $r_{h, h}$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): The Axiom of Countable Choice, written ${A C}_{ω}$ , asserts that every sequence of nonempty sets has a choice function.

[F1]

Error budget for computed Tikhonov inversion: The error-budget definition supplies $y = A x^{†}$ , $y_{δ} = y + e$ , $y_{h, δ} = A_{h} x^{†} + e$ , $d_{h} = (A - A_{h}) x^{†} = y_{δ} - y_{h, δ}$ , and the five bias, data, operator, pre-inversion, and solve vectors used below.

[F2]

Tikhonov error separates bias, data noise, discretization and solve residual: The supplier explicitly states that no rate for $d_{h}$ , no operator-perturbation estimate, and no floating-point residual bound is implicit.

[F3]

Hilbert-space Tikhonov amplifies data by at most $1 / (2 \sqrt{λ})$ : For a bounded $T$ between Hilbert spaces and $λ > 0$ , $∥ (T^{*} T + λ I)^{- 1} T^{*} g ∥ \leq ∥ g ∥ / (2 \sqrt{λ})$ .

[F4]

The shifted Hilbert-space normal operator is invertible with inverse norm at most $1 / λ$ : Under Countable Choice, the shifted normal operator $T^{*} T + λ I$ is bijective and its inverse has norm at most $1 / λ$ .

[F5]

The operator norm as the least bound and as the unit-sphere or unit-ball supremum: The operator norm is the supremum of $∥ T z ∥$ over $∥ z ∥ \leq 1$ ; rescaling gives $∥ T z ∥ \leq ∥ T ∥ ∥ z ∥$ .

[F6]

Computed augmented Tikhonov solves have certified residual and output-error bounds: For stored finite-matrix inputs and the successful augmented-QR solve with the supplier's stated operation, representation, nonsingularity, and residual-evaluation hypotheses, a certified residual $∥ \hat{r} - r ∥_{2} \leq ρ$ gives $∥ \hat{x} - x_{λ} ∥_{2} \leq (∥ \hat{r} ∥_{2} + ρ) / λ$ .

[F7]

The induced length is a norm: The norm induced by a real or complex inner product satisfies $∥ u + v ∥ \leq ∥ u ∥ + ∥ v ∥$ .

[F8]

Forward discretization enters before inversion and controls the Tikhonov parameter coupling: Its sequence convergence result additionally assumes $x^{†} ⊥ \ker A$ , exact data $y = A x^{†}$ , a common noise bound, an operator-norm approximation bound, $λ_{j} \to 0$ , and the stated limits for noise plus forward error over $\sqrt{λ_{j}}$ , the regularized-operator difference, and normal residual over $λ_{j}$ .

[F9]

The Hilbert-space adjoint of a bounded operator: Under Countable Choice, the Hilbert adjoint $A^{*}$ satisfies $⟨ A x, y ⟩_{Y} = ⟨ x, A^{*} y ⟩_{X}$ .

Proof

technique · direct

1.1givenA1F1F4F9algebra

Countable Choice [A1] and the adjoint definition [F9] give the Hilbert adjoints, while [F4] gives both shifted normal inverses; hence the displayed regularized operators are defined. The common perturbation cancels, so $y_{δ} - y_{h, δ} = (A x^{†} + e) - (A_{h} x^{†} + e) = d_{h}$ . Substituting the definitions in [F1] and adding in the order bias, data, pre-inversion, operator, solve gives the displayed telescoping sum: the adjacent $R_{λ} y$ , $R_{λ} y_{δ}$ , $R_{λ} y_{h, δ}$ , and $R_{λ, h} y_{h, δ}$ terms cancel, leaving $x^{†} - {\tilde{x}}_{h}$ .

1.2givenF1F5algebra

Under the stated operator-norm hypothesis, [F5] gives $∥ b_{o p e r a t o r} ∥ = ∥ (R_{λ} - R_{λ, h}) y_{h, δ} ∥ \leq η_{λ, h} ∥ y_{h, δ} ∥$ .

2.1step 1.1F7algebra

Taking norms in step 1.1 and applying the triangle inequality [F7] to the five summands gives the sum of the five channel norms.

3.1givenF1F3F4step 2.1algebra

By [F1], $b_{d a t a} = - R_{λ} e$ and $b_{p r e} = R_{λ} d_{h}$ . Applying [F3] to $e$ and $d_{h}$ gives $∥ b_{d a t a} ∥ \leq δ / (2 \sqrt{λ})$ and $∥ b_{p r e} ∥ \leq ∥ d_{h} ∥ / (2 \sqrt{λ})$ . With $H_{h} = A_{h}^{*} A_{h} + λ I_{X}$ , the normal equation gives $H_{h} R_{λ, h} y_{h, δ} = A_{h}^{*} y_{h, δ}$ , hence $H_{h} b_{s o l v e} = - r_{h, h}$ . By [F4], $∥ b_{s o l v e} ∥ \leq ∥ r_{h, h} ∥ / λ$ . Substitution in step 2.1 proves the displayed four-term estimate.

4.1givenF6F7step 3.1algebra

If a residual evaluation supplies the stated certificate, [F7] gives $∥ r_{h, h} ∥ \leq ∥ {\hat{r}}_{h, h} ∥ + ρ_{h, h}$ , which substituted in step 3.1 yields the residual-certificate variant. Under the finite-matrix hypotheses in [F6], the augmented-QR supplier is one concrete source of that certificate; its arithmetic and coordinate conditions remain assumptions.

5.1givenF2F8step 1.1step 2.1step 3.1step 4.1∎

Steps 1.1–4.1 prove a pointwise identity and bounds; the existing error-chain result [F2] likewise supplies no discretization rate or floating-point residual guarantee. The separate sufficient convergence result [F8] additionally assumes $x^{†} ⊥ \ker A$ , an operator-norm approximation bound, and the stated sequence coupling; none of those hypotheses is inferred here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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

Christian Clason, Regularization of Inverse Problems: Lecture Notes, arXiv:2001.00617v2, Chapter 8 (standard reference, not scraped)
Per Christian Hansen, Introduction to Inverse Problems, Chapter 5: Regularization Parameter Choice (standard reference, not scraped)
Tristan van Leeuwen and Christoph Brune, 10 Lectures on Inverse Problems and Imaging, Chapter 3 (standard reference, not scraped)