Herglotz's theorem: Bochner's theorem on the integers

A function φ : ℤ → ℂ is positive definite, ∑ᵢ ∑ⱼ cᵢ conj(cⱼ) φ(nᵢ - nⱼ) ≥ 0 for every finite family, if and only if it is the sequence of moments φ n = ∫ zⁿ dμ(z) of a finite positive measure μ on the unit circle. This is Herglotz's theorem. The unit circle is the Pontryagin dual of ℤ, the point z corresponding to the character n ↦ zⁿ, so the theorem is Bochner's theorem for the discrete group ℤ: the positive-definite functions on ℤ are exactly the Fourier–Stieltjes transforms MeasureTheory.FiniteMeasure.pontryaginMeasureTransform of finite measures on its dual, identified with the circle by TauCeti.circleEquivPontryaginDualInt. In that Pontryagin form it is the case G = ℤ of TauCeti.isPositiveDefiniteSub_iff_exists_pontryaginMeasureTransform_eq in TauCeti.Analysis.Bochner.DiscreteGroup. Every function on the discrete group ℤ is continuous, so no continuity hypothesis appears.

The measure is obtained from Fejér means. For N ≥ 1 the trigonometric polynomial

F_N(z) = N⁻¹ ∑_{a, b < N} φ(a - b) conj(z)ᵃ zᵇ

is N⁻¹ times the positive-definiteness form of φ at the points 0, …, N - 1 with weights conj(z)ᵃ, hence nonnegative. The measure ν_N with density F_N against normalized arc length has total mass φ 0, and by the orthogonality of the characters z ↦ zⁿ its moments are ∫ zⁿ dν_N = (1 - |n| / N)₊ φ n, the number of pairs (a, b) with a - b = n divided by N. A weak cluster point of the ν_N, which exists by Prokhorov's theorem on the compact circle, has moments φ n.

Main declarations

• TauCeti.exists_isFiniteMeasure_integral_zpow_eq: Herglotz's theorem, a positive-definite function on ℤ is the moment sequence of a finite measure on the circle.
• TauCeti.isPositiveDefiniteSub_iff_exists_isFiniteMeasure_integral_zpow_eq: the resulting characterization of positive-definite functions on ℤ.
• MeasureTheory.FiniteMeasure.pontryaginMeasureTransform_map_circleEquivPontryaginDualInt: the Fourier–Stieltjes transform of a measure carried from the circle to the dual of ℤ is its moment sequence.

References

• G. Herglotz, Über Potenzreihen mit positivem, reellem Teil im Einheitskreis, Ber. Verh. Sächs. Akad. Wiss. Leipzig 63 (1911), 501–511.
• Y. Katznelson, An Introduction to Harmonic Analysis, 3rd ed., Cambridge University Press (2004), Chapter I, §7 (positive-definite sequences and Herglotz's theorem via Fejér means).
• W. Rudin, Fourier Analysis on Groups, Interscience (1962), §1.4 (Bochner's theorem on a locally compact abelian group).

Fejér means of a positive-definite function

Herglotz's theorem

theorem TauCeti.exists_isFiniteMeasure_integral_zpow_eq (φ : ℤ → ℂ) (hφ : IsPositiveDefiniteSub φ) : ∃ (μ : MeasureTheory.Measure Circle), MeasureTheory.IsFiniteMeasure μ ∧ ∀ (n : ℤ), φ n = ∫ (z : Circle), ↑z ^ n ∂μ

Herglotz's theorem. A positive-definite function φ on ℤ is the moment sequence φ n = ∫ zⁿ dμ(z) of a finite positive measure μ on the unit circle.

@[simp]

theorem MeasureTheory.FiniteMeasure.pontryaginMeasureTransform_map_circleEquivPontryaginDualInt [MeasurableSpace (PontryaginDual (Multiplicative ℤ))] [BorelSpace (PontryaginDual (Multiplicative ℤ))] (μ : FiniteMeasure Circle) (n : ℤ) : (μ.map ⇑TauCeti.circleEquivPontryaginDualInt).pontryaginMeasureTransform n = ∫ (z : Circle), ↑z ^ n ∂↑μ

The Fourier–Stieltjes transform of the image of a finite measure on the circle under TauCeti.circleEquivPontryaginDualInt is its moment sequence.

theorem TauCeti.isPositiveDefiniteSub_iff_exists_isFiniteMeasure_integral_zpow_eq (φ : ℤ → ℂ) : IsPositiveDefiniteSub φ ↔ ∃ (μ : MeasureTheory.Measure Circle), MeasureTheory.IsFiniteMeasure μ ∧ ∀ (n : ℤ), φ n = ∫ (z : Circle), ↑z ^ n ∂μ

Herglotz's theorem, as a characterization: a function φ on ℤ is positive definite if and only if it is the moment sequence φ n = ∫ zⁿ dμ(z) of a finite positive measure on the unit circle.