Countable Gram-kernel conventions

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

def GrothendieckBessel.unitInterval : Set ℝ

The unit interval [0,1].

Equations

• GrothendieckBessel.unitInterval = Set.Icc 0 1

@[reducible, inline]

noncomputable abbrev GrothendieckBessel.μ : MeasureTheory.Measure ℝ

Lebesgue measure restricted to [0,1].

Equations

• GrothendieckBessel.μ = MeasureTheory.volume.restrict GrothendieckBessel.unitInterval

def GrothendieckBessel.BesselSequenceBoundOne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (x : ℕ → H) : Prop

A Bessel sequence in a complex Hilbert space with bound 1, expressed by the standard inequality for all finitely supported coefficient families.

Equations

• GrothendieckBessel.BesselSequenceBoundOne x = ∀ (F : Finset ℕ) (c : ℕ → ℂ), ‖∑ j ∈ F, c j • x j‖ ^ 2 ≤ ∑ j ∈ F, ‖c j‖ ^ 2

@[reducible, inline]

noncomputable abbrev GrothendieckBessel.μOn (S : Set ℝ) : MeasureTheory.Measure ℝ

Lebesgue measure restricted to a measurable set.

Equations

• GrothendieckBessel.μOn S = MeasureTheory.volume.restrict S

noncomputable def GrothendieckBessel.l2InnerOn (S : Set ℝ) (f g : ℝ → ℂ) : ℂ

The linear-in-the-first L² correlation on a measurable set.

Equations

• GrothendieckBessel.l2InnerOn S f g = ∫ (t : ℝ), f t * star (g t) ∂GrothendieckBessel.μOn S

def GrothendieckBessel.FiniteHermitianPositiveContraction {J : Type u_1} (h : J → J → ℂ) : Prop

Every finite quadratic form of the kernel is nonnegative and bounded above by the coefficient ℓ² norm. This is the finite positive-contraction condition used in the compactness argument.

Equations

• One or more equations did not get rendered due to their size.