Grothendieck's theorem for Bessel sequences

Abstract

We establish a sharp version of Grothendieck's theorem for Bessel sequences. Precisely, given a Bessel sequence $\{ x_j \}_{j\in\mathbb{N}}$ with Bessel bound $1$ in a Hilbert space, we show that there exists functions $\{ f_j \}_{j\in\mathbb{N}}$ belonging to the unit ball of $L^\infty([0,1])$ such that for all $j,k \in \mathbb{N}$ one has $$ \langle x_j,x_k\rangle = \int_0^1 f_j(x)\overline{f_k(x)}\,dx.$$ As an application, we give an affirmative answer to an extension problem of Olevskii: if $E \subset [0,1]$ is a Lebesgue measurable set such that $[0,1]\setminus E$ has positive measure, then every Bessel sequence in $L^2(E)$ with Bessel bound $1$ extends to an orthonormal system in $L^2([0,1])$ that is bounded by the (optimal) constant $λ([0,1]\setminus E)^{-1/2}$ on $[0,1]\setminus E$. A formalization of our main result in Lean 4 accompanies the paper.

Disclosure

“ended to a complete uniformly bounded orthonormal system. The completeness aspect is not addressed in the present paper. Usage of Large Language Models. Theorem 2.5 (for the case of real Hilbert spaces) was developed with the assistance of GPT-5.4. Specifically, the result of Ball and Prodromou [3], which was known to the authors, was provided to GPT- 5.4. GPT-5.4 was then guided toward a construction of the functions fj given in (2.1). The resulting functions provided a version of”

PDF page 4

Classification

Substantial proof generation

Multiplier

10

Verified

2026-08-23T05:11:53.817427Z

Structural counts