Motivation

The Fourier series of a periodic function decomposes it into sinusoidal components, but the partial sums of that series need not converge to the function even when the function is continuous: du Bois-Reymond exhibited in 1873 a continuous $2\pi$-periodic function whose Fourier partial sums diverge at a point. Fejér's 1904 theorem repairs this failure by replacing the partial sums with their Cesàro (arithmetic) averages: for every continuous periodic function, these averages converge to the function, uniformly, with no smoothness hypothesis beyond continuity. This was the first universally valid summation method for Fourier series, and its underlying technique — averaging against a kernel whose mass concentrates at the origin — became the template for what is now called a good kernel or approximate identity, the basic device used throughout harmonic analysis (heat-kernel smoothing, Poisson summation, Fourier-inversion arguments) [Stein & Shakarchi, 2003].

Timeline.

• 1873 — du Bois-Reymond constructs a continuous $2\pi$-periodic function whose Fourier series diverges at a point, showing continuity alone cannot guarantee convergence of the partial sums themselves.
• 1904 — Fejér proves that the Cesàro means of the Fourier series of any continuous periodic function converge to it uniformly (Fejér, 1904).
• The good-kernel method Fejér introduced was later systematized as the general framework for approximate identities in harmonic analysis (Stein & Shakarchi, 2003, Ch. 2, §5).

Setting

Let $f : \mathbb{R} \to \mathbb{C}$ be continuous and $2\pi$-periodic, i.e. $f(x + 2\pi) = f(x)$ for every $x \in \mathbb{R}$. Its $n$-th Fourier coefficient, for $n \in \mathbb{Z}$, is

$$\hat f(n) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta)\, e^{-in\theta}\, d\theta.$$

Its $N$-th partial sum is $S_N(f)(\theta) = \sum_{n=-N}^{N} \hat f(n)\, e^{in\theta}$, and its $N$-th Cesàro (Fejér) mean is the arithmetic average of the first $N+1$ partial sums,

$$\sigma_N(f)(\theta) = \frac{1}{N+1}\sum_{k=0}^{N} S_k(f)(\theta).$$

Formalization targets

Fejér's theorem

$$\sigma_N(f) \longrightarrow f \quad \text{uniformly on } \mathbb{R} \text{ as } N \to \infty.$$

This is the full 1904 statement: no restriction to pointwise convergence, and no extra regularity assumed on $f$ beyond continuity.

Significance

The result itself. Fejér's theorem gives the first universally valid summation method for the Fourier series of a continuous function, closing the gap left open by pointwise convergence tests that need extra regularity. It also yields, essentially for free, a proof of the Weierstrass approximation theorem on the circle — the trigonometric polynomials $\sigma_N(f)$ are dense in the continuous $2\pi$-periodic functions under the uniform norm — and it is the historical prototype of the good-kernel/approximate-identity method underlying Poisson summation, heat-kernel smoothing, and $L^1$ Fourier-inversion arguments.

Formalizing it. Mathlib currently has no infrastructure for this at all. Mathlib.Analysis.Fourier.AddCircle defines Fourier coefficients on the circle and proves $L^2$ convergence (Parseval's identity, via the orthonormal Fourier basis), but it has no notion of a partial sum, no Dirichlet or Fejér kernel, and no pointwise or uniform convergence result for Fourier series of any kind. This mission builds that classical convergence theory — the Fejér kernel, its closed form and positivity, the good-kernel estimates, and the uniform convergence theorem itself — from first principles.

Difficulty

The obvious first attempt is to bound $|\sigma_N(f)(\theta) - f(\theta)|$ termwise from the individual Fourier coefficients. This fails outright: a continuous function's Fourier coefficients need not be absolutely summable, which is exactly the mechanism behind du Bois-Reymond's divergence example. The real difficulty is representing $\sigma_N(f)$ as a convolution,

$$\sigma_N(f)(\theta) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta - \varphi)\, F_N(\varphi)\, d\varphi,$$

against the Fejér kernel $F_N$, and then proving $F_N$ is a good kernel: nonnegative, integrating to $1$ over one period, and — the genuinely quantitative step — with its mass outside any fixed neighborhood of $0$ vanishing as $N \to \infty$. That last estimate needs the closed form

$$F_N(\theta) = \frac{1}{N+1}\left(\frac{\sin((N+1)\theta/2)}{\sin(\theta/2)}\right)^2,$$

which carries a removable singularity at $\theta = 0$ that must be handled carefully, together with a genuine decay estimate — via a lower bound on $|\sin(\theta/2)|$ — valid uniformly outside any fixed $\delta$-neighborhood of the origin.

Formalization scope

$f$ is complex-valued, and only continuity together with exact $2\pi$-periodicity is assumed — no differentiability, no bounded variation, no realness. Uniform convergence is stated with Mathlib's TendstoUniformly. The period is fixed at $2\pi$, matching the classical circle-group convention, rather than a general $T > 0$; the $T$-periodic statement is a routine rescaling of this one and is not separately targeted here. One route to a trivializing formalization is worth ruling out explicitly: assuming any extra regularity on $f$ (differentiability, bounded variation, Lipschitz continuity) would let the uniform-convergence conclusion follow from the much easier Dirichlet-kernel estimates, and would no longer be Fejér's theorem — the entire content of the result is that continuity alone suffices.

The needed infrastructure is the four definitions above (Fourier coefficient, partial sum, Cesàro mean, Fejér kernel) and the milestone lemmas below, culminating in the goal. The Fejér kernel's closed form, positivity, and good-kernel estimates are reusable well beyond this mission: directly for a Lean proof of the Weierstrass approximation theorem on the circle, and for any future development that needs an explicit approximate identity on the circle group. Contributions are welcome at every milestone; the concentration estimate is the analytic heart of the mission and a natural place to start.

Selected references

• L. Fejér, "Untersuchungen über Fouriersche Reihen," Mathematische Annalen 58 (1904), 51–69.
• E. M. Stein and R. Shakarchi, Fourier Analysis: An Introduction, Princeton Lectures in Analysis I, Princeton University Press, 2003, Chapter 2, §5 ("Good Kernels") and Theorem 5.2.
• Wikipedia, "Fejér's theorem." https://en.wikipedia.org/wiki/Fej%C3%A9r%27s_theorem