The finitely supported Gram form of a positive-definite kernel

This file packages the finitely supported Hermitian form attached to a positive-definite kernel. For a kernel K : α → α → 𝕜 and finitely supported coefficient vectors x y : α →₀ 𝕜, the form is

∑ a ∈ x.support, ∑ b ∈ y.support, conj (x a) * y b * K a b.

The diagonal nonnegativity of this form is exactly the Matrix.PosSemidef content in TauCeti.IsPositiveDefiniteKernel, but a named finitely supported form is the object needed by the later GNS/Kolmogorov construction: its null space is quotiented, then completed.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C ("Positive-definite functions and Bochner's theorem"), specifically the positive-definite-kernel / GNS-Kolmogorov API prerequisite. No Mathlib code is vendored; the proofs reuse Mathlib's positive-semidefinite matrix API through TauCeti.IsPositiveDefiniteKernel.

Main declarations

• TauCeti.positiveDefiniteKernelFinsuppForm: the finitely supported Gram form attached to a kernel.
• TauCeti.positiveDefiniteKernelFinsuppSesqForm: the same form bundled as a sesquilinear form.
• TauCeti.positiveDefiniteKernelFinsuppForm_self_nonneg: nonnegativity on the diagonal for positive-definite kernels.
• TauCeti.positiveDefiniteKernelFinsuppForm_add_left and related lemmas: sesquilinearity of the form.
• TauCeti.positiveDefiniteKernelFinsuppForm_conj_symm: conjugate symmetry of the form.
• TauCeti.positiveDefiniteKernelFinsuppForm_single_single: the value on two basis vectors.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Chapter 3.

noncomputable def TauCeti.positiveDefiniteKernelFinsuppForm {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (K : α → α → 𝕜) (x y : α →₀ 𝕜) : 𝕜

The finitely supported Gram expression associated to a kernel K.

For positive-definite K, the diagonal value positiveDefiniteKernelFinsuppForm K x x is nonnegative, and the form is Hermitian. This is the pre-inner-product expression used before quotienting by its null space in the GNS/Kolmogorov construction.

Equations

• TauCeti.positiveDefiniteKernelFinsuppForm K x y = x.sum fun (a : α) (xa : 𝕜) => y.sum fun (b : α) (yb : 𝕜) => (starRingEnd 𝕜) xa * yb * K a b

theorem TauCeti.positiveDefiniteKernelFinsuppForm_def {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (K : α → α → 𝕜) (x y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm K x y = x.sum fun (a : α) (xa : 𝕜) => y.sum fun (b : α) (yb : 𝕜) => (starRingEnd 𝕜) xa * yb * K a b

The finitely supported Gram form unfolds to the double Finsupp.sum expression.

@[simp]

theorem TauCeti.positiveDefiniteKernelFinsuppForm_zero_left {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm K 0 y = 0

The finitely supported Gram form is zero when the left vector is zero.

@[simp]

theorem TauCeti.positiveDefiniteKernelFinsuppForm_zero_right {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (x : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm K x 0 = 0

The finitely supported Gram form is zero when the right vector is zero.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_self_nonneg {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : IsPositiveDefiniteKernel K) (x : α →₀ 𝕜) : 0 ≤ positiveDefiniteKernelFinsuppForm K x x

The diagonal finitely supported Gram form of a positive-definite kernel is nonnegative.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_add_left {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (x y z : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm K (x + y) z = positiveDefiniteKernelFinsuppForm K x z + positiveDefiniteKernelFinsuppForm K y z

The finitely supported Gram form is additive in the left argument.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_add_right {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (x y z : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm K x (y + z) = positiveDefiniteKernelFinsuppForm K x y + positiveDefiniteKernelFinsuppForm K x z

The finitely supported Gram form is additive in the right argument.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_smul_left {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (c : 𝕜) (x y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm K (c • x) y = (starRingEnd 𝕜) c * positiveDefiniteKernelFinsuppForm K x y

The finitely supported Gram form is conjugate-linear in the left scalar.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_smul_right {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (c : 𝕜) (x y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm K x (c • y) = c * positiveDefiniteKernelFinsuppForm K x y

The finitely supported Gram form is linear in the right scalar.

@[simp]

theorem TauCeti.positiveDefiniteKernelFinsuppForm_zero_kernel {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (x y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm (fun (x x_1 : α) => 0) x y = 0

The finitely supported Gram form is zero for the zero kernel.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_add_kernel {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (K L : α → α → 𝕜) (x y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm (fun (a b : α) => K a b + L a b) x y = positiveDefiniteKernelFinsuppForm K x y + positiveDefiniteKernelFinsuppForm L x y

The finitely supported Gram form is additive in the kernel.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_smul_kernel {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (c : 𝕜) (K : α → α → 𝕜) (x y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm (fun (a b : α) => c • K a b) x y = c * positiveDefiniteKernelFinsuppForm K x y

The finitely supported Gram form is homogeneous in the kernel.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_real_smul_kernel {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (r : ℝ) (K : α → α → 𝕜) (x y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm (fun (a b : α) => r • K a b) x y = r • positiveDefiniteKernelFinsuppForm K x y

The finitely supported Gram form is homogeneous in a real scalar on the kernel.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_sum_kernel {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {ι : Type u_1} (s : Finset ι) (K : ι → α → α → 𝕜) (x y : α →₀ 𝕜) : positiveDefiniteKernelFinsuppForm (fun (a b : α) => ∑ i ∈ s, K i a b) x y = ∑ i ∈ s, positiveDefiniteKernelFinsuppForm (K i) x y

The finitely supported Gram form sends finite sums of kernels to sums of Gram forms.

noncomputable def TauCeti.positiveDefiniteKernelFinsuppSesqForm {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (K : α → α → 𝕜) : (α →₀ 𝕜) →ₗ⋆[𝕜] (α →₀ 𝕜) →ₗ[𝕜] 𝕜

The finitely supported Gram form bundled as a sesquilinear form.

Equations

• TauCeti.positiveDefiniteKernelFinsuppSesqForm K = LinearMap.mk₂'ₛₗ (starRingEnd 𝕜) (RingHom.id 𝕜) (TauCeti.positiveDefiniteKernelFinsuppForm K) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.positiveDefiniteKernelFinsuppSesqForm_apply {𝕜 : Type u} [RCLike 𝕜] {α : Type v} (K : α → α → 𝕜) (x y : α →₀ 𝕜) : ((positiveDefiniteKernelFinsuppSesqForm K) x) y = positiveDefiniteKernelFinsuppForm K x y

Applying the bundled sesquilinear form gives the finitely supported Gram expression.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_conj_symm_of_conj_symm {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hsymm : ∀ (a b : α), (starRingEnd 𝕜) (K a b) = K b a) (x y : α →₀ 𝕜) : (starRingEnd 𝕜) (positiveDefiniteKernelFinsuppForm K x y) = positiveDefiniteKernelFinsuppForm K y x

A pointwise conjugate-symmetric kernel gives a conjugate-symmetric finitely supported Gram form.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_conj_symm {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : IsPositiveDefiniteKernel K) (x y : α →₀ 𝕜) : (starRingEnd 𝕜) (positiveDefiniteKernelFinsuppForm K x y) = positiveDefiniteKernelFinsuppForm K y x

The finitely supported Gram form attached to a positive-definite kernel is conjugate symmetric.

theorem TauCeti.positiveDefiniteKernelFinsuppSesqForm_isPosSemidef {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : IsPositiveDefiniteKernel K) : (positiveDefiniteKernelFinsuppSesqForm K).IsPosSemidef

Positive-definite kernels give positive-semidefinite finitely supported sesquilinear forms.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_isPositiveDefiniteKernel {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (hK : IsPositiveDefiniteKernel K) : IsPositiveDefiniteKernel fun (x y : α →₀ 𝕜) => positiveDefiniteKernelFinsuppForm K x y

The finitely supported Gram form of a positive-definite kernel is itself a positive-definite kernel on the finitely supported coefficient space.

@[simp]

theorem TauCeti.positiveDefiniteKernelFinsuppForm_single_single {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (a b : α) (r s : 𝕜) : positiveDefiniteKernelFinsuppForm K (Finsupp.single a r) (Finsupp.single b s) = (starRingEnd 𝕜) r * s * K a b

The finitely supported Gram form takes the expected value on two basis vectors.

theorem TauCeti.positiveDefiniteKernelFinsuppForm_single_self {𝕜 : Type u} [RCLike 𝕜] {α : Type v} {K : α → α → 𝕜} (a : α) (r : 𝕜) : positiveDefiniteKernelFinsuppForm K (Finsupp.single a r) (Finsupp.single a r) = ↑(RCLike.normSq r) * K a a

On a single finitely supported basis vector, the diagonal Gram form is the scalar norm-square times the corresponding diagonal kernel value.