Motivation

Positive-definite functions sit at a crossroads of harmonic analysis, probability, and machine learning. A function $f:\mathbb R\to\mathbb C$ is positive-definite if, for every finite family of points $x_1,\dots,x_n$ and complex coefficients $c_1,\dots,c_n$, the Hermitian quadratic form $\sum_{i,j}\overline{c_i}c_j f(x_i-x_j)$ is real and nonnegative. This single algebraic condition is exactly what makes $f$ realizable as: the covariance kernel of a stationary stochastic process; the characteristic function of a random variable (up to normalization); a valid Mercer/RBF kernel in machine learning; or a valid random-features/spectral density in random-feature kernel approximation methods.

Bochner's theorem (1932) is the structural reason all of these examples work: it says positive-definiteness is not merely a necessary condition for such a representation, but exactly characterizes it. A continuous, normalized ($f(0)=1$) function is positive-definite if and only if it is the Fourier–Stieltjes transform of some probability measure $\nu$ on $\mathbb R$ — i.e. $f$ is the characteristic function of a random variable. This mission asks for a machine-checked proof of that theorem, together with its most useful corollary: the case where $f$ is additionally Lebesgue-integrable, so that $\nu$ has an explicit continuous density given directly by the ordinary Fourier transform of $f$.

Setting

Fix IsPositiveDefinite f as above, for $f:\mathbb R\to\mathbb C$ (not restricted to real-valued kernels — the standard, fully general statement). A positive-definite function is automatically Hermitian-symmetric, $f(-x)=\overline{f(x)}$ (IsPositiveDefinite.conj_neg), which is exactly what makes a representation by a genuine (positive) probability measure possible, rather than a signed or complex one. The theorem works with f continuous and normalized. No further hypothesis (in particular, no integrability of f) is assumed for the general representation theorem: the representing measure $\nu$ need not be absolutely continuous (e.g. for a periodic $f$, $\nu$ is a discrete measure supported on the harmonics of the period — this is Herglotz's 1911 theorem, the periodic special case). Under the extra hypothesis that f is Lebesgue-integrable, the representing measure becomes absolutely continuous with a continuous density: this density is fourierTransform f, the (real part of the) Fourier transform of f — automatically real-valued, again by Hermitian symmetry — and Fourier inversion recovers f from it.

Formalization targets

Goal — Bochner's theorem, general case

$$f \text{ continuous, positive-definite, } f(0)=1 \;\Longrightarrow\; \exists\, \nu \text{ a probability measure on } \mathbb R,\; \forall x,\; f(x) = \int_{\mathbb R} e^{i2\pi\xi x}\,d\nu(\xi).$$

The central representation theorem: no integrability hypothesis on $f$, so $\nu$ may be any probability measure, not necessarily a density.

Milestone — Bochner's theorem, L¹ (density) case

$$f \text{ continuous, integrable, positive-definite, } f(0)=1 \;\Longrightarrow\; \tau:=\text{fourierTransform } f \text{ is continuous}, \;\tau \ge 0,\; \int \tau = 1, \text{ and } f(x) = \int e^{i2\pi\xi x}\tau(\xi)\,d\xi.$$

The special case where the representing measure of the goal theorem is absolutely continuous with an explicit density — the form most directly usable in applications. Provable independently of the general goal theorem via classical Fourier-inversion machinery, so it is a natural, self-contained first target.

Significance

Bochner's theorem is one of the load-bearing structural results of 20th-century harmonic analysis: it underlies Bochner–Minlos-type theorems for random fields, the entire theory of stationary Gaussian processes, kernel methods in statistics and machine learning, and (via its periodic specialization, Herglotz's theorem) the spectral theory of stationary time series. Formalizing it gives the platform a reusable, general-purpose characterization of positive-definite functions that any future mission on kernel methods, random features, or characteristic functions can build on directly.

Difficulty

The general representation theorem is the harder target: the standard proof (see the Wikipedia article linked below) constructs, from f, a strongly continuous unitary representation of $\mathbb R$ on a Hilbert space via a GNS-type construction, then invokes Stone's theorem and the spectral theorem to extract the representing measure — a substantial functional-analytic argument, since f need not be integrable and $\nu$ need not have a density. The L¹ milestone is comparatively more tractable: it can be attacked directly via Mathlib's existing Fourier-transform and Fourier-inversion machinery for integrable functions, plus the elementary fact (already available for reuse: IsPositiveDefinite.conj_neg) that a positive-definite function is Hermitian-symmetric.

Formalization scope

IsPositiveDefinite is formalized exactly as the finite Hermitian-form condition above, over Fin n → ℝ point families and Fin n → ℂ coefficients, matching the standard convention in the literature, with f : ℝ → ℂ — the fully general, complex-valued statement, not restricted to real-valued kernels. fourierTransform f ξ is defined as the real part of ∫ Complex.exp(-i2πξ x) * f(x) dx; this is provably the exact (not merely real-part-of) Fourier transform once f is positive-definite, since Hermitian symmetry forces the integral to be real already.

Selected references

• Bochner's theorem, Wikipedia — states the general locally-compact-abelian-group form and sketches the unitary-representation proof; a good map of the territory before diving into either target.
• Salomon Bochner, Vorlesungen über Fouriersche Integrale, Akademische Verlagsgesellschaft, 1932.
• Gustav Herglotz, Über Potenzreihen mit positivem, reellem Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.
• Walter Rudin, Fourier Analysis on Groups, Interscience, 1962, Chapter 1.