Internal finite Gram API

Finite Gram matrices, their Euclidean operators, and bounded-function predicates used by the finite decomposition and realization theorems. Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, Mathlib API, and compilation changes.

@[reducible, inline]

noncomputable abbrev OlevskiiGram.μ01 : MeasureTheory.Measure ℝ

Lebesgue measure restricted to the open unit interval.

Equations

• OlevskiiGram.μ01 = MeasureTheory.volume.restrict (Set.Ioo 0 1)

def OlevskiiGram.gramMatrix {N : ℕ} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (z : Fin N → H) : Matrix (Fin N) (Fin N) ℂ

The finite Gram matrix, using the paper's inner-product convention.

Equations

• OlevskiiGram.gramMatrix z j k = inner ℂ (z k) (z j)

noncomputable def OlevskiiGram.matrixL2Operator {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) : EuclideanSpace ℂ (Fin N) →L[ℂ] EuclideanSpace ℂ (Fin N)

The continuous Euclidean operator associated to a finite complex matrix.

Equations

• OlevskiiGram.matrixL2Operator A = LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A)

def OlevskiiGram.matrixL2OperatorNormLE {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (C : ℝ) : Prop

An upper bound on the Euclidean operator norm of a finite complex matrix.

Equations

• OlevskiiGram.matrixL2OperatorNormLE A C = (‖OlevskiiGram.matrixL2Operator A‖ ≤ C)

def OlevskiiGram.LInfNormLe (C : ℝ) (f : ℝ → ℂ) : Prop

An essential supremum bound relative to the open-unit-interval measure.

Equations

• OlevskiiGram.LInfNormLe C f = (MeasureTheory.eLpNormEssSup f OlevskiiGram.μ01 ≤ ENNReal.ofReal C)

def OlevskiiGram.RepresentsGramMatrixWithBound {N : ℕ} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (C : ℝ) (z : Fin N → H) (f : Fin N → ℝ → ℂ) : Prop

Bounded functions whose unit-interval correlations represent a finite Gram matrix.

Equations

• OlevskiiGram.RepresentsGramMatrixWithBound C z f = ((∀ (j : Fin N), OlevskiiGram.LInfNormLe C (f j)) ∧ ∀ (j k : Fin N), ∫ (t : ℝ) in Set.Ioo 0 1, f j t * star (f k t) = inner ℂ (z k) (z j))