A pointwise Lipschitz lower bound for the joint spectral radius
Let $\mathcal H_d$ be the set of nonempty compact subsets of $\mathbb{C}^{d \times d}$, with the Hausdorff distance $d_H$ induced by the spectral norm $\|\cdot\|_2$, and let $\widehat\rho(\mathcal M)$ be the joint spectral radius of $\mathcal M \in \mathcal H_d$. For a single matrix $A$, analytic perturbation theory gives $\Gamma, \varepsilon_0 > 0$ with $\rho(A + \varepsilon B) \ge \rho(A) - \Gamma\varepsilon$ whenever $\|B\|_2 \le 1$ and $0 < \varepsilon < \varepsilon_0$; the bound below is its analogue for the joint spectral radius. It holds at irreducible families, where the joint spectral radius is locally Lipschitz continuous (Wirth), and Epperlein and Wirth proved that the joint spectral radius is pointwise Hölder continuous on $\mathcal H_d$ with exponent $1/(d^2+d)$.
Problem. For every $d \ge 1$ and every $\mathcal M \in \mathcal H_d$, are there $r, C > 0$ such that $$\widehat\rho(\mathcal N) \ge \widehat\rho(\mathcal M) - C\, d_H(\mathcal M, \mathcal N)$$ for every $\mathcal N \in \mathcal H_d$ with $d_H(\mathcal M, \mathcal N) < r$?
Source: Epperlein and Wirth (2025), Conjecture 3 (P2), with exponent 1.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- DS — Dynamical Systems
- Secondary
- NA, OC
- Keywords
- joint spectral radius, OpenProblemsInNLA, perturbation bounds
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},
}
@article{wirth2002,
author = {Wirth, Fabian},
title = {The generalized spectral radius and extremal norms},
journal = {Linear Algebra Appl.},
volume = {342},
number = {1-3},
year = {2002},
pages = {17--40},
doi = {10.1016/S0024-3795(01)00446-3},
}
@misc{openproblemsinnla-mf06,
author = {Townsend, Alex},
title = {{MF-06}: A pointwise Lipschitz lower bound for the joint spectral radius},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-functions-and-stability/MF-06/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00091.
namespace RegistryProblems.OP_00091
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 WordIn {d : ℕ} (M : Set (Square d)) (w : List (Square d)) : Prop :=
∀ A ∈ w, A ∈ 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}
/-- The literal infimum in the canonical spectral Hausdorff formula.
Nonempty compact families are required by all correspondence contracts. -/
def pointFamilyDistance {d : ℕ} (A : Square d) (N : Set (Square d)) : ℝ :=
sInf ((fun B : Square d => spectralNorm (A - B)) '' N)
/-- The directed supremum in the canonical formula. -/
def directedSpectralDistance {d : ℕ} (M N : Set (Square d)) : ℝ :=
sSup ((fun A : Square d => pointFamilyDistance A N) '' M)
/-- The original max-of-two-sup-inf formula, with the actual spectral norm. -/
def canonicalHausdorff {d : ℕ} (M N : Set (Square d)) : ℝ :=
max (directedSpectralDistance M N) (directedSpectralDistance N M)
/-- OP-00091: A pointwise Lipschitz lower bound for the joint spectral radius -/
def _root_.RegistryProblems.Problem_OP_00091 : Prop :=
∀ (d : ℕ), 1 ≤ d → ∀ (M : Set (Square d)), IsCompact M → M.Nonempty →
∃ r : ℝ, 0 < r ∧ ∃ C : ℝ, 0 < C ∧
∀ N : Set (Square d), IsCompact N → N.Nonempty →
canonicalHausdorff M N < r →
jointSpectralRadius M - C * canonicalHausdorff M N ≤ jointSpectralRadius N
end
end RegistryProblems.OP_00091
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_00091 theorem resolution : RegistryProblems.Problem_OP_00091 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00091" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00091 := 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 fixed nonempty compact complex matrix family in every positive finite dimension, prove a one-sided linear lower perturbation bound for its joint spectral radius, uniformly over arbitrary nearby nonempty compact families. The proof includes the actual critical product-bounded exterior-power construction.
For every $d\ge1$ and every fixed nonempty compact family $\mathcal M\subseteq\mathbb C^{d\times d}$ there are $C,r>0$ such that every nonempty compact $\mathcal N$ with $d_H(\mathcal M,\mathcal N)<r$ satisfies $\widehat\rho(\mathcal N)\ge\widehat\rho(\mathcal M)-C\,d_H(\mathcal M,\mathcal N)$. This is the pointwise one-sided Lipschitz lower bound for the joint spectral radius. For a product-bounded reference family, a limiting seminorm and a cone argument build words …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MF-06/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00091, "A pointwise Lipschitz lower bound for the joint spectral radius", clopen.solutions.