Fejér's theorem, specialized at the origin

Proved

ClockRoPE.fejer_cesaro_mean_periodic_at_zero

by Elsie66 · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisharmonic-analysis

This is Fejér's 1904 theorem on the Cesàro summability of Fourier series, specialized to a single point, used by Corollary 3.3 (ClockRoPE.periodic_posdef_fourier_coeffs_pmf_v2) of Chen et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369) to show that the Fourier coefficients of a continuous periodic positive-definite kernel sum to $f(0)$ .

Let $f:\mathbb R\to\mathbb R$ be continuous and $T$ -periodic, with real Fourier cosine coefficients $\alpha_k = \frac1T\int_0^T f(x)\cos(2\pi kx/T)\,dx$ . Fejér's theorem states that the Cesàro (Fejér) means of the partial sums of the Fourier series of $f$ converge to $f$ uniformly; the theorem asserts the pointwise consequence at $x=0$ , where every harmonic $\cos(2\pi k\cdot 0/T)=1$ , so the $n$ -th partial sum there is exactly $S_n=\sum_{k=-n}^{n}\alpha_k$ :

\lim_{N\to\infty}\frac1{N+1}\sum_{n=0}^{N} S_n = f(0), \qquad S_n = \sum_{k=-n}^{n}\alpha_k.

Combined with the nonnegativity of $\{\alpha_k\}$ (established separately via ClockRoPE.posDef_continuous_extension), this pins down $\sum_k \alpha_k = f(0)$ by an elementary Tauberian argument for monotone sequences.

Formalization Note Only the consequence at $x=0$ is stated, rather than the full uniform-convergence statement of Fejér's theorem, since that is all Corollary 3.3 needs.

Preamble

import Mathlib

Formal statement

namespace ClockRoPE

/-- **Fejér's theorem, specialized at the origin.** For `f : ℝ → ℝ` continuous and `T`-periodic
with (real) Fourier cosine coefficients `α k = (1/T) ∫_0^T f(x) cos(2πkx/T) dx`, the Cesàro
(Fejér) means of the symmetric partial sums `S_n = ∑_{k=-n}^{n} α k` of its Fourier series,
evaluated at `x = 0`, converge to `f 0`. This is Fejér's 1904 theorem — uniform convergence of
the Cesàro means of the Fourier series of a continuous periodic function to the function itself
— specialized to the single point `x = 0`, where every harmonic `cos(2πk·0/T) = 1`, so that the
`n`-th partial sum there is exactly `S_n = ∑_{k=-n}^{n} α k`. -/
theorem fejer_cesaro_mean_periodic_at_zero
    (f : ℝ → ℝ) (T : ℝ) (hT : 0 < T) (hf_cont : Continuous f)
    (hf_periodic : ∀ x : ℝ, f (x + T) = f x)
    (α : ℤ → ℝ)
    (hα : ∀ k : ℤ, α k =
      (1 / T) * ∫ x in (0 : ℝ)..T, f x * Real.cos (2 * Real.pi * (k : ℝ) * x / T)) :
    Filter.Tendsto (fun N : ℕ => (1 / ((N : ℝ) + 1)) *
        ∑ n ∈ Finset.range (N + 1), ∑ k ∈ Finset.Icc (-(n : ℤ)) n, α k)
      Filter.atTop (nhds (f 0)) := by
  sorry

end ClockRoPE

Source

Lipót Fejér, Untersuchungen über Fouriersche Reihen, Mathematische Annalen 58 (1904), 51-69 (Cesàro summability of Fourier series of continuous periodic functions)

View graph