Bochner's theorem on locally compact abelian groups

A positive-definite function φ on a locally compact abelian group G that is continuous at 0 is the Fourier–Stieltjes transform φ(g) = ∫ χ(g) dμ(χ) of a finite inner regular positive measure μ on the Pontryagin dual of G.

The representing measure is unique among finite inner regular measures, and conversely the transform of every such measure is continuous and positive definite. Thus this is a full Bochner characterization without any countability assumption. When the dual is Polish, every finite Borel measure is regular, giving the corresponding characterization by arbitrary finite measures. The dual is Polish when G is second countable.

The measure comes from the GNS construction. The function φ is a matrix coefficient φ(g) = ⟪v, U(-g) v⟫ of the unitary translation representation U on its GNS Hilbert space, which is strongly continuous because φ is continuous at 0. The cyclic spectral theorem for strongly continuous unitary representations, ContRepresentation.exists_pontryaginMeasureTransform_eq_inner, writes such a matrix coefficient as a Fourier–Stieltjes transform.

The existence theorem assumes no second countability of G, and the GNS space need not be separable: the integrated form behind the spectral theorem is defined through the inner regularity of the Haar measure.

Main declarations

• TauCeti.IsPositiveDefiniteSub.exists_pontryaginMeasureTransform_eq_of_continuousAt: a positive-definite function, continuous at 0, on a locally compact abelian group is the Fourier–Stieltjes transform of a finite inner regular measure on the dual group.
• The countability-free Bochner characterization: continuous positive-definite functions are precisely the transforms of unique finite inner regular measures.
• TauCeti.continuous_and_isPositiveDefiniteSub_iff_existsUnique_pontryaginMeasureTransform_eq: the full Bochner characterization by unique finite measures on a locally compact abelian group with Polish dual.

References

• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC Press (2016), Theorem 4.18.

theorem TauCeti.IsPositiveDefiniteSub.exists_pontryaginMeasureTransform_eq_of_continuousAt {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [BorelSpace (PontryaginDual (Multiplicative G))] {φ : G → ℂ} (hφ : IsPositiveDefiniteSub φ) (hφ₀ : ContinuousAt φ 0) : ∃ (μ : MeasureTheory.FiniteMeasure (PontryaginDual (Multiplicative G))), (↑μ).InnerRegular ∧ μ.pontryaginMeasureTransform = φ

Bochner's theorem on a locally compact abelian group, existence half. A positive-definite function that is continuous at 0 is the Fourier–Stieltjes transform of a finite inner regular measure on the Pontryagin dual.

theorem TauCeti.IsPositiveDefiniteSub.existsUnique_innerRegular_pontryaginMeasureTransform_eq_of_continuousAt {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [BorelSpace (PontryaginDual (Multiplicative G))] {φ : G → ℂ} (hφ : IsPositiveDefiniteSub φ) (hφ₀ : ContinuousAt φ 0) : ∃! μ : MeasureTheory.FiniteMeasure (PontryaginDual (Multiplicative G)), (↑μ).InnerRegular ∧ μ.pontryaginMeasureTransform = φ

Unique inner regular form of Bochner's theorem. A positive-definite function continuous at 0 has a unique finite inner regular representing measure on the Pontryagin dual. No countability or metrizability assumption is needed.

theorem TauCeti.continuous_and_isPositiveDefiniteSub_iff_existsUnique_innerRegular_pontryaginMeasureTransform_eq {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [BorelSpace (PontryaginDual (Multiplicative G))] (φ : G → ℂ) : Continuous φ ∧ IsPositiveDefiniteSub φ ↔ ∃! μ : MeasureTheory.FiniteMeasure (PontryaginDual (Multiplicative G)), (↑μ).InnerRegular ∧ μ.pontryaginMeasureTransform = φ

Bochner's characterization without countability assumptions. A function on a locally compact abelian group is continuous and positive definite if and only if it is the Fourier–Stieltjes transform of a unique finite inner regular measure on the Pontryagin dual.

theorem TauCeti.continuous_and_isPositiveDefiniteSub_iff_existsUnique_pontryaginMeasureTransform_eq {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))] [BorelSpace (PontryaginDual (Multiplicative G))] [PolishSpace (PontryaginDual (Multiplicative G))] (φ : G → ℂ) : Continuous φ ∧ IsPositiveDefiniteSub φ ↔ ∃! μ : MeasureTheory.FiniteMeasure (PontryaginDual (Multiplicative G)), μ.pontryaginMeasureTransform = φ

Bochner's characterization on a locally compact abelian group with Polish dual. A function is continuous and positive definite if and only if it is the Fourier–Stieltjes transform of a unique finite positive Borel measure on the dual group. The dual is Polish when the group is second countable.