Closed form of the Fejér kernel

Proved

Fejer.fejerKernel_closed_form

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

fourier-seriesharmonic-analysis

For $\theta \not\equiv 0 \pmod {2\pi}$ , $F_N(\theta) = \frac{1}{N+1}\left(\frac{\sin((N+1)\theta/2)}{\sin(\theta/2)}\right)^2$ .

Formal statement

import Mathlib
import Definitions.Def_Fejer_fejerKernel

namespace Fejer

/-- **Closed form of the Fejér kernel.** For every `N` and `θ` not an integer multiple of
`2π`, `F_N(θ) = (1/(N+1)) · (sin((N+1)θ/2) / sin(θ/2))²`. -/
theorem fejerKernel_closed_form
    (N : ℕ) (θ : ℝ) (hθ : ∀ k : ℤ, θ ≠ 2 * Real.pi * k) :
    fejerKernel N θ = (1 / (N + 1)) * (Real.sin ((N + 1) * θ / 2) / Real.sin (θ / 2)) ^ 2 := 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

This theorem concerns the function fejerKernel, defined for a natural number $N$ and real $\theta$ as $\sum_{n=-N}^{N} \left(1 - \frac{|n|}{N+1}\right)\cos(n\theta)$ , where the sum ranges over integers $n$ from $-N$ to $N$ inclusive. The hypothesis hθ states: for every integer $k$ , $\theta \neq 2\pi k$ ; that is, $\theta$ is not an integer multiple of $2\pi$ (this rules out $\theta = 0$ among others, since $k=0$ gives $\theta \neq 0$ ). Under this hypothesis, the theorem asserts the equality

\sum_{n=-N}^{N} \left(1 - \frac{|n|}{N+1}\right)\cos(n\theta) = \frac{1}{N+1}\left(\frac{\sin\!\left(\frac{(N+1)\theta}{2}\right)}{\sin\!\left(\frac{\theta}{2}\right)}\right)^2,

where all instances of $N$ and $N+1$ on the right-hand side are the real-number casts of the natural number $N$ (plus one). No claim is made about what happens when $\theta$ is an integer multiple of $2\pi$ (those cases are excluded from the statement's scope by the hypothesis, not addressed as a limiting case or otherwise).

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