Fourier coefficients of measures on the circle

DefinitionFourier coefficients of a measure on the circle#✓fully proved

For a measure \(\mu\) on the circle \(\mathbb{T} = \mathbb{R}/2\pi\mathbb{Z}\) and an integer \(k\), the \(k\)-th Fourier coefficient of \(\mu\) is \(\hat\mu_k = \int_{\mathbb{T}} e^{ikx} \, d\mu(x)\).

noncomputable def fourierCoeffMeasure (μ : Measure (AddCircle (2 * Real.pi)))
    (k : ℤ) : ℂ :=
  ∫ x, fourier k x ∂μ

Used by 1

Used byWiener's atom-detection formula

TheoremWiener's atom-detection formula#●ready to prove

Let \(\mu\) be a probability measure on the circle \(\mathbb{T} = \mathbb{R}/2\pi\mathbb{Z}\), with Fourier coefficients \(\hat\mu_k = \int_{\mathbb{T}} e^{ikx} \, d\mu(x)\). Then \(\frac{1}{N} \sum_{k=1}^{N} \lvert \hat\mu_k \rvert^2 \to \sum_{x \in \mathbb{T}} \mu(\{x\})^2\) as \(N \to \infty\).

public theorem_wanted 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))

Sources

• 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). Problem wiener_atom_detection of the lean-eval benchmark.

Uses 1

Statement usesFourier coefficients of a measure on the circle

TheoremFourier decay of a circle measure passes to integrable densities#●ready to prove

Let \(\mu\) be a finite Borel measure on \(\mathbb{C}\) concentrated on the unit circle \(T = \{z \in \mathbb{C} : |z| = 1\}\), that is, \(\mu\)-almost every \(z\) lies in \(T\), and suppose that \(\int z^n \, d\mu(z) \to 0\) as \(n \to \infty\) through \(\mathbb{N}\). Then for every \(\mu\)-integrable function \(f : \mathbb{C} \to \mathbb{C}\),

\[ \lim_{n \to \infty} \int z^n f(z) \, d\mu(z) = 0. \]

public theorem_wanted tendsto_integral_pow_mul_of_tendsto_integral_pow
    (μ : MeasureTheory.Measure ℂ)
    (hfinite : μ Set.univ < ⊤)
    (hsphere : ∀ᵐ z ∂μ, z ∈ Metric.sphere (0 : ℂ) 1)
    (hpow : Filter.Tendsto (fun n : ℕ => ∫ z, z ^ n ∂μ) Filter.atTop (nhds 0))
    (f : ℂ → ℂ)
    (hf : MeasureTheory.Integrable f μ) :
    Filter.Tendsto (fun n : ℕ => ∫ z, z ^ n * f z ∂μ) Filter.atTop (nhds 0)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Set functions and measures on spaces with additional structure), problem ma_proofbench_l2_13.

1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.