Pith. sign in

REVIEW 6 minor 23 references

Grothendieck's theorem for Bessel sequences

T0 review · 0 major / 6 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Every Bessel sequence with Bessel bound 1 has its inner products reproduced by unit-bounded functions on [0,1], with the optimal constant 1.

desk verdict Sharp K=1 Grothendieck theorem for Bessel sequences, solving Olevskii's problem; the math is solid, but the Lean formalization is not yet reproducible as written. read the letter →

arxiv 2608.12280 v1 pith:KOWDRHUB submitted 2026-08-12 math.FA math.CA

Lukas Liehr , Mitchell A. Taylor , Peiyang Yu This is my paper · ORCID
classification math.FAmath.CA MSC 46B1546B2542C1568V20
keywords GrothendiecktheoremBesselsequencesGrammatrixfactorizationorthonormalextensionboundedorthogonalsystemsconvexhullofrank-onematricesformalizedmathematics
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper establishes a sharp, diagonal-preserving version of Grothendieck's theorem for Bessel sequences. It proves that if a countable family of vectors in a Hilbert space has Bessel bound 1, then its Gram matrix can be represented exactly as the $L^2([0,1])$ inner-product matrix of functions from the unit ball of $L^\infty([0,1])$, with constant 1 and no larger constant possible. This matters because it settles an open extension problem: any Bessel sequence in $L^2(E)$ with bound 1 extends to an orthonormal system on all of $[0,1]$, with an optimal pointwise bound on the complement of $E$. The proof runs through a finite-dimensional convex-geometric statement, an infinite passage by compactness, and a reported machine-checked formalization of the main existence claim.

What carries the argument

The load-bearing device is the finite-dimensional convex-geometric statement that every real symmetric matrix $G$ with $0 \le G \le I$ lies in the convex hull of $\{xx^T : x \in [-1,1]^N\}$; the complex analogue is obtained by doubling the dimension. Its proof compares support functions: for fixed symmetric $A$, the maximum of $\langle A, G\rangle$ over such $G$ is $\mathrm{tr}(A_+)$, while the corresponding maximum over the convex hull of rank-one box matrices is $\max_{x \in [-1,1]^N} x^T A x$. A quoted geometric theorem supplies a vector $w$ in the positive spectral subspace with $w^T A w \ge \mathrm{tr}(A_+)$ and $|\langle w,e_j\rangle| \le 1$ for every standard basis vector $e_j$, exactly bridging the two quantities. The finite convex combination is turned into piecewise-constant functions on $[0,1]$; a compactness argument in the space of probability measures on the countable product of closed disks, using a realization lemma, upgrades the representation to countably many vectors.

What would settle it

For a small fixed dimension, say $N=2$ or $N=3$, sample symmetric matrices $A$ and compare $\max_{x \in [-1,1]^N} x^T A x$ with $\mathrm{tr}(A_+)$: the paper's finite-dimensional claim is exactly that the maximum is never smaller than the trace, so a single numerical counterexample would refute the convex-hull statement from which the main theorem follows.

Watch

Extended reading notes

Core claim

The paper's central claim is that the Gram matrix of any Bessel sequence with bound 1 is, with no rescaling, the matrix of inner products of a sequence of functions each bounded in modulus by 1 on $[0,1]$, and that this is optimal because a unit vector already forces the constant to be at least 1. In Gram-matrix language: every Hermitian matrix $G$ with $0 \le G \le I$ is a convex combination of rank-one matrices $\zeta\zeta^*$ with $\zeta$ in the closed unit disk $\mathbb{D}$, from which simple functions on a partition of $[0,1]$ give the integral representation. A weak-compactness argument over probability measures on the infinite product of disks passes to countably infinite Gram matrices, and a measure-preserving rearrangement lemma transfers the representation from $[0,1]$ to any subset $A$ of positive measure. The authors draw the consequence that every Bessel sequence on $L^2(E)$ extends to an orthonormal system on $[0,1]$ with optimal pointwise bound on the complement, and they report a machine-checked formalization of the main existence theorem with constant 1.

Load-bearing premise

The entire proof hinges on a quoted finite-dimensional geometric theorem guaranteeing that, for the positive part of any symmetric matrix, a vector $w$ can be chosen with $|\langle w,e_j\rangle| \le 1$ for every standard basis vector $e_j$ and with $w^T A w$ at least the trace of that positive part; if the theorem is false or its hypotheses are not met by the projected vectors in the proof, the finite-dimensional core and with it the main theorem collapse.

Editorial extensions

If this is right

  • Every Hermitian matrix $G$ with $0 \le G \le I$, finite or countable, is entrywise the matrix $\int_0^1 f_j \overline{f_k}\,dx$, with each $|f_j| \le 1$ and no rescaling; the constant $1$ cannot be improved.
  • Every Bessel sequence in $L^2(E)$ with bound 1 extends to an orthonormal system on $[0,1]$ whose functions are bounded on the complement by $\lambda([0,1]\setminus E)^{-1/2}$.
  • The bound in the extension theorem is optimal for every measurable set $E$ whose complement has positive measure.
  • The result closes the diagonal gap left by earlier off-diagonal constructions: diagonal entries are preserved while the constant stays exactly 1.
  • In Gram-matrix terms, all positive semidefinite matrices between $0$ and $I$ are convex combinations of rank-one matrices generated by vectors in $[-1,1]^N$ in the real case and by points of the closed unit disk in the complex case.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • An unstated corollary of the compactness route is that the representation should survive for index sets of any cardinality: the finite-intersection argument works on the product of disks regardless of the index set, so countability looks like a convenience of presentation rather than a necessity.
  • The finite-dimensional core is a concrete membership problem that can be probed independently: for fixed $N$, checking whether every $0 \le G \le I$ lies in the convex hull of box rank-one matrices is a finite convex optimization question, so numerical search over small dimensions would be an inexpensive check of the argument.
  • The machine-checked version establishes existence but not the one-line optimality of $K=1$ nor the extension theorem; completing those formalizations is a natural next step.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 6 minor

Summary. The paper establishes a sharp infinite-dimensional version of Grothendieck's theorem for Bessel sequences: for any Hilbert space H and any Bessel sequence {x_j} with Bessel bound 1, there are functions f_j in the unit ball of L∞([0,1]) with ⟨x_j,x_k⟩ = ∫ f_j \overline{f_k} for all j,k, and the constant 1 is optimal. The proof proceeds through a finite-dimensional convex-geometric statement (Proposition 2.3), proved via the Ball–Prodromou theorem, a complex lifting step (Corollary 2.4), a compactness argument for the passage from finite to countable index sets (Theorem 2.7), and a measure-preserving change of variables (Lemma 2.8) that yields the application to Olevskii's extension problem (Theorem 1.2) with an optimal constant. An appendix describes a Lean 4 formalization of the main theorem.

Significance. If correct, the result resolves a well-known open problem attributed to Olevskii, as stated in Pisier's survey, and it sharpens Kashin's off-diagonal result by preserving the diagonal and achieving the optimal constant K=1. The proof is clean and essentially parameter-free: the only external input is the Ball–Prodromou theorem, and the optimality lower bound is a one-line argument. The claimed Lean formalization, if in a reproducible state, would be a valuable machine-checked companion.

minor comments (6)
  1. [§3.4 and the GitHub repository] The formalization is not reproducible as a fixed state: no commit hash or archive is given, and Showcase.lean is said to contain two `sorry`s. The paper should pin the repository to a specific commit and state explicitly that Showcase_WithProofs.lean is the machine-checked artifact, so that the formalization claim can be verified at a fixed state.
  2. [Theorems 1.1, 2.5, 2.7 and proof of Theorem 2.5] The constant is stated as '0 < K < 1' in several places, but the theorem then asserts K=1 and proves optimality; the upper bound '< 1' is inconsistent and should read '0 < K' (or 'K > 0').
  3. [Theorem 2.7, definition of C_jk and final display] The kernel is written z_j z_k, but the complex representation from Corollary 2.4 and Theorem 2.5 gives moments with kernel z_j \overline{z_k}; with the printed kernel the finite-dimensional moments do not verify membership in C_jk. The argument should use z_j \overline{z_k} throughout, and with that replacement the closedness and compactness reasoning are unaffected.
  4. [Corollary 2.4 and Theorem 2.5] The displayed identity should be ζ_j^{(r)} \overline{ζ_k^{(r)}}; the overline is missing in the text. The same missing conjugation appears in the display for g_jk in §1.5 and in the statement of Theorem 2.5.
  5. [Proofs of Theorem 2.5 and Theorem 2.7] In the proof of Theorem 2.5, 'By Proposition 2.4' should be 'By Corollary 2.4'; in the proof of Theorem 2.7, the phrase 'Gram matrix of {x_j}_{j∈F}' should be 'the matrix H_F', since the vectors x_j are not otherwise defined in that proof; and in Theorem 2.5 the quantity in the statement should be G_jk, not ⟨x_j,x_k⟩.
  6. [Theorem 2.1] The notation ∑ u_j · u_j = I_E should be explained as the sum of outer products; the verification in Proposition 2.3 relies on this interpretation.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular reasoning: finite core uses external Ball–Prodromou theorem; no fitted constants or self-citation chain.

full rationale

The derivation is self-contained in the relevant sense. The finite-dimensional core (Proposition 2.3) proves G ⊂ conv{xxᵀ : x ∈ [-1,1]^N} by support functions. Its only non-elementary input is the Ball–Prodromou theorem (Theorem 2.1), quoted from [3], an external published theorem by different authors; the paper explicitly verifies the hypothesis Σ u_j u_jᵀ = I_E before applying it, so no input of the target result is smuggled in. Corollary 2.4 and Theorem 2.5 then pass from the convex decomposition to simple L^∞ functions using only a partition of [0,1]; no parameter appearing in the conclusion is fitted to the data. Theorem 2.7 extends to countable Gram matrices by a standard compactness/finite-intersection-property argument together with Billingsley’s realization lemma; this is not an equivalent reformulation of the conclusion. The optimality of K = 1 is the separate one-line lower bound 1 = ⟨x_j,x_j⟩ = K∫|f_j|² ≤ K, not an output of the construction. The Olevskii application (Theorem 1.2) uses the main theorem on I − G and Lemma 2.8’s measure-preserving rescaling, so it is not definitionally forced. The only self-citation ([6]) appears as an example of prior formalization work, not as evidence; the Lean companion files are not used to justify the mathematics. Minor issues — the conflicting wording “0 < K < 1” followed by “one can choose K = 1”, and the unpinned Lean repository with sorrys in Showcase.lean — are presentation and reproducibility concerns, not circularity.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

No free parameters appear: K=1 and the extension bound are absolute constants proven optimal. No new entities are postulated; the functions f_j and v_j are constructed from the given data. The proof relies on standard theorems from convex geometry, spectral theory, and measure theory, plus the Ball-Prodromou theorem, which is quoted from the literature rather than reproved.

assumptions (6)
  • standard math Ball-Prodromou theorem: if u_1,...,u_N in a finite-dimensional real inner product space E satisfy Σ u_j u_j^T = I_E and Q is self-adjoint positive semidefinite, then some w ∈ E has <Qw,w> ≥ tr(Q) and |<w,u_j>| ≤ 1.
    Quoted as [3, Thm 1.4]; it supplies the vector in [-1,1]^N that realizes the support function lower bound in Proposition 2.3.
  • standard math Support-function characterization of convex hulls (Lemma 2.2): if the support of K is at most the support of L in every direction, then K is contained in L.
    Used to prove G ⊆ C in Proposition 2.3 by comparing α(A) and β(A).
  • standard math Spectral theorem for symmetric and Hermitian matrices, including the positive and negative spectral parts A_+, A_- and the projection P_E(A).
    Used in Proposition 2.3 for the identity α(A)=tr(A_+) and in Corollary 2.4 for the real 2N-dimensional embedding of a Hermitian matrix.
  • standard math Compactness of the set of Borel probability measures on a compact metric space, via Riesz-Markov-Kakutani and Banach-Alaoglu.
    Used in Theorem 2.7 to pass from finite intersection property to a measure satisfying all Gram-matrix constraints simultaneously.
  • standard math Every Borel probability measure on a compact metric space is a pushforward of Lebesgue measure under a Borel map (Lemma 2.6, from Billingsley).
    Used at the end of Theorem 2.7 to convert the measure on D^N into measurable functions on [0,1].
  • standard math Carathéodory's theorem and finite dimensionality imply that the convex hull of a compact set is compact.
    Used in Proposition 2.3 to prove the compactness of C = conv{xx^T : x ∈ [-1,1]^N}.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Grothendieck's theorem for Bessel sequences." pith.science (2026). https://pith.science/paper/KOWDRHUB

@misc{pith2026260812280,
  author       = {Pith},
  title        = {Pith review of: Grothendieck's theorem for Bessel sequences},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KOWDRHUB}},
  note         = {Machine review of arXiv:2608.12280}
}
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 $\lambda([0,1]\setminus E)^{-1/2}$ on $[0,1]\setminus E$. A formalization of our main result in Lean 4 accompanies the paper.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

23 extracted references · 18 canonical work pages

  1. [1]

    Quadratic forms on graphs

    Noga Alon, Konstantin Makarychev, Yury Makarychev, and Assaf Naor. Quadratic forms on graphs. Invent. Math. , 163(3):499–522, 2006

    work page 2006

  2. [2]

    Formalization of De Giorgi–Nash–Moser Theory in Lean

    Scott Armstrong and Julia Kempe. Formalization of De Giorgi–Nash–Moser Theory in Lean. arXiv preprint arXiv:2604.05984 , 2026

    arXiv 2026

  3. [3]

    Ball and Maria Prodromou

    Keith M. Ball and Maria Prodromou. A sharp combinatorial version of Vaaler’s theorem. Bull. Lond. Math. Soc. , 41(5):853–858, 2009

    work page 2009

  4. [4]

    Weak convergence of measures: Applications in probability , volume No

    Patrick Billingsley. Weak convergence of measures: Applications in probability , volume No. 5 of Conference Board of the Mathematical Sciences Regional Conference Series in Applied Mathematics. Society for Industrial and Applied Mathematics, Philadelphia, PA, 1971

    work page 1971

  5. [5]

    Maximizing quadratic programs: extending Grothendieck’s inequality

    Moses Charikar and Anthony Wirth. Maximizing quadratic programs: extending Grothendieck’s inequality. In 45th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2004) , pages 54–60. IEEE Computer Society, 2004

    work page 2004

  6. [6]

    Cantor measures with odd base do not admit Fourier frames

    Jaume de Dios de Dios Pont, Lukas Liehr, and Mitchell A Taylor. Cantor measures with odd base do not admit Fourier frames. arXiv preprint arXiv:2607.08656 , 2026

    arXiv 2026

  7. [7]

    The Lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28 , volume 12699 of Lecture Notes in Computer Science, pages 625–635, Cham, 2021. Springer

    work page 2021

  8. [8]

    Résumé de la théorie métrique des produits tensoriels topologiques

    Alexander Grothendieck. Résumé de la théorie métrique des produits tensoriels topologiques. Bol. Soc. Mat. São Paulo , 8:1–79, 1953

    work page 1953

Show all 23 references
  1. [9]

    A Milestone in Formalization: The Sphere Pack- ing Problem in Dimension 8

    Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, and Maryna Viazovska. A Milestone in Formalization: The Sphere Pack- ing Problem in Dimension 8. arXiv preprint arXiv:2604.23468 , 2026

    2026 arXiv

  2. [10]

    Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium

    Vasily Ilin. Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium. arXiv preprint arXiv:2603.15929 , 2026

    2026

  3. [11]

    Theorie der Orthogonalreihen , volume VI of Mono- grafje Matematyczne

    Stefan Kaczmarz and Hugo Steinhaus. Theorie der Orthogonalreihen , volume VI of Mono- grafje Matematyczne. Seminarjum Matematyczne Uniwersytetu Warszawskiego, Warszawa– Lwów, 1936

    1936

  4. [12]

    B. S. Kashin. An observation on the Gram matrices of systems of uniformly bounded func- tions and a problem of Olevskii. Russian Math. Surveys , 77(1):171–173, 2022. Translated from Uspekhi Mat. Nauk 77 (2022), no. 1, 183–184

    2022

  5. [13]

    B. S. Kashin and S. J. Szarek. On the Gram matrices of systems of uniformly bounded functions. Proc. Steklov Inst. Math. , 243:227–233, 2003. Translated from Tr. Mat. Inst. Steklova 243 (2003), 237–243

    2003

  6. [14]

    Kashin and Stanislaw J

    Boris S. Kashin and Stanislaw J. Szarek. The Knaster problem and the geometry of high- dimensional cubes. C. R. Math. Acad. Sci. Paris , 336(11):931–936, 2003

    2003

  7. [15]

    Relaxations of quadratic programs in operator theory and system analysis

    Alexandre Megretski. Relaxations of quadratic programs in operator theory and system analysis. In Systems, Approximation, Singular Integral Operators, and Related Topics (Bor- deaux, 2000) , volume 129 of Oper. Theory Adv. Appl. , pages 365–392. Birkhäuser, Basel, 2001

    2000

  8. [16]

    Menchoff

    D. Menchoff. Sur les séries de fonctions orthogonales bornées dans leur ensemble. Rec. Math. [Mat. Sbornik] N.S. , 3(45)(1):103–120, 1938

    1938

  9. [17]

    Joseph K. Miller. A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game. arXiv preprint arXiv:2607.08986, 2026

    2026 arXiv

  10. [18]

    On maximization of quadratic form over intersection of ellipsoids with common center

    Arkadi Nemirovski, Cornelis Roos, and Tamás Terlaky. On maximization of quadratic form over intersection of ellipsoids with common center. Math. Program., 86(3):463–473, 1999

    1999

  11. [19]

    A. M. Olevskii. On the extension of a sequence of functions to a complete orthonormal system. Math. Notes Acad. Sci. USSR , 6(6):908–913, 1969. Translated from Mat. Zametki 6 (1969), no. 6, 737–747

    1969

  12. [20]

    A. M. Olevskii. Fourier Series with Respect to General Orthogonal Systems , volume 86 of Ergebnisse der Mathematik und ihrer Grenzgebiete . Springer-Verlag, New York–Heidelberg, 1975. GROTHENDIECK’S THEOREM FOR BESSEL SEQUENCES 15

    1975

  13. [21]

    Grothendieck’s theorem, past and present

    Gilles Pisier. Grothendieck’s theorem, past and present. Bull. Amer. Math. Soc. (N.S.) , 49(2):237–323, 2012

    2012

  14. [22]

    Tyrrell Rockafellar

    R. Tyrrell Rockafellar. Convex analysis , volume No. 28 of Princeton Mathematical Series . Princeton University Press, Princeton, NJ, 1970

    1970

  15. [23]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , pages 367–381, New York, NY, 2020. ACM. Department of Mathematics, Bar-Ilan University, Ramat-Gan 5290002, Israel ...

    2020

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.