Grothendieck's theorem for Bessel sequences

Source: arxiv:2608.12280, url:https://github.com/lukasliehr/GrothendieckBessel/tree/f1ad1c7680bce2b1ab4218a02bddd694fb57062a Authors: Lukas Liehr, Mitchell A. Taylor, Peiyang Yu Status: verified Main declarations: GrothendieckBessel.main Tags: functional-analysis, bessel-sequences, gram-matrices MSC: 46B15, 46B25, 46C05

Countable Grothendieck--Bessel Gram representation, with proofs

Proof-carrying counterpart to the declaration in Showcase.lean. Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, Mathlib API, and compilation changes.

theorem GrothendieckBessel.main_withProof (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] (x : ℕ → H) (hx : BesselSequenceBoundOne x) : ∃ (f : ℕ → ℝ → ℂ), (∀ (j : ℕ), MeasureTheory.AEStronglyMeasurable (f j) μ) ∧ (∀ (j : ℕ), ∀ t ∈ unitInterval, ‖f j t‖ ≤ 1) ∧ ∀ (j k : ℕ), inner ℂ (x k) (x j) = ∫ (t : ℝ) in unitInterval, f j t * star (f k t)

theorem GrothendieckBessel.main (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] (x : ℕ → H) (hx : BesselSequenceBoundOne x) : ∃ (f : ℕ → ℝ → ℂ), (∀ (j : ℕ), MeasureTheory.AEStronglyMeasurable (f j) μ) ∧ (∀ (j : ℕ), ∀ t ∈ unitInterval, ‖f j t‖ ≤ 1) ∧ ∀ (j k : ℕ), inner ℂ (x k) (x j) = ∫ (t : ℝ) in unitInterval, f j t * star (f k t)

Comparator-facing proved counterpart to GrothendieckBessel.main in Showcase.lean. The existing main_withProof entry point is retained.