Pipeline-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.

Nonlinear Landweber with discrepancy stopping — Examples and Counterexamples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

The initial residual can already meet the discrepancy threshold

Example

Take $X = Y = R$ with the usual real Hilbert structure, $U = R$ , $F (x) = x$ , $x_{0} = x^{†} = 0$ , $y = F (x^{†}) = 0$ , noise level $δ = 1$ , noisy datum $y^{δ} = 1$ , discrepancy parameter $τ > 2$ , and update budget $M = 0$ . The local Landweber assumptions hold with any radius $r > 0$ and $η = 0$ , and the initial residual is $1 \leq τ δ$ . The algorithm therefore returns stopped at index zero with iterate $0$ and residual $1$ , before consulting the zero update budget.

Example references

Landweber update, stopping test, and budget order

Facts & Assumptions

Given: The scalar real Hilbert space $X = Y = R$ , $U = R$ , $F (x) = x$ , $x_{0} = x^{†} = 0$ , $y = 0$ , $δ = 1$ , $y^{δ} = 1$ , $τ > 2$ , and $M = 0$ .

[F1]

Nonlinear Landweber iteration with discrepancy stopping: the algorithm tests $∥ y^{δ} - F (x_{k}^{δ}) ∥_{Y} \leq τ δ$ before testing whether $k = M$ .

[F2]

Local tangential cone condition: the local TCC remainder is $F (x + h) - F (x) - F^{'} (x) h$ and its required bound is relative to $∥ F (x + h) - F (x) ∥$ .

Verification

1.1givenF2algebra

The map is continuously Fréchet differentiable with $F^{'} (x) h = h$ , so $∥ F^{'} (x) ∥ = 1$ . Its TCC remainder vanishes for every pair, hence the uniform TCC holds with $η = 0$ ; ${\overline{B}}_{2 r} (0) \subset R$ and $x^{†} = 0 \in {\overline{B}}_{r} (0)$ for any $r > 0$ . Also $∣ y^{δ} - y ∣ = 1 = δ$ .

2.1givenF1algebra∎

At the initial point, $∥ y^{δ} - F (x_{0}) ∥ = ∣ 1 - 0 ∣ = 1 \leq τ δ$ . By [F1] the procedure returns stopped at $k = 0$ with iterate $x_{0} = 0$ and residual $1$ before the $M = 0$ budget condition is checked.

CounterexampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Exact-data Landweber can stall without a local tangential-cone condition

Statement refuted

Exact solvability by itself is enough for exact-data nonlinear Landweber to converge from every initial point; no local tangential-cone or initial-ball hypothesis is needed.

Statement references

The local hypotheses and exact-data conclusion

Facts & Assumptions

Given: The real Hilbert line $X = Y = R$ , $U = R$ , $F (x) = x^{2} - 1$ , exact solution $x^{†} = 1$ , exact datum $y = 0$ , and initial point $x_{0} = 0$ .

[F1]

Nonlinear Landweber iteration with discrepancy stopping specifies the exact-data update $x_{n + 1} = x_{n} + F^{'} (x_{n})^{*} (y - F (x_{n}))$ . Here we study that formula as a bare recurrence, not as a run of the defined procedure: step 2.1 shows this instance violates its admissible local TCC hypothesis. A zero derivative gives a zero update.

[F2]

Local tangential cone condition: at a base point $x$ the local TCC requires $∣ F (x + h) - F (x) - F^{'} (x) h ∣ \leq η ∣ F (x + h) - F (x) ∣$ for every increment in its radius.

[F3]

Nonlinear Landweber Fejér decrease and discrepancy stopping: its exact-data convergence conclusion assumes the specified outer ball, derivative bound, and uniform TCC on that ball.

Counterexample

1.1givenF1algebrainduction

For every $x, h \in R$ , $F (x + h) - F (x) - 2 x h = h^{2}$ , so $F$ is Fréchet differentiable with $F^{'} (x) h = 2 x h$ . Thus $F (1) = 0 = y$ is an exact solution and $F^{'} (x_{0}) = F^{'} (0) = 0$ . The Landweber update in [F1] gives $x_{1} = 0$ ; induction gives $x_{n} = 0$ and residual $∣ y - F (x_{n}) ∣ = 1$ for every $n$ . The exact-data iterates therefore do not converge to a solution.

2.1givenF2F3choosealgebra∎

For any proposed local radius $δ > 0$ , choose $h = δ / 2 > 0$ . At $x_{0} = 0$ , $F (h) - F (0) = h^{2}$ and $F^{'} (0) h = 0$ , so [F2] would require $h^{2} \leq η h^{2}$ . Since $h^{2} > 0$ , this forces $η \geq 1$ . Thus no local TCC ball at this initial point has a constant $η < 1 / 2$ , violating the theorem's retained local hypothesis [F3].

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Exact data can converge without a finite discrepancy stop

Example

Take $X = Y = R$ , $U = R$ , $F (x) = x / 2$ , initial point $x_{0} = 1$ , exact solution $x^{†} = 0$ , exact datum $y = 0$ , and exact data $y^{δ} = y$ with $δ = 0$ . The derivative norm is $1 / 2$ and the uniform TCC holds with $η = 0$ on every ball. For any $τ > 2$ and any finite update budget $M$ , the ideal exact-data iterates are $x_{n} = (3 / 4)^{n}$ and have strictly positive residual at every finite index. They converge to the exact solution, but the zero discrepancy threshold is never met finitely, so the finite-budget algorithm returns budget_exhausted.

Example references

Exact-data discrepancy test and budget status

Exact-data convergence and the absence of a finite-stop guarantee

Facts & Assumptions

Given: $X = Y = R$ , $U = R$ , $F (x) = x / 2$ , $x_{0} = 1$ , $x^{†} = 0$ , $y = y^{δ} = 0$ , $δ = 0$ , $τ > 2$ , and an arbitrary finite $M \in N_{0}$ .

[F1]

Nonlinear Landweber iteration with discrepancy stopping: the procedure returns stopped only when the current residual is at most $τ δ$ ; after $M$ updates it returns budget_exhausted if that test has not succeeded.

[F2]

Nonlinear Landweber Fejér decrease and discrepancy stopping: for exact data under the stated local hypotheses, the ideal Landweber sequence converges to a solution; the theorem does not claim a finite exact-data stop.

Verification

1.1givenalgebra

The derivative is $F^{'} (x) h = h / 2$ , so $∥ F^{'} (x) ∥ = 1 / 2 \leq 1$ , and the linearization remainder is identically zero. Thus the uniform TCC holds with $η = 0$ . With $r = 1$ , $x^{†} = 0 \in {\overline{B}}_{r} (1)$ and ${\overline{B}}_{2 r} (1) \subset R$ , so the local hypotheses hold.

2.1givenF1F2algebrainduction∎

The update is $x_{n + 1} = x_{n} + (1 / 2) (- x_{n} / 2) = (3 / 4) x_{n}$ ; induction gives $x_{n} = (3 / 4)^{n} > 0$ and residual $∣ F (x_{n}) - y ∣ = (1 / 2) (3 / 4)^{n} > 0$ for every finite $n$ . Hence the discrepancy test with threshold $τ δ = 0$ never succeeds at a finite index. By [F2], the exact-data sequence converges to a solution; the only solution of $F (x) = 0$ is $0$ . Therefore any finite-budget run reaches $M$ with positive residual and returns budget_exhausted by [F1].