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.
Numerical Inverse Problems and Regularization Error — Examples
1 · Prerequisites
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compact Operators and Riesz Schauder Theory
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Direct Matrix Factorisations: LU, Cholesky and QR
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces Adjoint Operators and Annihilators
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite-precision direct factorizations and least squares
- Foundations of the Real Numbers for Analysis
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Limits of Real Functions
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Matrix Norms, Condition Numbers and Numerical Stability
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Numerical Inverse Problems and Regularization Error
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- 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
- Splitting Fields
- Subspaces, Products, and Quotients
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Analytic Hahn Banach Theorem
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Galois Correspondence
- The Moore--Penrose Pseudoinverse and Regularised Least Squares
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
These examples calculate noise amplification in an ill-conditioned diagonal problem, compare Tikhonov bias and data response at two parameters, retain a quadrature residual before inversion, and apply the exact normal-equation residual bound. The residual example uses an exact residual and does not by itself certify its floating-point evaluation.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A small singular value makes the Tikhonov noise bound sharp
Example
Assume Countable Choice. Take on , exact target , noise , observed data , and . The regularized inverse sends this noise to a vector of norm , exactly the general bound .
Facts & Assumptions
Given: Countable Choice, the diagonal matrix, target, noise and parameter above; verify the regularized noise amplification and the claimed sharp bound.
Hilbert-space Tikhonov amplifies data by at most : For every data vector , the Tikhonov map satisfies .
Verification
Here and , so and .
Since , [F1] gives the upper bound , equal to the computed output norm. Thus the constant is attained in this example.
Increasing the Tikhonov parameter trades smaller data response for more bias
Example
Assume Countable Choice. In the scalar problem , , and , the data are . At , the regularization bias is and the data-noise contribution has magnitude . At , the corresponding magnitudes are and . This pair of parameter choices shows the tradeoff; it does not assert a universally optimal parameter rule.
Facts & Assumptions
Given: Countable Choice, , , , , and the two positive parameter values; verify the regularization bias and data-noise terms.
Tikhonov error separates bias, data noise, discretization and solve residual: For finite matrices, with .
Verification
In this scalar case , so the bias magnitude is and the noise magnitude is by [F1].
At these values are and ; at they are and . The two components move in opposite directions for these choices, with no parameter-choice guarantee asserted.
A scalar quadrature residual appears before the regularized inverse
Example
Assume Countable Choice. Model a quadrature or collocation approximation by the scalar maps and , exact target , shared data noise , and . Then the exact forward datum is , the perturbed datum is , the discretized perturbed datum is , and the forward residual discarded before inversion is . The refined error chain keeps its propagated residual as a separate term.
Facts & Assumptions
Given: Countable Choice, the scalar exact and discretized operators, target, shared noise, and above; verify the pre-inversion residual and full error chain.
Tikhonov error separates bias, data noise, discretization and solve residual: For and , the exact chain contains the separate term before the discretized solve.
Verification
The scalar regularized maps are and . Also , so [F1] gives the propagated pre-inversion residual .
With the exact discrete solve , the five chain terms are respectively , , , , and . Their sum is , verifying the telescoping identity with the forward residual counted once.
An exact normal-equation residual gives an a posteriori solution bound
Example
Assume Countable Choice. Let on , , and . The exact regularized solution is . For the approximate value , the exact normal-equation residual is , so the bound holds. This uses an exact residual; it does not certify how floating-point residual evaluation error should be bounded.
Facts & Assumptions
Given: Countable Choice, , , , and ; compute the exact residual and compare it with the error bound.
The shifted Hilbert-space normal operator is invertible with inverse norm at most : The inverse of exists and has norm at most .
Verification
Here , while the exact regularized solution is . Thus .
The exact residual is . Since , [F1] bounds the error by . The residual here is exact, not a floating-point evaluation certificate.