Bochner's theorem, L¹ case: nonnegative Fourier transform integrating to 1, with inversion

Proved

Bochner.bochner_L1_case

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

fourier-analysisharmonic-analysispositive-definite-kernels

Bochner's theorem, $L^1$ case. The special case of Bochner's theorem (Bochner.bochner_theorem) where the positive-definite function $f$ is additionally Lebesgue-integrable, so that the representing measure is absolutely continuous with an explicit continuous density.

Let $f:\mathbb R\to\mathbb C$ be continuous, Lebesgue-integrable, positive-definite, and normalized ( $f(0)=1$ ). Let $\tau=\text{fourierTransform } f$ be its Fourier transform (a real-valued function, since $f$ is Hermitian-symmetric). The theorem asserts:

\tau \text{ is continuous}, \qquad \tau(\xi)\ge 0 \text{ for every } \xi, \qquad \int_{\mathbb R}\tau(\xi)\,d\xi = 1,

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

Together, these say $\tau$ is (the density of) a probability measure, and $f$ is recovered from it by Fourier inversion. This is provable directly via Mathlib's existing Fourier-transform and inversion machinery for integrable functions, independently of the harder general goal theorem.

Formalization Note $f$ is complex-valued, not restricted to real-valued kernels (the standard, fully general $L^1$ case).

Preamble

import Mathlib
import Definitions.Def_PositiveDefinite

Formal statement

import Mathlib
import Definitions.Def_PositiveDefinite

namespace Bochner

open MeasureTheory

/-- **Bochner's theorem, `L¹` case.** If `f : ℝ → ℂ` is continuous, Lebesgue-integrable,
positive-definite, and normalized (`f 0 = 1`), then its Fourier transform `fourierTransform f`
is everywhere nonnegative, integrates to `1`, and recovers `f` by Fourier inversion. Together
these say the Fourier transform of `f` is (the density of) a probability measure, and `f` is
recovered from it — the density special case of the general representation theorem
(`bochner_theorem`), where the representing measure is absolutely continuous. -/
theorem bochner_L1_case
    (f : ℝ → ℂ) (hf_cont : Continuous f) (hf_int : Integrable f (volume : Measure ℝ))
    (hf_pd : IsPositiveDefinite f) (hf0 : f 0 = 1) :
    Continuous (fourierTransform f) ∧
      (∀ ξ : ℝ, 0 ≤ fourierTransform f ξ) ∧
      (∫ ξ : ℝ, fourierTransform f ξ = 1) ∧
      (∀ x : ℝ, f x =
        ∫ ξ : ℝ, Complex.exp (2 * Real.pi * Complex.I * ξ * x) * (fourierTransform f ξ : ℂ)) := by
  sorry

end Bochner

Source

Salomon Bochner, Vorlesungen ueber Fouriersche Integrale, 1932; standard L1 corollary of Bochner's theorem via Fourier inversion, see e.g. Rudin, Fourier Analysis on Groups, Section 1.4

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