Gaussian RBF Kernel is Positive Definite

Proves that the Gaussian radial basis function kernel h ↦ exp(-‖h‖² / 2) is a positive definite function on any real inner product space. The proof uses three steps: (1) the inner product kernel ⟨x, y⟩ is positive definite; (2) exponentiation preserves positive definiteness via the Hadamard series in HadamardExp.lean; (3) the Gaussian kernel factors as exp(-‖x - y‖² / 2) = exp(-‖x‖² / 2) · exp(-‖y‖² / 2) · exp(⟨x, y⟩), reducing from the RBF to the inner product kernel.

def IsPositiveDefiniteKernel {α : Type u_2} (K : α → α → ℂ) : Prop

Definition of a positive definite kernel K : α × α → ℂ.

Equations

• IsPositiveDefiniteKernel K = ∀ (m : ℕ) (x : Fin m → α) (c : Fin m → ℂ), 0 ≤ (∑ i : Fin m, ∑ j : Fin m, star (c i) * c j * K (x i) (x j)).re

theorem innerProduct_is_pd_kernel {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : IsPositiveDefiniteKernel fun (x y : H) => ↑(inner ℝ x y)

Step 2: The inner product kernel is positive definite.

theorem real_valued_PD_kernel_gives_PSD_matrix {α : Type u_2} (K : α → α → ℂ) (h_real : ∀ (x y : α), (K x y).im = 0) (h_symm : ∀ (x y : α), K x y = K y x) (hK : IsPositiveDefiniteKernel K) (m : ℕ) (x : Fin m → α) : (Matrix.of fun (i j : Fin m) => (K (x i) (x j)).re).PosSemidef

Helper: For a real-valued PD kernel, the kernel matrix is PSD. Forward direction of the bridge between complex kernels and real matrices.

theorem exp_is_pd_kernel {α : Type u_2} (K : α → α → ℂ) (hK : IsPositiveDefiniteKernel K) (h_real : ∀ (x y : α), (K x y).im = 0) (h_symm : ∀ (x y : α), K x y = K y x) : IsPositiveDefiniteKernel fun (x y : α) => Complex.exp (K x y)

Step 3b: Exponential of a symmetric real-valued PD kernel is PD. Uses the Hadamard series machinery from HadamardExp.lean (same as OS3 proof).

theorem gaussian_rbf_pd_innerProduct_proof {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : GFF4D.IsPositiveDefinite fun (h : H) => Complex.exp (-(1 / 2) * ↑(‖h‖ ^ 2))

The Gaussian RBF kernel is positive definite on any inner product space.