Fejér's theorem

The theorem takes $f : \mathbb{R} \to \mathbb{C}$, a hypothesis hf_cont that $f$ is continuous everywhere, and a hypothesis hf_per that $f$ is periodic with period $2\pi$: $\forall x \in \mathbb{R},\ f(x + 2\pi) = f(x)$.

Unfolding: fourierCoeff f n is $\hat f(n) = \frac{1}{2\pi} \int_{-\pi}^{\pi} f(\theta)\, e^{-in\theta}\, d\theta$ (Lean's total interval integral). partialSum f N θ is $S_N(f)(\theta) = \sum_{n=-N}^{N} \hat f(n)\, e^{in\theta}$ over the $2N+1$ integers $n\in[-N,N]$. cesaroMean f N θ is $\sigma_N(f)(\theta) = \frac{1}{N+1} \sum_{k=0}^{N} S_k(f)(\theta)$, i.e. the average of the first $N+1$ partial sums — a fully explicit nested finite sum of complex numbers once $N,\theta$ are fixed.

The conclusion is that the family $N \mapsto (\theta \mapsto \sigma_N(f)(\theta))$ converges to $f$ uniformly with respect to Filter.atTop on $\mathbb{N}$, in the sense of Mathlib's TendstoUniformly: for every $\varepsilon > 0$ there is a threshold $N_0$ such that for all $N \ge N_0$ and simultaneously for every $\theta \in \mathbb{R}$ (unrestricted — not confined to $[-\pi,\pi]$ or any fundamental domain), $\|\sigma_N(f)(\theta) - f(\theta)\| < \varepsilon$. The single threshold $N_0$ works for all $\theta$ at once — the convergence rate is independent of $\theta$. No hypothesis beyond continuity and the stated $2\pi$-periodicity is imposed (no boundedness, integrability, or differentiability assumption appears separately), and no claim is made about convergence of $S_N(f)$ itself, only of the Cesàro averages $\sigma_N(f)$.