Grothendieck's theorem for Bessel sequences

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^{\mathrm{\infty }}([0,1])$ such that for all $j,k\in \mathbb{N}$ one has $$⟨x_j,x_k⟩={\int }_0^1{f}_j(x)\overline{f_k(x)}dx\mathrm{.}$$ 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 $\lambda ([0,1]\setminus E{)}^{-1\mathrm{/}2}$ on $[0,1]\setminus E$. A formalization of our main result in Lean 4 accompanies the paper.