Grothendieck's theorem for Bessel sequences
Lukas Liehr, Mitchell A. Taylor, Peiyang Yu
math.FA
Aug 12, 2026 · v1
math.CA
TL;DR
The main sharp Grothendieck-type theorem for Bessel sequences is formalized in Lean 4 accompanying the paper.
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.
Problem
Establish a sharp version of Grothendieck's theorem for Bessel sequences, representing Hilbert space inner products as correlations of uniformly bounded L^infinity functions, and resolve an extension problem of Olevskii for orthonormal systems.
Approach
The authors prove a finite-dimensional version using the Ball–Prodromou theorem and characterization of convex sets via support functions, then pass to the infinite case. A Lean 4 formalization of the main result accompanies the paper.
Results
For any Bessel sequence with bound 1 in a Hilbert space, there exist functions in the unit ball of L^infinity([0,1]) whose correlations reproduce the inner products. As an application, Bessel sequences in L^2(E) extend to orthonormal systems in L^2([0,1]) with an optimal bounding constant.
