The uniform expansion threshold for Toeplitz symbols with higher-order zeros
For an integer $m \ge 3$ let $g_m(\theta) = \bigl(2\sin(\theta/2)\bigr)^{2m}$, let $T_n(g_m) = (\widehat g_{m,j-k})_{j,k=1}^n$ be the $n \times n$ Toeplitz matrix generated by $g_m$, where $\widehat g_{m,k}$ are the Fourier coefficients of $g_m$ on $[-\pi, \pi]$, and let $\lambda_{n,1} \le \dots \le \lambda_{n,n}$ be its eigenvalues. For real continuous functions $d_0, \dots, d_{2m}$ on $[0, \pi]$ write $$R_{p,n,j} = \lambda_{n,j} - \sum_{k=0}^{p} \frac{d_k(j\pi/(n+2))}{(n+2)^k}.$$ For $m = 2$, Barrera, Böttcher, Grudsky and Maximenko proved the analogue of the three properties below, with $2\log(n+2) \le j \le n$ in the second.
Problem. Is it true that for every integer $m \ge 3$ there are such functions, with $d_0 = g_m$, that have the following three properties? (i) For every integer $0 \le p \le 2m-1$ there are $D_p > 0$ and $N_p$ such that $|R_{p,n,j}| \le D_p (n+2)^{-p-1}$ for all $n \ge N_p$ and $1 \le j \le n$. (ii) There are $D_{2m} > 0$ and $N_{2m}$ such that $|R_{2m,n,j}| \le D_{2m} (n+2)^{-2m-1}$ for all $n \ge N_{2m}$ and $\lceil (\log(n+2))^2 \rceil \le j \le n$, with $\log$ the natural logarithm. (iii) There are no $D > 0$ and $N$ such that $|R_{2m,n,j}| \le D (n+2)^{-2m-1}$ for all $n \ge N$ and $1 \le j \le n$.
Source: Barrera, Böttcher, Grudsky and Maximenko (2018), Conjecture 8.4; made precise by OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- FA, SP
- Keywords
- eigenvalue asymptotics, OpenProblemsInNLA, Toeplitz matrices
References
@incollection{barrera2018,
author = {Barrera, Mauricio and B{\"o}ttcher, Albrecht and Grudsky, Sergei M. and Maximenko, Egor A.},
title = {Eigenvalues of even very nice {T}oeplitz matrices can be unexpectedly erratic},
booktitle = {The Diversity and Beauty of Applied Operator Theory},
editor = {B{\"o}ttcher, Albrecht and Potts, Daniel and Stollmann, Peter and Wenzel, David},
series = {Oper. Theory Adv. Appl.},
volume = {268},
publisher = {Birkh{\"a}user},
address = {Cham},
year = {2018},
pages = {51--77},
doi = {10.1007/978-3-319-75996-8_2},
eprint = {1710.05243},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mf21,
author = {Townsend, Alex},
title = {{MF-21}: The uniform expansion threshold for Toeplitz symbols with higher-order zeros},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-functions-and-stability/MF-21/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00096.
namespace RegistryProblems.OP_00096
noncomputable section
/-- The source symbol, exactly (2 sin(theta/2))^(2m). -/
def symbol (m : ℕ) (theta : ℝ) : ℝ :=
(2 * Real.sin (theta / 2)) ^ (2 * m)
/-- Signed-binomial candidate for the Fourier coefficient at distance d.
`Nat.choose` is zero for d > m; there is no periodic wraparound. -/
def coefficient (m d : ℕ) : ℝ :=
(-1 : ℝ) ^ d * ((2 * m).choose (m + d) : ℝ)
/-- The n-by-n real Toeplitz matrix with zero-based matrix indices.
Formal equality to the source's Fourier integral is proved in FourierCoefficients.lean. -/
def toeplitz (m n : ℕ) : Matrix (Fin n) (Fin n) ℝ :=
fun i j ↦ coefficient m (Nat.dist i.val j.val)
/-- Elementary symmetry needed to invoke the actual spectral theorem. -/
theorem toeplitz_isHermitian (m n : ℕ) : (toeplitz m n).IsHermitian := by
rw [Matrix.isHermitian_iff_isSymm]
ext i j
simp [toeplitz, Matrix.transpose_apply, Nat.dist_comm]
/-- Increasing eigenvalues, with multiplicity. Mathlib's `eigenvalues₀` is
antitone, so `Fin.rev` reverses its order. Index j here means source index j+1. -/
def eigenvalue (m n : ℕ) (j : Fin n) : ℝ :=
(toeplitz_isHermitian m n).eigenvalues₀
(Fin.cast (Fintype.card_fin n).symm j.rev)
/-- The exact source grid: source index j+1, spacing pi/(n+2). -/
def grid (n : ℕ) (j : Fin n) : ℝ :=
((j.val + 1 : ℕ) : ℝ) * Real.pi / ((n : ℝ) + 2)
/-- Natural-log-squared index cutoff, rounded up to a natural number. -/
def cutoff (n : ℕ) : ℕ :=
Nat.ceil ((Real.log ((n : ℝ) + 2)) ^ 2)
/-- Families are independent of matrix dimension and eigenvalue index.
Only entries 0 through 2m are relevant to the target. -/
abbrev Coefficients := ℕ → ℝ → ℝ
def ContinuousCoefficients (m : ℕ) (d : Coefficients) : Prop :=
∀ k ≤ 2 * m, ContinuousOn (d k) (Set.Icc 0 Real.pi)
def remainder (m p n : ℕ) (d : Coefficients) (j : Fin n) : ℝ :=
eigenvalue m n j -
∑ k ∈ Finset.range (p + 1), d k (grid n j) / ((n : ℝ) + 2) ^ k
/-- Constants may depend on m,p,d, but not on n or j. -/
def UniformOrder (m p : ℕ) (d : Coefficients) : Prop :=
∃ D : ℝ, 0 < D ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ j : Fin n,
|remainder m p n d j| ≤ D / ((n : ℝ) + 2) ^ (p + 1)
/-- The order 2m estimate holds only at or above the source cutoff. -/
def BulkTopOrder (m : ℕ) (d : Coefficients) : Prop :=
∃ D : ℝ, 0 < D ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ j : Fin n,
cutoff n ≤ j.val + 1 →
|remainder m (2 * m) n d j| ≤ D / ((n : ℝ) + 2) ^ (2 * m + 1)
/-- All three original assertions use one continuous coefficient family.
The leading coefficient agrees with the symbol on the entire closed interval. -/
def TargetAt (m : ℕ) : Prop :=
∃ d : Coefficients, ContinuousCoefficients m d ∧
(∀ x ∈ Set.Icc 0 Real.pi, d 0 x = symbol m x) ∧
(∀ p : ℕ, p ≤ 2 * m - 1 → UniformOrder m p d) ∧
BulkTopOrder m d ∧ ¬ UniformOrder m (2 * m) d
/-- OP-00096: The uniform expansion threshold for Toeplitz symbols with higher-order zeros -/
def _root_.RegistryProblems.Problem_OP_00096 : Prop :=
∀ m : ℕ, 3 ≤ m → TargetAt m
end
end RegistryProblems.OP_00096
Formalised by OpenAI Codex AI agents (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_00096 theorem resolution : RegistryProblems.Problem_OP_00096 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00096" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00096 := 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 an integer $m\ge3$ let $\lambda_{n,1}\le\cdots\le\lambda_{n,n}$ be the eigenvalues of the Toeplitz matrix $T_n(g)$ generated by $g(\theta)=(2-2\cos\theta)^m$, and put $h=(n+2)^{-1}$. There are real $C^\infty$ functions $d_0=g,d_1,\ldots,d_{2m}$ on $[0,\pi]$, given by an explicit phase built from the stable roots of the characteristic equation, such that $\lambda_{n,j}-\sum_{k=0}^p d_k(j\pi h)h^k=O(h^{p+1})$ uniformly in $j$ for every $p\le2m-1$, and for $p=2m$ when $j\ge\lceil(\log(n+2))^2\rceil$, while the …
Complete symbolic Lean proof of the original three-part target, continuous-family obstruction, smooth common coefficients, sharp finite-head and global errors, and exact Fourier-matrix correspondence. All five contracts passed actual non-root Linux Comparator and default-kernel acceptance at the recorded immutable proof revision.
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MF-21/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00096, "The uniform expansion threshold for Toeplitz symbols with higher-order zeros", clopen.solutions.