Example 16.2: on ℝ, ψ(x)ₙ = e^{−x²/2} xⁿ/√n! into ℓ² has ⟨ψ(x), ψ(x')⟩ = e^{−(x−x')²/2}; the Gaussian kernel e^{−‖x−x'‖²/(2σ)} on ℝⁿ is a kernel

Proved

UnderstandingML.gaussian_kernel

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

gaussian-kernelhilbert-spacekernel-methods

Example 16.2 (Gaussian Kernel). Let the original instance space be $\mathbb{R}$ and consider the mapping $\psi$ where for each $n \ge 0$ there is an element $\psi(x)_n = \frac{1}{\sqrt{n!}}e^{-x^2/2}x^n$ . Then $\langle\psi(x), \psi(x')\rangle = e^{-(x-x')^2/2}$ . More generally, given $\sigma > 0$ , the Gaussian kernel $K(x, x') = e^{-\|x - x'\|^2/(2\sigma)}$ implements an inner product in a (infinite-dimensional) feature space.

Formally: the map into $\ell^2$ with the stated inner products, and IsKernel for the Gaussian kernel on $\mathbb{R}^n$ for every $\sigma > 0$ .

Preamble

import Definitions.Def_UnderstandingML_Kernel

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **Example 16.2 (Gaussian Kernel)** (pp. 220–221). On `ℝ`, the mapping `ψ` with coordinates
`ψ(x)ₙ = (1/√n!) e^{−x²/2} xⁿ` into `ℓ²` satisfies `⟨ψ(x), ψ(x')⟩ = e^{−(x − x')²/2}`; more
generally, for every `σ > 0` the Gaussian kernel `K(x, x') = e^{−‖x − x'‖²/(2σ)}` on `ℝ^n`
implements an inner product in some Hilbert space. -/
theorem gaussian_kernel :
    (∃ ψ : ℝ → lp (fun _ : ℕ ↦ ℝ) 2,
      ∀ x x' : ℝ, ⟪ψ x, ψ x'⟫_ℝ = Real.exp (-((x - x') ^ 2) / 2)) ∧
    ∀ (n : ℕ) (σ : ℝ), 0 < σ → IsKernel (gaussianKernel (n := n) σ) := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §16.2 pp. 220-221, Example 16.2 with its derivation and the general Gaussian kernel

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph