Fourier criteria for weak convergence on the circle

Probability measures on an additive circle converge weakly exactly when all their integer Fourier moments converge. In particular, convergence to Haar probability is equivalent to vanishing of every nonconstant Fourier moment. This detects the uniform limits of wrapped distributions without requiring a density representation. Applied to a constant sequence, the criterion shows that a circle probability measure is determined by its Fourier moments.

The proof uses Mathlib's span_fourier_closure_eq_top, the Stone–Weierstrass density of trigonometric polynomials. Integration against a probability measure is uniformly Lipschitz in the supremum norm, so convergence extends from this span to every continuous function.

theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_fourier_tendsto {T : ℝ} [Fact (0 < T)] {ι : Type u_1} {L : Filter ι} {μs : ι → ProbabilityMeasure (AddCircle T)} {μ : ProbabilityMeasure (AddCircle T)} : Filter.Tendsto μs L (nhds μ) ↔ ∀ (n : ℤ), Filter.Tendsto (fun (i : ι) => ∫ (x : AddCircle T), (fourier n) x ∂↑(μs i)) L (nhds (∫ (x : AddCircle T), (fourier n) x ∂↑μ))

Weak convergence of circle probability measures is equivalent to convergence of all integer Fourier moments.

theorem MeasureTheory.ProbabilityMeasure.tendsto_haarAddCircle_iff {T : ℝ} [Fact (0 < T)] {ι : Type u_1} {L : Filter ι} {μs : ι → ProbabilityMeasure (AddCircle T)} : Filter.Tendsto μs L (nhds AddCircle.haarAddCircle.toProbabilityMeasure) ↔ ∀ (n : ℤ), n ≠ 0 → Filter.Tendsto (fun (i : ι) => ∫ (x : AddCircle T), (fourier n) x ∂↑(μs i)) L (nhds 0)

Circle probability measures tend weakly to Haar probability exactly when every nonzero integer Fourier moment tends to zero.

theorem MeasureTheory.ProbabilityMeasure.ext_of_forall_integral_fourier_eq {T : ℝ} [Fact (0 < T)] {μ ν : ProbabilityMeasure (AddCircle T)} (h : ∀ (n : ℤ), ∫ (x : AddCircle T), (fourier n) x ∂↑μ = ∫ (x : AddCircle T), (fourier n) x ∂↑ν) : μ = ν

A probability measure on an additive circle is determined by its integer Fourier moments.