The Fejér kernel has integral one

Proved

Fejer.fejerKernel_integral_eq_one

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

fourier-seriesharmonic-analysis

$\frac{1}{2\pi}\int_{-\pi}^{\pi} F_N(\theta)\,d\theta = 1$ for every $N$ .

Formal statement

import Mathlib
import Definitions.Def_Fejer_fejerKernel

namespace Fejer

open MeasureTheory

/-- **The Fejér kernel has integral `1` over one period.** -/
theorem fejerKernel_integral_eq_one (N : ℕ) :
    (1 / (2 * Real.pi)) * ∫ θ in (-Real.pi)..Real.pi, fejerKernel N θ = 1 := by
  sorry

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, §5.

Read-back

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

For every natural number $N$ (universally quantified as an argument to the theorem), the claim is that

\frac{1}{2\pi}\int_{-\pi}^{\pi} \operatorname{fejerKernel}(N,\theta)\,d\theta = 1,

where $\operatorname{fejerKernel}(N,\theta) = \sum_{n=-N}^{N} \left(1 - \frac{|n|}{N+1}\right)\cos(n\theta)$ , a sum over $2N+1$ integer terms. At $N=0$ : the sum has the single term $n=0$ , giving $\operatorname{fejerKernel}(0,\theta) = 1$ identically, so the claimed identity reduces to $\frac{1}{2\pi}\int_{-\pi}^{\pi} 1\,d\theta = 1$ . No other hypotheses are imposed on $N$ (in particular $N$ is not assumed positive), and the equality asserted is exact equality of real numbers, not a limit or an inequality.

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