Is the ideal GMRES bound sharp for every Jordan block?
For $n \ge 2$ and $\lambda \in \mathbb{C} \setminus \{0\}$ let $J_n(\lambda) = \lambda I + N$ be the $n \times n$ Jordan block, where $N$ has ones on the superdiagonal and zeros elsewhere. Let $\mathcal{P}_k$ be the set of complex polynomials $p$ of degree at most $k$ with $p(0) = 1$, and for $J \in \mathbb{C}^{n \times n}$ let $$\psi_k(J) = \max_{v \in \mathbb{C}^n,\ \|v\|_2 = 1} \min_{p \in \mathcal{P}_k} \|p(J)v\|_2, \qquad \varphi_k(J) = \min_{p \in \mathcal{P}_k} \|p(J)\|_2$$ be the worst-case and the ideal GMRES approximations at step $k$: $\psi_k$ is the slowest possible GMRES residual reduction, and $\varphi_k$ the ideal bound. Always $\psi_k(J) \le \varphi_k(J)$, with equality when $J$ is normal. Tichý, Liesen and Faber proved $\psi_k(J_n(\lambda)) = \varphi_k(J_n(\lambda))$ whenever $k$ divides $n$, and in further cases depending on $k$, $n$ and $|\lambda|$.
Problem. Is $\psi_k(J_n(\lambda)) = \varphi_k(J_n(\lambda))$ for every $n \ge 2$, every $\lambda \in \mathbb{C} \setminus \{0\}$ and every $1 \le k < n$?
Source: Tichý, Liesen and Faber (2007), Section 1.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- CA
- Keywords
- GMRES, Jordan blocks, Krylov subspace methods, OpenProblemsInNLA
References
@article{tichy2007,
author = {Tich{\'y}, Petr and Liesen, J{\"o}rg and Faber, Vance},
title = {On worst-case {GMRES}, ideal {GMRES}, and the polynomial numerical hull of a {J}ordan block},
journal = {Electron. Trans. Numer. Anal.},
volume = {26},
year = {2007},
pages = {453--473},
url = {https://etna.ricam.oeaw.ac.at/vol.26.2007/pp453-473.dir/pp453-473.pdf},
}
@misc{openproblemsinnla-ie02,
author = {Townsend, Alex},
title = {{IE-02}: Is the ideal GMRES bound sharp for every Jordan block?},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/linear-systems-and-elimination/IE-02/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00077.
namespace RegistryProblems.OP_00077
noncomputable section
open scoped BigOperators Matrix
open Polynomial
abbrev Poly := Polynomial ℂ
abbrev Square (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
abbrev H (n : ℕ) := EuclideanSpace ℂ (Fin n)
def DegreeLE (p : Poly) (m : ℕ) : Prop := p.degree ≤ (m : WithBot ℕ)
def euclideanLin {n : ℕ} (A : Square n) : H n →ₗ[ℂ] H n := Matrix.toEuclideanLin A
def euclideanCLM {n : ℕ} (A : Square n) : H n →L[ℂ] H n :=
(euclideanLin A).toContinuousLinearMap
def operatorNorm {n : ℕ} (A : Square n) : ℝ := ‖euclideanCLM A‖
def unitSphere (n : ℕ) : Set (H n) := {x | ‖x‖ = 1}
def upperShift (n : ℕ) : Square n :=
fun i j => if j.val = i.val + 1 then 1 else 0
def jordan (n : ℕ) (lam : ℂ) : Square n := lam • 1 + upperShift n
def polyEval {n : ℕ} (p : Poly) (A : Square n) : Square n := Polynomial.aeval A p
def Admissible (k : ℕ) (p : Poly) : Prop := DegreeLE p k ∧ p.eval 0 = 1
def gmresInner {n : ℕ} (A : Square n) (k : ℕ) (x : H n) : ℝ :=
sInf {t : ℝ | ∃ p : Poly, Admissible k p ∧ t = ‖euclideanLin (polyEval p A) x‖}
def idealGMRES {n : ℕ} (A : Square n) (k : ℕ) : ℝ :=
sInf {t : ℝ | ∃ p : Poly, Admissible k p ∧ t = operatorNorm (polyEval p A)}
def worstGMRES {n : ℕ} (A : Square n) (k : ℕ) : ℝ :=
sSup (gmresInner A k '' unitSphere n)
/-- OP-00077: Is the ideal GMRES bound sharp for every Jordan block? -/
def _root_.RegistryProblems.Problem_OP_00077 : Prop :=
∀ (n k : ℕ) (lam : ℂ), 2 ≤ n → lam ≠ 0 → 1 ≤ k → k < n →
worstGMRES (jordan n lam) k = idealGMRES (jordan n lam) k ∧
(∀ x ∈ unitSphere n, ∃ p : Poly, Admissible k p ∧
‖euclideanLin (polyEval p (jordan n lam)) x‖ = gmresInner (jordan n lam) k x ∧
∀ q : Poly, Admissible k q → ‖euclideanLin (polyEval p (jordan n lam)) x‖ ≤
‖euclideanLin (polyEval q (jordan n lam)) x‖) ∧
∃ (p : Poly) (x : H n), Admissible k p ∧ x ∈ unitSphere n ∧
operatorNorm (polyEval p (jordan n lam)) = idealGMRES (jordan n lam) k ∧
‖euclideanLin (polyEval p (jordan n lam)) x‖ = operatorNorm (polyEval p (jordan n lam)) ∧
gmresInner (jordan n lam) k x = worstGMRES (jordan n lam) k ∧
(∀ q : Poly, Admissible k q →
operatorNorm (polyEval p (jordan n lam)) ≤ operatorNorm (polyEval q (jordan n lam))) ∧
(∀ q : Poly, Admissible k q → ‖euclideanLin (polyEval p (jordan n lam)) x‖ ≤
‖euclideanLin (polyEval q (jordan n lam)) x‖) ∧
(∀ z ∈ unitSphere n, gmresInner (jordan n lam) k z ≤ gmresInner (jordan n lam) k x)
end
end RegistryProblems.OP_00077
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_00077 theorem resolution : RegistryProblems.Problem_OP_00077 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00077" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00077 := 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
For every complex Jordan block in the original IE-02 range, ideal GMRES equals worst-case GMRES. All polynomial minima, sphere suprema and their attaining witnesses use the actual Euclidean matrix and vector norms.
For every $n\ge2$, every $\lambda\in\mathbb C\setminus\{0\}$ and every $1\le k<n$, the Jordan block $J_n(\lambda)=\lambda I+N$ satisfies $\max_{\|v\|_2=1}\min_{p\in\mathcal P_k}\|p(J_n(\lambda))v\|_2=\min_{p\in\mathcal P_k}\|p(J_n(\lambda))\|_2$, where $\mathcal P_k$ is the set of complex polynomials of degree at most $k$ with $p(0)=1$: worst-case and ideal GMRES coincide. The argument proves a stronger minimax equality for finite affine families of lower triangular Toeplitz matrices. Finite Carathéodory–Fejér interpolation describes …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-06 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IE-02/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00077, "Is the ideal GMRES bound sharp for every Jordan block?", clopen.solutions.