Bochner's theorem in characteristic-function form

TauCeti.bochner represents a continuous positive-definite function on a finite-dimensional real inner-product space V in the Fourier convention v ↦ ∫ q, exp (-2πi⟪v, q⟫) ∂μ. Probability and much of classical harmonic analysis use the characteristic-function convention v ↦ ∫ q, exp (i⟪q, v⟫) ∂μ instead, which is Mathlib's MeasureTheory.charFun μ. This file restates Bochner's theorem in that convention: a function F : V → ℂ is continuous and positive definite if and only if it is the characteristic function of a unique finite Borel measure, and the normalization F 0 = 1 corresponds to that measure being a probability measure (the Bochner–Khinchin theorem). On V = ℝ this is the classical statement F x = ∫ ξ, exp (i x ξ) dμ(ξ).

The two conventions differ by the rescaling q ↦ (-2π) • q of the representing measure: the characteristic-function representing measure of F is the image of TauCeti.bochnerMeasure F under this rescaling (TauCeti.charFun_map_neg_two_pi_smul_bochnerMeasure).

Main declarations

• TauCeti.charFun_map_neg_two_pi_smul_bochnerMeasure: the rescaled Bochner measure has characteristic function F.
• TauCeti.bochner_charFun: Bochner's theorem, characteristic-function form.
• TauCeti.bochner_charFun_probabilityMeasure: the normalized form — continuous positive-definite functions with F 0 = 1 are exactly the characteristic functions of probability measures.
• TauCeti.bochner_charFun_real: the characteristic-function statement on the real line.

References

• S. Bochner, Vorlesungen über Fouriersche Integrale, Akademische Verlagsgesellschaft (1932).
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II (1971), Section XIX.2.
• W. Rudin, Fourier Analysis on Groups (1962), Theorem 1.4.3.

theorem TauCeti.charFun_map_neg_two_pi_smul_bochnerMeasure {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (hcont : Continuous F) (hpd : IsPositiveDefiniteSub F) : MeasureTheory.charFun (MeasureTheory.Measure.map (fun (x : V) => (-2 * Real.pi) • x) (bochnerMeasure F)) = F

The characteristic-function representing measure. The image of the Bochner measure of a continuous positive-definite function F under the rescaling q ↦ (-2π) • q has characteristic function F.

theorem TauCeti.bochner_charFun {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 μ ∧ MeasureTheory.charFun μ = F

Bochner's theorem, characteristic-function form. A function F on a finite-dimensional real inner-product space is continuous and positive definite if and only if it is the characteristic function v ↦ ∫ q, exp (i⟪q, v⟫) ∂μ of a unique finite Borel measure μ.

theorem TauCeti.bochner_charFun_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 μ ∧ MeasureTheory.charFun μ = F

The Bochner–Khinchin theorem. A function F on a finite-dimensional real inner-product space is continuous, positive definite and normalized by F 0 = 1 if and only if it is the characteristic function of a unique Borel probability measure.

theorem TauCeti.bochner_charFun_real (F : ℝ → ℂ) : Continuous F ∧ IsPositiveDefiniteSub F ↔ ∃! μ : MeasureTheory.Measure ℝ, MeasureTheory.IsFiniteMeasure μ ∧ ∀ (x : ℝ), F x = ∫ (ξ : ℝ), Complex.exp (↑x * ↑ξ * Complex.I) ∂μ

Bochner's theorem on the real line, in its classical form: a function F : ℝ → ℂ is continuous and positive definite if and only if F x = ∫ ξ, exp (i x ξ) dμ(ξ) for a unique finite Borel measure μ on ℝ.