Bounded-function correlation representations of Bessel sequences

Can the full Gram matrix of every countable complex Hilbert-space Bessel sequence of bound 1 be represented as correlations of functions on [0,1] bounded in modulus by 1? Diagonal entries must be preserved as well as off-diagonal correlations.

Why it matters and what counts as progress

Why it matters: Preserving the complete Gram matrix, including diagonals, gives a sharp bounded-function representation beyond earlier finite or real cases.

What counts as progress: Prove a sharp bounded-function representation for countable sequences or determine which restrictions prevent such a representation.

How the problem developed

1953 · Theorem [1]
Alexander Grothendieck Proved the correlation representation now underlying Grothendieck’s theorem, with a universal comparison constant for pairs of vector families.
2012 · Open question recorded [1]
Gilles Pisier Recorded Olevskii’s question about a uniform one-function correlation representation for Bessel sequences.
12 Aug 2026 · Theorem [2]
Liehr, Taylor, and Yu Proved the one-function representation for countable complex Bessel sequences with constant 1, including the diagonal correlations.

AI contribution

Grothendieck's theorem for Bessel sequences

Lukas Liehr, Mitchell A. Taylor, Peiyang Yu

Liehr, Taylor and Yu prove that every countable Bessel sequence of bound 1 in a complex Hilbert space has its full Gram matrix, including diagonal entries, represented by correlations of complex functions on [0,1] bounded in modulus by 1.

AI involvementAI-centered

ImportanceMajor

Technical verificationFormal (Lean 4/Mathlib kernel, Comparator and NanoDa)

Human understandingFull