Local Hölder continuity of 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$. By a theorem of Elsner, the spectral radius on $\mathbb{C}^{d \times d}$ is locally Hölder continuous of order $1/d$. The joint spectral radius is locally Lipschitz continuous on irreducible families (Wirth), and Epperlein and Wirth proved that it is pointwise Hölder continuous on $\mathcal H_d$ with exponent $1/(d^2+d)$, and locally Hölder continuous with exponent $1/6$ on the families in $\mathcal H_2$ with positive joint spectral radius.
Problem. For every $d \ge 1$ and every $\mathcal M_0 \in \mathcal H_d$, are there $r, C > 0$ such that $$|\widehat\rho(\mathcal M) - \widehat\rho(\mathcal N)| \le C\, d_H(\mathcal M, \mathcal N)^{1/d}$$ for all $\mathcal M, \mathcal N \in \mathcal H_d$ with $d_H(\mathcal M, \mathcal M_0) < r$ and $d_H(\mathcal N, \mathcal M_0) < r$?
Source: Epperlein and Wirth (2025), Conjecture 3 (L1), who credit the suggestion of the exponent 1/d to Jean-Michel Coron (private communication, 2001).
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- DS — Dynamical Systems
- Secondary
- NA, OC
- Keywords
- Hölder continuity, joint spectral radius, 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},
}
@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-mf05,
author = {Townsend, Alex},
title = {{MF-05}: Local Hölder continuity of 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-05/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00090.
namespace RegistryProblems.OP_00090
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-00090: Local Hölder continuity of the joint spectral radius -/
def _root_.RegistryProblems.Problem_OP_00090 : Prop :=
∀ (d : ℕ), 1 ≤ d → ∀ (M0 : Set (Square d)), IsCompact M0 → M0.Nonempty →
∃ r : ℝ, 0 < r ∧ ∃ C : ℝ, 0 < C ∧
∀ M N : Set (Square d),
IsCompact M → M.Nonempty → IsCompact N → N.Nonempty →
canonicalHausdorff M M0 < r → canonicalHausdorff N M0 < r →
|jointSpectralRadius M - jointSpectralRadius N| ≤
C * Real.rpow (canonicalHausdorff M N) (1 / (d : ℝ))
end
end RegistryProblems.OP_00090
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_00090 theorem resolution : RegistryProblems.Problem_OP_00090 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00090" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00090 := 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 Lean verification of the original local two-family Holder assertion for arbitrary nonempty compact complex matrix families. All 14 exact contracts passed local compilation, two independent final source reviews, and actual canonical non-root Linux verification 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-05/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00090, "Local Hölder continuity of the joint spectral radius", clopen.solutions.