Abstract Bessel sequences and their Gram kernels

Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, Mathlib API, and compilation changes.

def GrothendieckBessel.besselGram {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (x : ℕ → H) : ℕ → ℕ → ℂ

The paper-convention Gram kernel of an abstract Hilbert-space sequence.

Equations

• GrothendieckBessel.besselGram x j k = inner ℂ (x k) (x j)

theorem GrothendieckBessel.besselGram_conj_symm {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (x : ℕ → H) (j k : ℕ) : besselGram x k j = star (besselGram x j k)

Conjugate symmetry of the abstract Gram kernel.

theorem GrothendieckBessel.besselGram_quadratic_eq_norm_sq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (x : ℕ → H) (F : Finset ℕ) (c : ℕ → ℂ) : (∑ j ∈ F, ∑ k ∈ F, c j * star (c k) * besselGram x j k).re = ‖∑ j ∈ F, c j • x j‖ ^ 2

The finite Gram quadratic form is the squared norm of the vector sum.

theorem GrothendieckBessel.besselGram_finite_positive_contraction {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (x : ℕ → H) (hx : BesselSequenceBoundOne x) : FiniteHermitianPositiveContraction (besselGram x)

A Bessel sequence with bound one has a finite positive-contraction Gram kernel.