Fejér kernel

Definition

Fejer_fejerKernel

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

fourier-seriesharmonic-analysis

The $N$ -th Fejér kernel, $F_N(\theta) = \sum_{n=-N}^{N} \left(1 - \frac{|n|}{N+1}\right)\cos(n\theta)$ .

Definition code

import Mathlib

namespace Fejer

/-- The `N`-th Fejér kernel, `F_N(θ) = ∑_{n=-N}^{N} (1 - |n|/(N+1)) cos(nθ)` — the real-valued
function whose convolution against `f` computes the `N`-th Cesàro mean of `f`'s Fourier series. -/
noncomputable def fejerKernel (N : ℕ) (θ : ℝ) : ℝ :=
  ∑ n ∈ Finset.Icc (-(N : ℤ)) (N : ℤ), (1 - (|n| : ℝ) / (N + 1)) * Real.cos (n * θ)

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.

Read-back

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

For every natural number $N$ and every real number $\theta$ , $\text{fejerKernel}(N,\theta)$ is defined as a finite sum over the integers $n$ ranging over the closed integer interval $[-N, N]$ (exactly $2N+1$ terms). For each such integer $n$ , the summand is

\left(1 - \frac{|n|}{N+1}\right)\cos(n\theta),

where $|n|$ is cast to a real number and $N+1$ (with $N$ cast to a real number) appears in the denominator. Thus

\text{fejerKernel}(N,\theta) = \sum_{n=-N}^{N}\left(1 - \frac{|n|}{N+1}\right)\cos(n\theta).

The weight $1 - \frac{|n|}{N+1}$ equals $1$ at $n=0$ , decreases linearly in $|n|$ , and reaches its smallest value $\frac{1}{N+1}$ at $n = \pm N$ ; since $|n| \le N < N+1$ throughout the summation range, this weight is always strictly positive. No case analysis or restriction is placed on $\theta$ ; the formula is evaluated literally at whatever real value $\theta$ is given, using $\cos(n\theta)$ for each integer $n$ in range.

In the case $N = 0$ : the summation range is the singleton $\{0\}$ , so the sum has exactly one term, with weight $1 - 0 = 1$ and $\cos(0\cdot\theta)=1$ . Hence $\text{fejerKernel}(0,\theta) = 1$ for every real $\theta$ , with no dependence on $\theta$ whatsoever.

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