LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pendingjudge 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.

Product condition gives the LM range-approximation bound

Statement

Let $X, Y$ be real Hilbert spaces, let $U \subseteq X$ be open, and let $F : U \to Y$ be Fréchet differentiable at every point of $U$ with $x \mapsto F^{'} (x)$ continuous in operator norm. Let $V \subseteq U$ and let $c > 0$ be such that, for every $u, \tilde{u} \in V$ , $∥ F (u) - F (\tilde{u}) - F^{'} (u) (u - \tilde{u}) ∥_{Y} \leq c ∥ u - \tilde{u} ∥_{X} ∥ F (u) - F (\tilde{u}) ∥_{Y} .$ Suppose $x^{†}, x \in V$ , $F (x^{†}) = y$ , $∥ y^{δ} - y ∥_{Y} \leq δ$ with $δ \geq 0$ , $τ > 0$ , and $∥ x - x^{†} ∥_{X} \leq e$ . If $R : = ∥ F (x) - y^{δ} ∥_{Y} > τ δ$ , then

$∥ F^{'} (x) (x^{†} - x) + F (x) - y^{δ} ∥_{Y} \leq \frac{1 + c e (1 + τ)}{τ} R .$

In particular, if $σ \in (0, 1)$ , $e \leq e_{0}$ , and $γ : = \frac{σ τ}{1 + c e_{0} (1 + τ)} > 1,$ then $∥ F^{'} (x) (x^{†} - x) + F (x) - y^{δ} ∥_{Y} \leq \frac{σ}{γ} R .$

Statement references

Product-type tangential cone condition

Nonlinear forward map and exact-data convention

Real Hilbert spaces and their induced norms

Fréchet differentiability and operator-norm derivative

Christian Clason, Regularization of Inverse Problems, Assumption 11.10 and proof of Theorem 11.11

Facts & Assumptions

Given: The spaces, map, set, constant, exact solution, datum, noise bound, $τ$ , and points in the Statement.

[F1]

For $x, \tilde{x} \in V$ , the product condition gives $∥ F (x) - F (\tilde{x}) - F^{'} (x) (x - \tilde{x}) ∥_{Y} \leq c ∥ x - \tilde{x} ∥_{X} ∥ F (x) - F (\tilde{x}) ∥_{Y}$ (Product-type tangential cone condition).

[F2]

The exact-data convention is $F (x^{†}) = y$ (Nonlinear forward maps between Hilbert spaces); the noise bound $∥ y^{δ} - y ∥_{Y} \leq δ$ is an additional hypothesis in the Statement.

[F3]

The induced real Hilbert norm satisfies the triangle inequality (The induced length is a norm).

Proof

1.1givenF1constructalgebra

Set $E : = F (x) - F (x^{†}) - F^{'} (x) (x - x^{†})$ . By [F1] with $\tilde{x} = x^{†}$ and the point-distance bound, $∥ E ∥_{Y} \leq c e ∥ F (x) - y ∥_{Y}$ .

2.1givenF2F3step 1.1algebra

The target residual equals $E + (y - y^{δ})$ . Also [F3] gives $∥ F (x) - y ∥_{Y} \leq R + δ$ . Therefore [F3] and [F2] yield $∥ F^{'} (x) (x^{†} - x) + F (x) - y^{δ} ∥_{Y} \leq c e (R + δ) + δ .$

3.1givenstep 2.1algebra

Since $R > τ δ$ and $τ > 0$ , $δ < R / τ$ . Substituting into step 2.1 and collecting the coefficient of $R$ gives $c e (R + δ) + δ \leq (c e (1 + \frac{1}{τ}) + \frac{1}{τ}) R = \frac{1 + c e (1 + τ)}{τ} R,$ which is the first conclusion.

4.1givenstep 3.1algebra∎

If $e \leq e_{0}$ , then $1 + c e (1 + τ) \leq 1 + c e_{0} (1 + τ) = σ τ / γ$ . Applying this inequality to step 3.1 proves the stated $σ / γ$ range-approximation bound.

Remarks

No choice principle is used: the proof applies the product condition to the two fixed points in the hypotheses and then uses norm inequalities.

Depends on

Used by

Dependency tree · two levels

25 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, Assumption 11.10 and proof of Theorem 11.11 (standard reference, not scraped)