Strict interlacing across block Lanczos iterations
Let $A \in \mathbb{R}^{n \times n}$ be symmetric and $V \in \mathbb{R}^{n \times p}$ of full column rank, let $\mathcal K_j = \operatorname{range}[V, AV, \dots, A^{j-1}V]$ be the block Krylov subspaces, and let $s$ be the largest $j$ with $\dim \mathcal K_j = jp$. For $1 \le j \le s$ let $T_j = Q_j^{\mathsf T} A Q_j$, where $Q_j$ is an orthonormal basis of $\mathcal K_j$, and let $\theta^{(j)}_1 \le \dots \le \theta^{(j)}_{jp}$ be its eigenvalues, the Ritz values, counted with multiplicity. They do not depend on the choice of $Q_j$; the block Lanczos method, in exact arithmetic, produces a block tridiagonal $T_j$. For $p = 1$, between two consecutive Ritz values of one Lanczos iteration lies a Ritz value of every later iteration, and Šimonová and Tichý derive the case $j = k + 1$ of the statement below from eigenvalue interlacing.
Problem. For every such $A$ and $V$, all $1 \le k < j \le s$ and all $1 \le i \le (k-1)p$, must the open interval $(\theta^{(k)}_i, \theta^{(k)}_{i+p})$ contain an eigenvalue of $T_j$?
Source: Šimonová and Tichý (2025), the unnumbered conjecture in §2.1 of arXiv:2507.16484v1.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- SP
- Keywords
- block Lanczos methods, eigenvalue interlacing, OpenProblemsInNLA, Ritz values
References
@article{simonova2025,
author = {{\v{S}}imonov{\'a}, Dorota and Tich{\'y}, Petr},
title = {On finite precision block {L}anczos computations},
journal = {BIT Numer. Math.},
volume = {65},
number = {4},
year = {2025},
pages = {Paper No. 47},
doi = {10.1007/s10543-025-01089-2},
eprint = {2507.16484},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ke04,
author = {Townsend, Alex},
title = {{KE-04}: Strict interlacing across block Lanczos iterations},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/eigenvalues-and-inverse-problems/KE-04/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00089.
namespace RegistryProblems.OP_00089
noncomputable section
open scoped BigOperators
abbrev Vec (n : ℕ) := EuclideanSpace ℝ (Fin n)
abbrev Rect (n m : ℕ) := Matrix (Fin n) (Fin m) ℝ
abbrev Mat (n : ℕ) := Rect n n
def column {n m : ℕ} (M : Rect n m) (j : Fin m) : Vec n :=
WithLp.toLp 2 (fun i => M i j)
def columnSpace {n m : ℕ} (M : Rect n m) : Submodule ℝ (Vec n) :=
Submodule.span ℝ (Set.range (column M))
def FullColumnRank {n p : ℕ} (V : Rect n p) : Prop :=
LinearIndependent ℝ (column V)
/-- Degree is the first index; the second index selects a starting-block column. -/
def krylovColumns {n p : ℕ} (A : Mat n) (V : Rect n p) (ell : ℕ) :
Fin ell × Fin p → Vec n :=
fun rc => column (A ^ rc.1.val * V) rc.2
/-- Exactly the span of the columns of [V, A V, ..., A^(ell-1) V]. -/
def krylov {n p : ℕ} (A : Mat n) (V : Rect n p) (ell : ℕ) :
Submodule ℝ (Vec n) :=
Submodule.span ℝ (Set.range (krylovColumns A V ell))
/-- Actual dimension, with no eigenvalue or polynomial condition attached. -/
def FullBlockDimension {n p : ℕ} (A : Mat n) (V : Rect n p) (ell : ℕ) : Prop :=
Module.finrank ℝ (krylov A V ell) = ell * p
/-- The canonical maximality convention. For p=0 there is no largest such index. -/
def LastFullBlockIteration {n p : ℕ} (A : Mat n) (V : Rect n p) (s : ℕ) : Prop :=
FullBlockDimension A V s ∧ ∀ t, FullBlockDimension A V t → t ≤ s
/-- Arbitrary orthonormal columns spanning the exact Krylov space.
No compatibility or block-tridiagonal premise is imposed between iterations. -/
def IsKrylovBasis {n p : ℕ} (A : Mat n) (V : Rect n p) (ell : ℕ)
(Q : Rect n (ell * p)) : Prop :=
Q.transpose * Q = 1 ∧ columnSpace Q = krylov A V ell
/-- Over the real field this is exactly Q.transpose * A * Q. -/
def compression {n m : ℕ} (A : Mat n) (Q : Rect n m) : Mat m :=
Q.conjTranspose * A * Q
/-- Mathlib sorts self-adjoint eigenvalues in decreasing order; `Fin.rev`
reverses that order. The genuine spectral theorem retains all multiplicities. -/
def orderedEigenvalues {m : ℕ} (M : Mat m) (hM : M.IsHermitian) : Fin m → ℝ :=
fun r => (Matrix.isSymmetric_toEuclideanLin_iff.mpr hM).eigenvalues
finrank_euclideanSpace_fin r.rev
/-- Total zero-based indexing. The target's index bounds guarantee the first
branch; a separate index contract makes that fact explicit. -/
def eigenvalueAt {m : ℕ} (M : Mat m) (hM : M.IsHermitian) (i : ℕ) : ℝ :=
if h : i < m then orderedEigenvalues M hM ⟨i, h⟩ else 0
/-- Only real symmetry is required to obtain the genuine compression spectrum.
The imported elementary Hermitian-congruence lemma supplies its symmetry. -/
def ritzValues {n m : ℕ} (A : Mat n) (hA : A.IsHermitian) (Q : Rect n m) :
Fin m → ℝ :=
orderedEigenvalues (compression A Q) (Matrix.isHermitian_conjTranspose_mul_mul Q hA)
def ritzValueAt {n m : ℕ} (A : Mat n) (hA : A.IsHermitian)
(Q : Rect n m) (i : ℕ) : ℝ :=
eigenvalueAt (compression A Q) (Matrix.isHermitian_conjTranspose_mul_mul Q hA) i
/-- The complete occupancy assertion through s, for all permitted k,j,i and
independently chosen orthonormal bases. The natural i is one-based as in the source. -/
def IterationOccupancy {n p : ℕ} (A : Mat n) (hA : A.IsHermitian)
(V : Rect n p) (s : ℕ) : Prop :=
∀ k j : ℕ, 1 ≤ k → k < j → j ≤ s →
∀ (Qk : Rect n (k * p)) (Qj : Rect n (j * p)),
IsKrylovBasis A V k Qk → IsKrylovBasis A V j Qj →
∀ i : ℕ, 1 ≤ i → i ≤ (k - 1) * p →
∃ r : Fin (j * p),
ritzValueAt A hA Qk (i - 1) < ritzValues A hA Qj r ∧
ritzValues A hA Qj r < ritzValueAt A hA Qk (i + p - 1)
/-- OP-00089: Strict interlacing across block Lanczos iterations -/
def _root_.RegistryProblems.Problem_OP_00089 : Prop :=
∀ (n p : ℕ) (A : Mat n) (hA : A.IsHermitian) (V : Rect n p),
FullColumnRank V → ∀ s, LastFullBlockIteration A V s → IterationOccupancy A hA V s
end
end RegistryProblems.OP_00089
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_00089 theorem resolution : RegistryProblems.Problem_OP_00089 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00089" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00089 := 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 formalization of the original block-Lanczos interval-occupancy conjecture, via the stronger full-prefix theorem and exact finite-dimensional real linear algebra.
Let $A\in\mathbb R^{n\times n}$ be symmetric and $V\in\mathbb R^{n\times p}$ of full column rank, and suppose the block Krylov space $\mathcal K_s$ has full dimension $sp$. For all $1\le k<j\le s$ and $1\le i\le(k-1)p$, with Ritz values listed with multiplicity, the open interval $(\theta_i^{(k)},\theta_{i+p}^{(k)})$ between Ritz values of iteration $k$ contains a Ritz value of iteration $j$. Suppose the compression …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, KE-04/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00089, "Strict interlacing across block Lanczos iterations", clopen.solutions.