Bochner's theorem: positive-definite functions as Fourier transforms of measures

Proved

Bochner.bochner_theorem

by Elsie66 · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisharmonic-analysispositive-definite-kernelsprobability

Bochner's theorem (Bochner–Herglotz representation theorem).

Let $f:\mathbb R\to\mathbb C$ be continuous, positive-definite (IsPositiveDefinite), and normalized ( $f(0)=1$ ). The theorem asserts that $f$ is the Fourier–Stieltjes transform of a probability measure $\nu$ on $\mathbb R$ : there exists a probability measure $\nu$ such that

f(x) = \int_{\mathbb R} e^{i2\pi\xi x}\,d\nu(\xi) \quad \text{for every } x\in\mathbb R.

No integrability hypothesis on $f$ is assumed: this is the fully general representation theorem, of which the $L^1$ case (Bochner.bochner_L1_case, where $f$ is additionally Lebesgue-integrable and $\nu$ has a continuous density) is a corollary.

Formalization Note $f$ is complex-valued (not restricted to real-valued kernels): this is the standard, fully general statement of Bochner's theorem. A positive-definite $f$ is automatically Hermitian-symmetric ( $f(-x)=\overline{f(x)}$ , IsPositiveDefinite.conj_neg), which is what makes the representation with a genuine probability measure (rather than a signed or complex one) possible.

Preamble

import Mathlib
import Definitions.Def_PositiveDefinite

Formal statement

import Mathlib
import Definitions.Def_PositiveDefinite

namespace Bochner

open MeasureTheory

/-- **Bochner's theorem** (Bochner–Herglotz representation theorem). If `f : ℝ → ℂ` is
continuous, positive-definite, and normalized (`f 0 = 1`), then `f` is the Fourier–Stieltjes
transform of a probability measure `ν` on `ℝ`: there exists a probability measure `ν` such that
`f x = ∫ e^{i2πξx} dν(ξ)` for every `x`. No integrability hypothesis on `f` itself is needed
here — this is the general representation theorem, of which the `L¹` case (where `f` is
additionally Lebesgue-integrable, so that `ν` has a continuous density given directly by the
Fourier transform of `f`) is a corollary. -/
theorem bochner_theorem
    (f : ℝ → ℂ) (hf_cont : Continuous f) (hf_pd : IsPositiveDefinite f) (hf0 : f 0 = 1) :
    ∃ ν : Measure ℝ, IsProbabilityMeasure ν ∧
      ∀ x : ℝ, f x = ∫ ξ, Complex.exp (2 * Real.pi * Complex.I * ξ * x) ∂ν := by
  sorry

end Bochner

Source

Salomon Bochner, Vorlesungen ueber Fouriersche Integrale, Akademische Verlagsgesellschaft, 1932

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by Elsie66 · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph