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
1 · Prerequisites
- Banach-Space Differential Calculus and Banach Manifolds
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces Adjoint Operators and Annihilators
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Inverse maps, identifiability, and stability
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Nonlinear maps and tangential cone control
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- The Analytic Hahn Banach Theorem
- The ZFC Axioms and the Basic Set Constructions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Logical flowchart
3 · Definitions, theorems and proofs
Nonlinear Landweber iteration with discrepancy stopping
Definition
Let be real Hilbert spaces, let be open, and let be Fréchet differentiable at every point with a derivative map that is continuous in operator norm. This is the real-Hilbert forward-map convention. Assume Countable Choice, so every bounded derivative has the Hilbert adjoint characterized by .
An admissible local instance consists of an initial point , a radius , an exact solution with exact datum , a noise level , noisy datum with , a constant , a discrepancy parameter , and a finite update budget . The closed outer ball is contained in ; for every ; and the uniform two-point tangential-cone inequality
holds for every . This is the uniform family of the one-basepoint local tangential-cone inequality; the shared constant and pair domain are part of the admissibility hypothesis. The exact solution and the bounds are analysis data and need not be available to the computational loop.
Inputs: , , , , , and from an admissible local instance.
Output: Either stopped with an index , iterate , and residual , or budget_exhausted with the last iterate and its residual.
Procedure: Set . For , compute . If , return stopped with . If , return budget_exhausted with . Otherwise set
and continue at the next index. Each update is evaluated at a current point in , where the derivative and its Hilbert adjoint are defined.
Definition references
Real-Hilbert forward-map and exact-data interface
Fréchet derivatives are bounded linear operators, with the derivative map defined pointwise
Completeness and real-Hilbert-space convention
Inner-product convention, linear in the first argument
One-basepoint local tangential-cone inequality
Operator norm of each derivative
Hilbert adjoints under Countable Choice
Adjoint identity and norm equality
Christian Clason, Regularization of Inverse Problems, Chapter 11
Nonlinear Landweber Fejér decrease and discrepancy stopping
Statement
Let be real Hilbert spaces, let be open, and let be Fréchet differentiable at every point with continuous in operator norm. Fix and such that , and suppose an exact solution satisfies . Assume for every and that, for some ,
for every . This is a uniform two-point hypothesis with the derivative based at the first point. Assume Countable Choice so that the bounded derivatives have Hilbert adjoints. For and with , set and define the ideal Landweber sequence by
Let . For , let denote the first with , if it exists. Put and . Then the following hold.
-
For every update before the first discrepancy stop, writing , the squared-error estimate is
In particular, the iterates are Fejér monotone relative to up to the stop: their distance to does not increase. Here Fejér monotonicity means exactly this nonincrease of distance to the stated solution.
-
If , the first discrepancy index exists and
A run of the finite-budget algorithm with budget returns
stoppedat this first index; if , it returnsbudget_exhaustedat . -
For exact data ( and ), the ideal sequence is defined for every , satisfies
and converges strongly to some with . No finite stopping index is claimed in the exact-data case.
-
For noisy data (), the ideal stopped iterates converge uniformly over the admissible noise ball to that same exact-data limit:
For finite-budget runs this conclusion concerns outputs only when their budgets reach the first discrepancy indices. The theorem asserts neither a convergence rate nor that is an -minimum-norm solution.
Statement references
Facts & Assumptions
Given: All hypotheses in the Statement. For any current iterate in the outer ball, write and . The update is .
The Axiom of Countable Choice (): the Axiom of Countable Choice, , is assumed. No stronger form of choice is assumed.
The data satisfy and .
The closed outer ball lies in , is within distance of , is continuous in operator norm on , and the derivative bound and uniform two-point tangential-cone inequality in the Statement hold on that ball.
Nonlinear Landweber iteration with discrepancy stopping: the iteration is and the discrepancy check is made before the finite-budget check.
Local tangential cone condition: at a base point , the local TCC bounds by . The theorem assumes this exact orientation uniformly for pairs in the outer ball.
The Hilbert-space adjoint of a bounded operator and Hilbert-adjoint identities: and for every bounded Hilbert-space operator .
Real and complex inner-product spaces and their induced length: the real inner product is symmetric and ; the corresponding expansion is .
The induced length is a norm: in each real Hilbert space.
Hilbert space: every Cauchy sequence in for the induced norm converges in .
Series, partial sums, convergence and the sum, divergence, and the tail series and A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum: a series with nonnegative real terms and bounded partial sums converges, and its tails tend to zero.
The reals are complete and Every complete ordered field is Archimedean: the real field is complete and its natural numbers are unbounded above.
The well-ordering principle: every nonempty set of natural indices has a least member.
The operator norm as the least bound and as the unit-sphere or unit-ball supremum: for every bounded linear , .
Nonlinear forward maps between Hilbert spaces: a real-Hilbert forward map is on an open domain, and exact solutions satisfy .
Fréchet derivative between Banach spaces: each Fréchet derivative is a bounded real-linear operator, and differentiability on defines the derivative map .
Proof
Fix a current point and any exact solution in the outer ball, and set , , and . The uniform TCC gives . Since , , so by the noise bound and the triangle inequality, .
The update has . Expanding its squared norm and using the adjoint identity yields . Since [F13] makes a bounded operator, [F11] gives .
Write . By [F5] and step 1.2, . Substituting step 1.1 gives the stated one-step estimate .
If and , then by the strict lower bound on , so the squared error decreases. For exact data , the same bound is for every residual, including zero.
Put , which is positive by the strict hypothesis on . For each , the residual is greater than ; step 2.1 then gives .
For exact data, step 2.1 gives for every . Summing the first inequalities telescopes and yields .
The initial point satisfies . At every update before the noisy stop, or at every exact-data update, step 3.1 keeps ; consequently . Induction therefore keeps every iterate needed by the recurrence in the declared outer ball and proves Fejér decrease relative to .
Suppose and the discrepancy test never succeeds. Summing step 3.2 over the first updates telescopes, while every residual exceeds , so for every natural . The Archimedean property in [F9] supplies a natural , contradicting this bound. Hence the first stopping index is finite.
The partial sums of the nonnegative residual-square series are bounded by step 3.3. By [F8] the series converges, its tails tend to zero, and its terms tend to zero; thus and the claimed infinite-series bound holds.
Let , , and . The sequence is nonincreasing by step 3.1. Hence , and the partial sums satisfy . Applying [F8] again shows that the tail sums tend to zero.
If , the bound is immediate because and . If , telescoping through that positive first index gives , hence the same bound. If , then and the initial residual is at most , so and the same bound holds for the stated positive . By [F1], a budget reaching returns the first stop, while a shorter budget returns budget_exhausted.
Fix and choose minimizing the finite set of residuals ; [F10] supplies a least index among minimizers. For , put , , and . The uniform TCC gives and . Since , Cauchy–Schwarz gives .
For any fixed finite number of executed updates, the noisy iterates converge to the exact iterates as along data sequences whose discrepancy stop occurs no earlier. Indeed, the update map is continuous: is continuous by Fréchet differentiability, is continuous by hypothesis, and [F3] together with [F11] gives operator-norm continuity of the adjoint action. Induction from the common initial point proves the fixed-index assertion.
The exact update gives . Summing this identity and using [F3] shows , and likewise .
Real inner-product expansion gives , since . It also gives , because .
By the triangle inequality, , which tends to zero uniformly in by steps 4.3 and 4.4. Thus is Cauchy. Completeness of gives . By Fréchet differentiability at , , so boundedness of implies ; step 4.3 gives . step 4.1 and the triangle inequality give , so passage to the limit gives .
Suppose the uniform noisy-data conclusion fails. Then some and, for every integer , a positive and admissible datum can be selected so that the stopped iterate is at least from ; [A1] supplies this countable selection from the nonempty bad-data sets. Let . Passing to a subsequence, either is a fixed integer or : a bounded sequence of natural indices has a value occurring infinitely often, and an unbounded one has an increasing subsequence chosen recursively by least indices.
In the fixed-index case, write . Step 5.3 gives . Fréchet differentiability at and boundedness of imply . The discrepancy test and noise bound give , so . The exact update at is then zero, so for every and therefore . Step 5.3 now gives , contradicting the selected distance lower bound.
In the case , choose with by step 8.1. For all sufficiently large , and step 5.3 gives . Each noisy iterate before its stop stays in the outer ball by step 4.1, and lies there by step 8.1; applying the one-step estimate of step 2.1 with the exact solution makes the noisy iterates Fejér monotone relative to up to . Hence , again contradicting the selected lower bound.
Both subsequence cases contradict the failure assumption in step 9.1. Therefore the supremum over all data satisfying tends to zero as .
Remarks
The lower bound on is sufficient, not necessary. The local TCC constant can be difficult to verify and is often not known numerically; when it is unknown, a chosen cannot be certified by this theorem merely because it is a common practical value. The nonlinear residual sequence need not be monotone, which is why the exact-data Cauchy proof selects a minimum residual on each finite block. The result is local to the declared ball and gives neither a rate nor a minimum-norm selection.
4 · Examples, counterexamples and false statements
None yet.
Sources
- Christian Clason, Regularization of Inverse Problems, Chapter 11
- S. Hubmer, E. Sherina, S. Kindermann, and K. Raik, A numerical comparison of some heuristic stopping rules for nonlinear Landweber iteration, §2.1
- Christian Clason, Regularization of Inverse Problems, Chapter 11, Assumption 11.2, Lemma 11.3, and Theorems 11.4–11.6