Wiener's atom-detection formula

wiener_atom_detection

Submitter: Kim Morrison.

Notes: §66 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. Wiener's atom-detection formula states that for a probability measure μ on the circle ℝ/2πℤ, the Cesàro averages (1/N) ∑_{k=1}^N |μ̂_k|² of the squared Fourier coefficients converge to ∑_x μ({x})², the total squared mass of the atoms. Thus the asymptotic behavior of the Fourier coefficients detects exactly the pure-point part of the measure. Mathlib provides AddCircle, the Fourier characters fourier, and related Fourier theory for functions, but it does not currently package Fourier coefficients of measures or this Wiener atom-detection theorem.

Source: N. Wiener, The Fourier Integral and Certain of its Applications (1933). Listed as §66 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Expand |μ̂_k|² = μ̂_k · conj(μ̂_k) = ∫∫ e^{ik(x−y)} dμ(x) dμ(y) by Fubini. Averaging over k = 1, …, N gives (1/N) ∑_{k=1}^N |μ̂_k|² = ∫∫ D_N(x−y) dμ(x) dμ(y), where D_N(t) = (1/N) ∑_{k=1}^N e^{ikt} is a Cesàro/Fejér-type kernel with |D_N| ≤ 1 and D_N(t) → 1 if t = 0 and → 0 if t ≠ 0. By dominated convergence (against the finite product measure μ × μ) the double integral converges to (μ × μ){(x, y) : x = y} = ∑_x μ({x})², the mass the diagonal carries, which is exactly the sum of squared atomic masses. The right-hand side is summable because the atoms of a finite measure are at most countable with masses bounded by μ(𝕋) = 1.

theorem declaration uses `sorry`wiener_atom_detection (μ : Measure (AddCircle (2 * Real.pi))) [IsProbabilityMeasure μ] :
    Tendsto
      (fun N : ℕ =>
        (1 / (N : ℝ)) *
          ∑ k ∈ Finset.Icc (1 : ℤ) N, ‖fourierCoeffMeasure μ k‖ ^ 2)
      atTop
      (𝓝 (∑' x : AddCircle (2 * Real.pi), ((μ {x}).toReal) ^ 2)) := byμ:Measure (AddCircle (2 * π))inst✝:IsProbabilityMeasure μ⊢ Tendsto (fun N => 1 / ↑N * ∑ k ∈ Finset.Icc 1 ↑N, ‖fourierCoeffMeasure μ k‖ ^ 2) atTop
  (𝓝 (∑' (x : AddCircle (2 * π)), (μ {x}).toReal ^ 2))
  sorryAll goals completed! 🐙

Solved by

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 2, 2026

• @GanjinZero with Seed Prover (ByteDance) on Jun 2, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 3, 2026