Wiener's atom-detection formula

wiener_atom_detection — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Wiener's atom-detection formula** (§66). For a probability measure `μ` on
the circle `𝕋 = ℝ/2πℤ`, the Cesàro average of `|μ̂_k|²` for `k = 1, …, N`
converges to the sum of the squared masses of the atoms of `μ`. The right-hand
side is automatically summable: the atoms of a finite measure are at most
countable and their masses are bounded by `μ(𝕋) = 1`. -/
theorem 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
  sorry

Informal solution sketch

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.

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: wiener_atom_detection
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.