Monotonic optimal backward error along LSMR
Let $A \in \mathbb{R}^{m \times n}$ and $b \in \mathbb{R}^m$, and let $x_0 = 0, x_1, x_2, \dots$ be the LSMR iterates in exact arithmetic: $x_k$ minimises $\|A^T(b - Ax)\|_2$ over the Krylov subspace $\mathcal{K}_k(A^TA, A^Tb)$, taking the minimum-length minimiser where it is not unique, up to exact termination. For $x$ with residual $r = b - Ax$, the optimal backward error, which perturbs $A$ and keeps $b$ fixed, is $$\mu(x) = \min\{\|E\|_2 : (A + E)^T((A + E)x - b) = 0\},$$ and for $x \ne 0$ its approximation is $$\widetilde\mu(x) = \frac{\|K_x K_x^{\dagger} v_x\|_2}{\|x\|_2}, \qquad K_x = \begin{bmatrix} A \\ (\|r\|_2/\|x\|_2)\, I \end{bmatrix}, \quad v_x = \begin{bmatrix} r \\ 0 \end{bmatrix},$$ where $\dagger$ is the Moore–Penrose inverse; both are $0$ at an exact least-squares solution. Along LSMR both $\|A^Tr_k\|_2$ and $\|r_k\|_2$ decrease monotonically.
Problem. For all $A$ and $b$, are both sequences $\mu(x_k)$ and $\widetilde\mu(x_k)$ nonincreasing over successive nonzero iterates $x_k$?
Source: Fong (2011), Section 7.2.1, after the observation in Fong and Saunders (2011), Sec. 7; made precise by OpenProblemsInNLA (spectral norm, nonincreasing, nonzero iterates).
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Keywords
- backward errors, least-squares problems, LSMR, OpenProblemsInNLA
References
@phdthesis{fong2011,
author = {Fong, David Chin-Lung},
title = {Minimum-Residual Methods for Sparse Least-Squares Using {G}olub--{K}ahan Bidiagonalization},
school = {Stanford University},
year = {2011},
url = {https://purl.stanford.edu/sd504kj0427},
}
@article{fong2011lsmr,
author = {Fong, David Chin-Lung and Saunders, Michael},
title = {{LSMR}: An iterative algorithm for sparse least-squares problems},
journal = {SIAM J. Sci. Comput.},
volume = {33},
number = {5},
year = {2011},
pages = {2950--2971},
doi = {10.1137/10079687X},
eprint = {1006.0758},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ie17,
author = {Townsend, Alex},
title = {{IE-17}: Monotonic optimal backward error along LSMR},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/linear-systems-and-elimination/IE-17/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00081.
namespace RegistryProblems.OP_00081
noncomputable section
open Matrix
abbrev Mat (m n : ℕ) := Matrix (Fin m) (Fin n) ℝ
abbrev Vec (n : ℕ) := EuclideanSpace ℝ (Fin n)
/-- The induced Euclidean operator norm, with both spaces carrying their L2 norms. -/
def spectralNorm {m n : ℕ} (A : Mat m n) : ℝ :=
‖A.toEuclideanLin.toContinuousLinearMap‖
def residual {m n : ℕ} (A : Mat m n) (b : Vec m) (x : Vec n) : Vec m :=
b - A.toEuclideanLin x
def normalResidual {m n : ℕ} (A : Mat m n) (b : Vec m) (x : Vec n) : Vec n :=
A.transpose.toEuclideanLin (residual A b x)
/-- Only the matrix is perturbed; b is kept fixed. -/
def Feasible {m n : ℕ} (A : Mat m n) (b : Vec m) (x : Vec n) (E : Mat m n) : Prop :=
normalResidual (A + E) b x = 0
def errorSet {m n : ℕ} (A : Mat m n) (b : Vec m) (x : Vec n) : Set ℝ :=
{δ | ∃ E : Mat m n, Feasible A b x E ∧ spectralNorm E = δ}
/-- A minimum, including actual attainment, not merely an infimum. -/
def IsOptimalError {m n : ℕ} (A : Mat m n) (b : Vec m) (x : Vec n) (δ : ℝ) : Prop :=
IsLeast (errorSet A b x) δ
/-- K_k(AᵀA,Aᵀb), with K_0={0}. -/
def krylov {m n : ℕ} (A : Mat m n) (b : Vec m) (k : ℕ) : Submodule ℝ (Vec n) :=
Submodule.span ℝ {v | ∃ j : ℕ, j < k ∧
v = ((A.transpose * A) ^ j).toEuclideanLin (A.transpose.toEuclideanLin b)}
/-- Exact normal-residual minimization and the specified minimum-length convention. -/
def IsLSMRIterate {m n : ℕ} (A : Mat m n) (b : Vec m) (k : ℕ) (x : Vec n) : Prop :=
x ∈ krylov A b k ∧
(∀ y ∈ krylov A b k, ‖normalResidual A b x‖ ≤ ‖normalResidual A b y‖) ∧
(∀ y ∈ krylov A b k, ‖normalResidual A b y‖ = ‖normalResidual A b x‖ → ‖x‖ ≤ ‖y‖)
/-- A complete finite exact run from zero through its first least-squares solution. -/
def IsTerminatingLSMRRun {m n N : ℕ} (A : Mat m n) (b : Vec m)
(xs : Fin (N + 1) → Vec n) : Prop :=
xs 0 = 0 ∧ (∀ k, IsLSMRIterate A b k.val (xs k)) ∧
(∀ k, k.val < N → normalResidual A b (xs k) ≠ 0) ∧
normalResidual A b (xs (Fin.last N)) = 0
/-- Four real Moore–Penrose equations; no nonsingular-inverse substitute. -/
def IsMoorePenrose {ι κ : Type*} [Fintype ι] [Fintype κ]
[DecidableEq ι] [DecidableEq κ]
(K : Matrix ι κ ℝ) (P : Matrix κ ι ℝ) : Prop :=
K * P * K = K ∧ P * K * P = P ∧ (K * P).transpose = K * P ∧
(P * K).transpose = P * K
/-- The canonical stacked matrix [A; (‖r‖₂/‖x‖₂)I]. -/
def stacked {m n : ℕ} (A : Mat m n) (b : Vec m) (x : Vec n) :
Matrix (Fin m ⊕ Fin n) (Fin n) ℝ :=
fun i j => match i with
| Sum.inl i => A i j
| Sum.inr i => if i = j then ‖residual A b x‖ / ‖x‖ else 0
def stackedResidual {m n : ℕ} (A : Mat m n) (b : Vec m) (x : Vec n) :
EuclideanSpace ℝ (Fin m ⊕ Fin n) :=
WithLp.toLp 2 (fun i => match i with
| Sum.inl i => residual A b x i
| Sum.inr _ => 0)
/-- The canonical approximation on nonzero iterates, with its exact-LS zero convention.
The complete target also requires uniqueness, so no choice of generalized inverse changes q. -/
def IsApproximation {m n : ℕ} (A : Mat m n) (b : Vec m) (x : Vec n) (q : ℝ) : Prop :=
x ≠ 0 ∧ if normalResidual A b x = 0 then q = 0 else
∃ P : Matrix (Fin n) (Fin m ⊕ Fin n) ℝ,
IsMoorePenrose (stacked A b x) P ∧
q = ‖((stacked A b x) * P).toEuclideanLin (stackedResidual A b x)‖ / ‖x‖
/-- OP-00081: Monotonic optimal backward error along LSMR -/
def _root_.RegistryProblems.Problem_OP_00081 : Prop :=
(∀ (m n N : ℕ) (A : Mat m n) (b : Vec m) (xs : Fin (N + 1) → Vec n),
IsTerminatingLSMRRun A b xs →
∀ (i j : Fin (N + 1)), j.val = i.val + 1 → xs i ≠ 0 → xs j ≠ 0 →
∀ (μ ν : ℝ), IsOptimalError A b (xs i) μ → IsOptimalError A b (xs j) ν → ν ≤ μ) ∧
(∀ (m n N : ℕ) (A : Mat m n) (b : Vec m) (xs : Fin (N + 1) → Vec n),
IsTerminatingLSMRRun A b xs →
∀ (i j : Fin (N + 1)), j.val = i.val + 1 → xs i ≠ 0 → xs j ≠ 0 →
∀ (μ ν : ℝ), IsApproximation A b (xs i) μ → IsApproximation A b (xs j) ν → ν ≤ μ)
end
end RegistryProblems.OP_00081
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00081 theorem resolution : RegistryProblems.Problem_OP_00081 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00081" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00081 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Complete exact counterexample to both canonical monotonicity claims: attained matrix-only spectral minimum and the literal Moore–Penrose approximation along actual exact LSMR iterates.
An integer $4\times3$ least-squares problem has exact LSMR iterates with increasing optimal matrix-only spectral-norm backward error. A spectral completion gives an upper certificate $1979/2000$ for the squared first error, and a positive-definite rational matrix gives a strict lower certificate $99/100$ for the squared second error. The approximation $\widetilde\mu$ of the backward error increases as well. These certificates use exact rational …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IE-17/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00081, "Monotonic optimal backward error along LSMR", clopen.solutions.