Cesàro mean as convolution with the Fejér kernel

The statement is universally quantified over: a function $f:\mathbb{R}\to\mathbb{C}$; a hypothesis hf_cont that $f$ is continuous everywhere; a hypothesis hf_per that $f$ is periodic with period $2\pi$, spelled out as $\forall x\in\mathbb{R},\ f(x+2\pi)=f(x)$; a natural number $N:\mathbb{N}$ (including $N=0$); and a real number $\theta:\mathbb{R}$ (unrestricted). Under exactly these hypotheses, the theorem asserts a single equality of complex numbers.

Unfolding definitions: fourierCoeff f n is $\widehat f(n) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\psi)\,\exp(-i n \psi)\,d\psi$ (Lean's total interval integral, junk value $0$ if not integrable). partialSum f k θ is $S_k(f,\theta) = \sum_{n=-k}^{k} \widehat f(n)\,\exp(i n \theta)$ over the $2k+1$ integers $n\in[-k,k]$. cesaroMean f N θ is $\sigma_N(f,\theta) = \frac{1}{N+1}\sum_{k=0}^{N} S_k(f,\theta)$, a sum over $k\in\{0,\dots,N\}$ (well-defined division since $N+1\ge 1$). At $N=0$ this reduces to $\sigma_0(f,\theta)=\widehat f(0)$.

Separately, fejerKernel N φ is the real number $K_N(\varphi) = \sum_{n=-N}^{N} \left(1 - \frac{|n|}{N+1}\right)\cos(n\varphi)$; at $N=0$, $K_0(\varphi)=1$ for every $\varphi$.

The conclusion is the equation

where $K_N(\varphi)$ (real) is coerced into $\mathbb{C}$ before being multiplied by $f(\theta-\varphi)$. No claim is made about any limit as $N\to\infty$, about uniform or pointwise convergence, about positivity or normalization of $K_N$, or about any property of $f$ beyond continuity and exact $2\pi$-periodicity as stated.