Uniform polynomial bounds for products at joint spectral radius one
Let $\mathcal H_d$ be the set of nonempty compact subsets of $\mathbb{C}^{d \times d}$, let $\widehat\rho(\mathcal M)$ be the joint spectral radius of $\mathcal M \in \mathcal H_d$, and let $\|\cdot\|_2$ be the spectral norm. For each $\mathcal M$ with $\widehat\rho(\mathcal M) = 1$ there is a $\Theta$, depending on $\mathcal M$, with $\|A_k \cdots A_1\|_2 \le \Theta k^{d-1}$ for all $k \ge 1$ and $A_1, \dots, A_k \in \mathcal M$. Epperlein and Wirth proved the uniform bound below for $d = 2$, and showed that it would make the joint spectral radius locally Hölder continuous, with exponent $1/(d^2+d)$, on the families with positive joint spectral radius.
Problem. Is there, for every $d \ge 1$, a constant $\Theta_d > 0$ such that every $\mathcal M \in \mathcal H_d$ with $\widehat\rho(\mathcal M) = 1$ satisfies $$\|A_k \cdots A_1\|_2 \le \Theta_d (Lk)^{d-1}, \qquad L = \max_{A \in \mathcal M} \|A\|_2,$$ for all $k \ge 1$ and all $A_1, \dots, A_k \in \mathcal M$?
Source: Epperlein and Wirth (2025), Conjecture 3 (L3).
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- DS — Dynamical Systems
- Secondary
- NA, OC
- Keywords
- joint spectral radius, matrix products, OpenProblemsInNLA
References
@article{epperlein2025,
author = {Epperlein, Jeremias and Wirth, Fabian},
title = {The joint spectral radius is pointwise {H}{\"o}lder continuous},
journal = {Linear Algebra Appl.},
volume = {704},
year = {2025},
pages = {92--122},
doi = {10.1016/j.laa.2024.09.016},
eprint = {2311.18633},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mf07,
author = {Townsend, Alex},
title = {{MF-07}: Uniform polynomial bounds for products at joint spectral radius one},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-functions-and-stability/MF-07/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00092.
namespace RegistryProblems.OP_00092
noncomputable section
abbrev Square (d : ℕ) := Matrix (Fin d) (Fin d) ℂ
/-- Actual complex Euclidean operator norm, with no default entrywise norm. -/
def spectralNorm {d : ℕ} (A : Square d) : ℝ :=
‖Matrix.toEuclideanCLM (n := Fin d) (𝕜 := ℂ) A‖
/-- Chronological order: later factors act on the left. -/
def matrixProduct {d : ℕ} (w : List (Square d)) : Square d := w.reverse.prod
def finiteProduct {d n : ℕ} (A : Fin n → Square d) : Square d :=
matrixProduct (List.ofFn A)
def WordIn {d : ℕ} (M : Set (Square d)) (w : List (Square d)) : Prop :=
∀ A ∈ w, A ∈ M
/-- The actual supremum; compact attainment is an independent obligation. -/
def familyNorm {d : ℕ} (M : Set (Square d)) : ℝ := sSup (spectralNorm '' M)
/-- All words are retained, including repetitions and infinitely many possible
generators. This is not a finite-generator restriction. -/
def wordNorms {d : ℕ} (M : Set (Square d)) (n : ℕ) : Set ℝ :=
{r | ∃ w : List (Square d), w.length = n ∧ WordIn M w ∧
r = spectralNorm (matrixProduct w)}
def familyGrowth {d : ℕ} (M : Set (Square d)) (n : ℕ) : ℝ := sSup (wordNorms M n)
/-- The n=0 value is immaterial to the limit and excluded from the infimum. -/
def rootGrowth {d : ℕ} (M : Set (Square d)) (n : ℕ) : ℝ :=
Real.rpow (familyGrowth M n) (1 / (n : ℝ))
/-- Fekete's infimum formula. Its radius-one equivalence with the canonical
root limit is mandatory; no radius is assigned by definition. -/
def jointSpectralRadius {d : ℕ} (M : Set (Square d)) : ℝ :=
sInf {r : ℝ | ∃ n : ℕ, 1 ≤ n ∧ r = rootGrowth M n}
/-- OP-00092: Uniform polynomial bounds for products at joint spectral radius one -/
def _root_.RegistryProblems.Problem_OP_00092 : Prop :=
∀ (d : ℕ), 1 ≤ d →
∃ Θ : ℝ, 0 < Θ ∧ ∀ M : Set (Square d), IsCompact M → M.Nonempty →
jointSpectralRadius M = 1 → ∀ n : ℕ, 1 ≤ n → ∀ A : Fin n → Square d,
(∀ i, A i ∈ M) →
spectralNorm (finiteProduct A) ≤ Θ * (familyNorm M * (n : ℝ)) ^ (d - 1)
end
end RegistryProblems.OP_00092
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_00092 theorem resolution : RegistryProblems.Problem_OP_00092 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00092" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00092 := 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 original MF-07 result for arbitrary nonempty compact complex matrix families at joint spectral radius one, all positive dimensions and every switching word. All 18 exports passed actual canonical Linux default-kernel, Comparator, axiom and control checks at the immutable proof revision.
For a bounded family of matrices of order $d$, with joint spectral radius one and individual spectral norms at most $L$, every product of length $n$ is bounded by $\Theta_d(Ln)^{d-1}$, where $\Theta_d$ depends only on $d$. The proof uses an approximate extremal norm, a well-rounded coordinate system, and triangular comparison. Diagonal rescaling of a block triangular product is controlled by …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MF-07/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00092, "Uniform polynomial bounds for products at joint spectral radius one", clopen.solutions.