Positive Definite Functions

This file contains the definition of positive definite functions and basic lemmas. Extracted from Minlos.lean to avoid circular imports with GaussianRBF.lean.

Key definitions:

• IsPositiveDefinite: A function φ : α → ℂ is positive definite if for any finite collection of points and complex coefficients, ∑ᵢⱼ cbarᵢ cⱼ φ(xᵢ - xⱼ) ≥ 0

Key lemmas:

• isPositiveDefinite_precomp_linear: Composition with linear map preserves PD

Positive Definiteness

Namespaced under GFF4D to avoid clash with IsPositiveDefinite from the bochner library (which requires both hermitian + nonneg).

def GFF4D.IsPositiveDefinite {α : Type u_1} [AddGroup α] (φ : α → ℂ) : Prop

A function φ : α → ℂ is positive definite if for any finite collection of points x₁, ..., xₘ and complex coefficients c₁, ..., cₘ, we have ∑ᵢⱼ cbarᵢ cⱼ φ(xᵢ - xⱼ) ≥ 0

This is the standard definition in harmonic analysis and probability theory.

Equations

• GFF4D.IsPositiveDefinite φ = ∀ (m : ℕ) (x : Fin m → α) (c : Fin m → ℂ), 0 ≤ (∑ i : Fin m, ∑ j : Fin m, (starRingEnd ℂ) (c i) * c j * φ (x i - x j)).re

theorem GFF4D.isPositiveDefinite_precomp_linear {E : Type u_1} {H : Type u_2} [AddCommGroup E] [AddCommGroup H] [Module ℝ E] [Module ℝ H] (ψ : H → ℂ) (hPD : IsPositiveDefinite ψ) (T : E →ₗ[ℝ] H) : IsPositiveDefinite fun (f : E) => ψ (T f)

Composition preserves positive definiteness: if ψ is positive definite on H and T : E →ₗ[ℝ] H is linear, then ψ ∘ T is positive definite on E.