Bochner's theorem

A function F : V → ℂ on a finite-dimensional real inner-product space is continuous and positive definite if and only if it is the Fourier-convention transform v ↦ ∫ q, fourierAtom v q ∂μ of a unique finite Borel measure μ on V. This file assembles the final statement from the two analytic predecessors, names the representing measure TauCeti.bochnerMeasure, and records its transform, total mass, scaling, and normalization.

Positive definiteness is TauCeti.IsPositiveDefiniteSub, the classical subtraction-form predicate on an additive commutative group; the equivalent positive-semidefiniteness of the subtraction kernel (a, b) ↦ F (a - b) is available through TauCeti.isPositiveDefiniteSub_iff_posSemidef and is the hypothesis of the kernel-form statement TauCeti.bochner_posSemidef.

The L¹ case comes first: for a continuous integrable positive-definite F, the finite measure with density (𝓕⁻ F).re against Lebesgue measure recovers F as the Fourier-convention transform ∫ q, fourierAtom · q of the measure, by Fourier inversion; this is the representing measure of Bochner's theorem, given explicitly.

Existence is proved by Gaussian regularization and a compactness argument. If F 0 = 0 the kernel Cauchy–Schwarz inequality forces F = 0 and the zero measure represents. Otherwise, after normalizing to G 0 = 1, the regularizations G_n = G · exp (-‖·‖²/(n+1)) are integrable positive-definite functions, each represented by an explicit probability measure ν_n with density (𝓕⁻ G_n).re (integral_fourierAtom_withDensity_re_fourierInv). The characteristic functions of the ν_n converge pointwise to a rescaling of G, which is continuous at 0, so the family is tight by the Lévy continuity theorem; Prokhorov's theorem and the metrizability of the space of probability measures extract a weakly convergent subsequence, whose limit represents G by passing to the limit in the characteristic functions. Uniqueness is Measure.ext_of_forall_integral_fourierAtom_eq from Fourier/Convention.lean.

Adapted (Apache 2.0) from the Bochner–Minlos formalization by Michael R. Douglas (https://github.com/mrdouglasny/bochner, revision 08eb302), source file Bochner/Main.lean; the positive-definiteness hypotheses are restated through TauCeti.IsPositiveDefiniteSub and Matrix.PosSemidef, and the representation is stated in the fourierAtom convention rather than through MeasureTheory.charFun.

Main declarations

• TauCeti.integral_fourierAtom_withDensity_re_fourierInv: the measure volume.withDensity (ENNReal.ofReal (𝓕⁻ F ·).re) recovers F through the Fourier atom — the L¹ case of Bochner's theorem.
• TauCeti.exists_isFiniteMeasure_integral_fourierAtom_eq: existence of a finite representing measure for a continuous positive-definite function.
• TauCeti.bochner, with the Euclidean specialization TauCeti.bochner_euclideanSpace: Bochner's theorem, the equivalence between continuity together with positive definiteness and the unique Fourier representation.
• TauCeti.bochner_posSemidef: the same equivalence with positive definiteness written as positive semidefiniteness of the subtraction kernel.
• TauCeti.bochner_probabilityMeasure: the normalized form — a positive-definite function with F 0 = 1 is the transform of a unique probability measure.
• TauCeti.bochnerMeasure: the representing measure itself, with TauCeti.integral_fourierAtom_bochnerMeasure (its transform), TauCeti.eq_bochnerMeasure (uniqueness), TauCeti.bochnerMeasure_eq_zero_of_not (the fallback branch), TauCeti.bochnerMeasure_univ and TauCeti.bochnerMeasure_real_univ (total mass), TauCeti.bochnerMeasure_const_mul and TauCeti.bochnerMeasure_add (nonnegative real scaling and additivity), and TauCeti.isProbabilityMeasure_bochnerMeasure (normalization).

References

• S. Bochner, Vorlesungen über Fouriersche Integrale, Akademische Verlagsgesellschaft (1932).
• W. Rudin, Fourier Analysis on Groups (1962), Theorem 1.4.3.
• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part C (Bochner milestone).

The L¹ representing measure

theorem TauCeti.integral_fourierAtom_withDensity_re_fourierInv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hpd : Matrix.PosSemidef fun (a b : V) => F (a - b)) (hint : MeasureTheory.Integrable F MeasureTheory.volume) (hcont : Continuous F) (v : V) : (∫ (q : V), fourierAtom v q ∂MeasureTheory.volume.withDensity fun (ξ : V) => ENNReal.ofReal (FourierTransformInv.fourierInv F ξ).re) = F v

Bochner recovery for L¹ positive-definite functions. A continuous integrable function F with positive-definite subtraction kernel is the Fourier-convention transform v ↦ ∫ q, fourierAtom v q ∂μ of the finite measure μ with density (𝓕⁻ F).re against Lebesgue measure. The identity is Fourier inversion 𝓕 (𝓕⁻ F) = F, using that 𝓕⁻ F is real and nonnegative. Rudin, Fourier Analysis on Groups, §1.4; Folland, §4.2.

The normalized existence argument

Bochner's theorem

theorem TauCeti.exists_isFiniteMeasure_integral_fourierAtom_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) (hcont : Continuous F) (hpd : IsPositiveDefiniteSub F) : ∃ (μ : MeasureTheory.Measure V), MeasureTheory.IsFiniteMeasure μ ∧ ∀ (v : V), F v = ∫ (q : V), fourierAtom v q ∂μ

Existence half of Bochner's theorem. A continuous positive-definite function F on a finite-dimensional real inner-product space is the Fourier-convention transform v ↦ ∫ q, fourierAtom v q ∂μ of a finite Borel measure μ. Rudin, Fourier Analysis on Groups, Theorem 1.4.3.

theorem TauCeti.continuous_and_isPositiveDefiniteSub_of_integral_fourierAtom_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (μ : MeasureTheory.Measure V) [MeasureTheory.IsFiniteMeasure μ] (hrep : ∀ (v : V), F v = ∫ (q : V), fourierAtom v q ∂μ) : Continuous F ∧ IsPositiveDefiniteSub F

Converse half of Bochner's theorem. The Fourier-convention transform of a finite Borel measure is continuous and positive definite.

theorem TauCeti.bochner {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) : Continuous F ∧ IsPositiveDefiniteSub F ↔ ∃! μ : MeasureTheory.Measure V, MeasureTheory.IsFiniteMeasure μ ∧ ∀ (v : V), F v = ∫ (q : V), fourierAtom v q ∂μ

Bochner's theorem. A function F on a finite-dimensional real inner-product space is continuous and positive definite if and only if it is the Fourier-convention transform v ↦ ∫ q, fourierAtom v q ∂μ of a unique finite Borel measure μ. Bochner (1932); Rudin, Fourier Analysis on Groups, Theorem 1.4.3.

theorem TauCeti.bochner_posSemidef {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) : (Continuous F ∧ Matrix.PosSemidef fun (a b : V) => F (a - b)) ↔ ∃! μ : MeasureTheory.Measure V, MeasureTheory.IsFiniteMeasure μ ∧ ∀ (v : V), F v = ∫ (q : V), fourierAtom v q ∂μ

Bochner's theorem, kernel form. The subtraction kernel (a, b) ↦ F (a - b) of a continuous function is positive semidefinite if and only if F is the Fourier-convention transform of a unique finite Borel measure. This is TauCeti.bochner read through the PD-function ↔ PD-kernel correspondence TauCeti.isPositiveDefiniteSub_iff_posSemidef.

theorem TauCeti.bochner_euclideanSpace (d : ℕ) (F : EuclideanSpace ℝ (Fin d) → ℂ) : Continuous F ∧ IsPositiveDefiniteSub F ↔ ∃! μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d)), MeasureTheory.IsFiniteMeasure μ ∧ ∀ (v : EuclideanSpace ℝ (Fin d)), F v = ∫ (q : EuclideanSpace ℝ (Fin d)), fourierAtom v q ∂μ

Bochner's theorem on ℝᵈ: the specialization of bochner to Euclidean space. A function on EuclideanSpace ℝ (Fin d) is continuous and positive definite if and only if it is the Fourier transform of a unique finite positive measure.

theorem TauCeti.bochner_probabilityMeasure {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) : Continuous F ∧ IsPositiveDefiniteSub F ∧ F 0 = 1 ↔ ∃! μ : MeasureTheory.Measure V, MeasureTheory.IsProbabilityMeasure μ ∧ ∀ (v : V), F v = ∫ (q : V), fourierAtom v q ∂μ

Bochner's theorem for normalized functions. A function is continuous, positive definite and normalized by F 0 = 1 if and only if it is the Fourier-convention transform of a unique probability measure; this is the characteristic-function form of the theorem. Normalization is part of the equivalence: a probability representation forces F 0 = 1.

The representing measure

noncomputable def TauCeti.bochnerMeasure {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) : MeasureTheory.Measure V

The representing measure of Bochner's theorem: the unique finite Borel measure whose Fourier-convention transform is F, when F is continuous and positive definite, and the zero measure otherwise.

Equations

• TauCeti.bochnerMeasure F = if h : Continuous F ∧ TauCeti.IsPositiveDefiniteSub F then ⋯.choose else 0

theorem TauCeti.bochnerMeasure_eq_zero_of_not {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (h : ¬(Continuous F ∧ IsPositiveDefiniteSub F)) : bochnerMeasure F = 0

Outside the hypotheses of Bochner's theorem the Bochner measure is 0.

instance TauCeti.isFiniteMeasure_bochnerMeasure {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) : MeasureTheory.IsFiniteMeasure (bochnerMeasure F)

The Bochner measure of any function is finite: for a continuous positive-definite function this is the finiteness of its representing measure, and otherwise the measure is 0.

theorem TauCeti.integral_fourierAtom_bochnerMeasure {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (hcont : Continuous F) (hpd : IsPositiveDefiniteSub F) (v : V) : ∫ (q : V), fourierAtom v q ∂bochnerMeasure F = F v

The Bochner measure represents its function.

theorem TauCeti.eq_bochnerMeasure {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (μ : MeasureTheory.Measure V) [MeasureTheory.IsFiniteMeasure μ] (hrep : ∀ (v : V), F v = ∫ (q : V), fourierAtom v q ∂μ) : μ = bochnerMeasure F

Uniqueness of the Bochner measure. Any finite Borel measure whose Fourier-convention transform is F is the Bochner measure of F; no hypothesis on F is needed, since a function represented by a finite measure is automatically continuous and positive definite.

theorem TauCeti.bochnerMeasure_real_univ {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (hcont : Continuous F) (hpd : IsPositiveDefiniteSub F) : (bochnerMeasure F).real Set.univ = (F 0).re

The total mass of the Bochner measure is the value of the function at the origin.

theorem TauCeti.bochnerMeasure_univ {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (hcont : Continuous F) (hpd : IsPositiveDefiniteSub F) : (bochnerMeasure F) Set.univ = ENNReal.ofReal (F 0).re

The total mass of the Bochner measure, as an extended nonnegative real.

theorem TauCeti.isProbabilityMeasure_bochnerMeasure {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (hcont : Continuous F) (hpd : IsPositiveDefiniteSub F) (hF0 : F 0 = 1) : MeasureTheory.IsProbabilityMeasure (bochnerMeasure F)

The normalized case. The Bochner measure of a positive-definite function with F 0 = 1 is a probability measure.

@[simp]

theorem TauCeti.bochnerMeasure_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : (bochnerMeasure fun (x : V) => 0) = 0

The Bochner measure of the zero function is the zero measure.

theorem TauCeti.bochnerMeasure_const_mul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) {r : ℝ} (hr : 0 ≤ r) : (bochnerMeasure fun (v : V) => ↑r * F v) = ENNReal.ofReal r • bochnerMeasure F

Scaling a function by a nonnegative real scales its Bochner measure by the same factor. No hypothesis on F is needed: for a positive factor the two sides are simultaneously outside the hypotheses of Bochner's theorem, where both are 0.

theorem TauCeti.bochnerMeasure_add {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F H : V → ℂ} (hFcont : Continuous F) (hFpd : IsPositiveDefiniteSub F) (hHcont : Continuous H) (hHpd : IsPositiveDefiniteSub H) : (bochnerMeasure fun (v : V) => F v + H v) = bochnerMeasure F + bochnerMeasure H

The Bochner measure of a sum of continuous positive-definite functions is the sum of their Bochner measures.