Prove2Me

Cesàro (Fejér) mean of a Fourier series

Definition
Fejer_cesaroMean

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

fourier-seriesharmonic-analysis

The NN-th Cesàro mean of the Fourier series of ff, σN(f)(θ)=1N+1∑k=0NSk(f)(θ)\sigma_N(f)(\theta) = \frac{1}{N+1}\sum_{k=0}^{N} S_k(f)(\theta).

Definition code
import Mathlib
import Definitions.Def_Fejer_partialSum

namespace Fejer

/-- The `N`-th Cesàro (Fejér) mean of the Fourier series of `f`,
`σ_N(f) = (1/(N+1)) ∑_{n=0}^{N} S_n(f)`. -/
noncomputable def cesaroMean (f : ℝ → ℂ) (N : ℕ) (θ : ℝ) : ℂ :=
  (1 / ((N : ℂ) + 1)) * ∑ n ∈ Finset.range (N + 1), partialSum f n θ

end Fejer
Source
L. Fejér, "Untersuchungen über Fouriersche Reihen," Math. Ann. 58 (1904); E. M. Stein & R. Shakarchi, Fourier Analysis: An Introduction, Ch. 2.
Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

cesaroMean f N θ (with partialSum and fourierCoeff fully unfolded)

For f:R→Cf:\mathbb{R}\to\mathbb{C}, N∈NN\in\mathbb{N}, θ∈R\theta\in\mathbb{R}:

cesaroMean(f,N,θ)  =  1N+1∑n=0NpartialSum(f,n,θ)  =  1N+1∑n=0N  (∑k=−nnfourierCoeff(f,k) exp⁡ ⁣(i k θ)).\text{cesaroMean}(f,N,\theta) \;=\; \frac{1}{N+1}\sum_{n=0}^{N} \text{partialSum}(f,n,\theta) \;=\; \frac{1}{N+1}\sum_{n=0}^{N}\;\left(\sum_{k=-n}^{n} \text{fourierCoeff}(f,k)\,\exp\!\big(i\,k\,\theta\big)\right).

The outer sum ranges over Finset.range (N+1), i.e. over the N+1N+1 integers n=0,1,…,Nn = 0, 1, \dots, N (this nn is an order index for partialSum, unrelated to the summation index reused inside fourierCoeff/partialSum). The whole sum is divided by N+1N+1 (computed as (N:C)+1(N:\mathbb C)+1), which is always ≥1\ge 1 and never zero for any NN, so there is no division-by-zero issue. Each fourierCoeff(f,k) occurring anywhere is defined by 12π∫−ππf(θ′)e−ikθ′dθ′\frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta')e^{-ik\theta'}d\theta' (Mathlib's total interval integral, junk value 00 if not integrable), and that junk value propagates additively into cesaroMean if it occurs. No hypothesis of continuity, integrability, or periodicity of ff is assumed anywhere.

Edge case N=0N=0: the outer sum has exactly one term, n=0n=0, with denominator 0+1=10+1=1; that term is partialSum(f,0,θ)=fourierCoeff(f,0)\text{partialSum}(f,0,\theta) = \text{fourierCoeff}(f,0). Hence cesaroMean(f,0,θ)=fourierCoeff(f,0)=12π∫−ππf(θ′) dθ′\text{cesaroMean}(f,0,\theta) = \text{fourierCoeff}(f,0) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta')\,d\theta', a value literally independent of θ\theta. No hypothesis anywhere requires N≥1N\ge 1; N=0N=0 is a fully legal, defined case that collapses the average to this single constant term.

Human review

  • Endorsed by Shuze Chen · Sep 7, 2026

  • Endorsed by Elsie66 · Sep 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph