Positive Definite Functions

A function φ : α → ℂ on an additive group is positive definite if:

1. φ(-x) = conj(φ(x)) for all x (Hermitian symmetry), and
2. For any finite collection of points x₁, ..., xₘ and complex coefficients c₁, ..., cₘ, the quadratic form ∑ᵢⱼ cbarᵢ cⱼ φ(xᵢ - xⱼ) ≥ 0.

Condition (1) ensures that the matrix [φ(xᵢ-xⱼ)] is Hermitian, so the quadratic form in (2) is automatically real-valued. Together they say the matrix is Hermitian positive semidefinite.

This is the standard definition in harmonic analysis (Rudin, Fourier Analysis on Groups, §1.4). Note: some references define PD using only .re ≥ 0, but that weaker condition does not imply Hermitian symmetry.

Main definitions

• IsPositiveDefinite: positive definiteness for functions on additive groups

Main results

• IsPositiveDefinite.conj_symm: φ(-x) = conj(φ(x))
• IsPositiveDefinite.nonneg: the quadratic form is nonneg
• IsPositiveDefinite.eval_zero_nonneg: φ(0) ≥ 0
• IsPositiveDefinite.bounded_by_zero: ‖φ(x)‖ ≤ φ(0).re for all x
• IsPositiveDefinite.mul: pointwise product of PD functions is PD (Schur)
• isPositiveDefinite_precomp_linear: composition with linear maps preserves PD

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

A function φ : α → ℂ is positive definite if the matrix [φ(xᵢ-xⱼ)] is Hermitian positive semidefinite for every finite set of points.

This bundles two conditions:

• hermitian: φ(-x) = conj(φ(x)) (ensures the matrix is Hermitian)
• nonneg: Re(∑ᵢⱼ cbarᵢ cⱼ φ(xᵢ - xⱼ)) ≥ 0 (positive semidefiniteness)

The Hermitian condition ensures the quadratic form is real, so Re ≥ 0 is equivalent to the full condition ≥ 0.

• hermitian (x : α) : φ (-x) = (starRingEnd ℂ) (φ x)
• nonneg (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 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.

theorem IsPositiveDefinite.conj_symm {α : Type u_1} [AddGroup α] {φ : α → ℂ} (hpd : IsPositiveDefinite φ) (x : α) : φ (-x) = (starRingEnd ℂ) (φ x)

φ(-x) = conj(φ(x)).

theorem IsPositiveDefinite.eval_zero_nonneg {α : Type u_1} [AddGroup α] {φ : α → ℂ} (hpd : IsPositiveDefinite φ) : 0 ≤ (φ 0).re

φ(0) is real and nonneg. (Test with m = 1, c₁ = 1.)

theorem IsPositiveDefinite.eval_zero_real {α : Type u_1} [AddGroup α] {φ : α → ℂ} (hpd : IsPositiveDefinite φ) : (φ 0).im = 0

φ(0) is real (imaginary part is zero).

theorem IsPositiveDefinite.bounded_by_zero {α : Type u_1} [AddGroup α] {φ : α → ℂ} (hpd : IsPositiveDefinite φ) (x : α) : ‖φ x‖ ≤ (φ 0).re

‖φ(x)‖ ≤ φ(0).re for all x. (Cauchy-Schwarz on the 2×2 PD matrix.)

theorem IsPositiveDefinite.mul {α : Type u_1} [AddGroup α] {φ : α → ℂ} (hpd : IsPositiveDefinite φ) {ψ : α → ℂ} (hψ : IsPositiveDefinite ψ) : IsPositiveDefinite fun (x : α) => φ x * ψ x

Pointwise product of PD functions is PD (Schur product theorem for functions). This is the key fact used in Phase 2 (Gaussian regularization).

Proof idea: The Hadamard (entrywise) product of two PSD Hermitian matrices is PSD. For the Hermitian condition, use conj(φψ) = conj(φ)conj(ψ).