Bochner's theorem on discrete abelian groups

A function φ on a discrete abelian group G is positive definite, ∑ᵢ ∑ⱼ cᵢ conj(cⱼ) φ(gᵢ - gⱼ) ≥ 0 for every finite family, if and only if it is the Fourier–Stieltjes transform φ(g) = ∫ χ(g) dμ(χ) of a finite inner regular positive measure μ on the Pontryagin dual of G. Every function on a discrete group is continuous, so no continuity hypothesis appears.

The representing measure is the one of Bochner's theorem on locally compact abelian groups, TauCeti.IsPositiveDefiniteSub.exists_pontryaginMeasureTransform_eq_of_continuousAt, whose continuity hypothesis is automatic on a discrete group.

For G = ℤ this recovers Herglotz's theorem, proved separately by Fejér means in TauCeti.Analysis.Bochner.Herglotz.

Main declarations

• TauCeti.isPositiveDefiniteSub_iff_exists_pontryaginMeasureTransform_eq: Bochner's theorem for discrete abelian groups.

References

• W. Rudin, Fourier Analysis on Groups, Interscience (1962), §1.4.
• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC Press (2016), §3.3 and §4.2.

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

Bochner's theorem on a discrete abelian group. A function on a discrete abelian group is positive definite if and only if it is the Fourier–Stieltjes transform of a finite inner regular measure on the Pontryagin dual.