The Fejér kernel concentrates at the origin

Proved

Fejer.fejerKernel_tendsto_zero_away_from_origin

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

fourier-seriesharmonic-analysis

For every $\delta \in (0,\pi)$ , $\int_{\delta \le |\theta| \le \pi} F_N(\theta)\,d\theta \to 0$ as $N \to \infty$ .

Formal statement

import Mathlib
import Definitions.Def_Fejer_fejerKernel

namespace Fejer

open MeasureTheory

/-- **The Fejér kernel's mass away from the origin vanishes.** For every `δ ∈ (0, π)`,
`∫_{δ ≤ |θ| ≤ π} F_N(θ) dθ → 0` as `N → ∞`. -/
theorem fejerKernel_tendsto_zero_away_from_origin
    (δ : ℝ) (hδ0 : 0 < δ) (hδπ : δ < Real.pi) :
    Filter.Tendsto
      (fun N : ℕ => ∫ θ in (Set.Icc (-Real.pi) Real.pi) ∩ {θ : ℝ | δ ≤ |θ|}, fejerKernel N θ)
      Filter.atTop (nhds 0) := 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

The statement fixes a real number $\delta$ subject to exactly two hypotheses: $0 < \delta$ (strict) and $\delta < \pi$ (strict), i.e. $\delta$ ranges over the open interval $(0,\pi)$ , with both endpoints excluded. Under these hypotheses, the integration domain

\big([-\pi,\pi]\big)\cap\{\theta \in \mathbb{R} : \delta \le |\theta|\}

is, in plain terms, $[-\pi,-\delta]\cup[\delta,\pi]$ — the closed interval $[-\pi,\pi]$ with the open middle portion $(-\delta,\delta)$ removed. The theorem's claim is that the function of $N$ given by

N \;\longmapsto\; \int_{[-\pi,-\delta]\cup[\delta,\pi]} \operatorname{fejerKernel}(N,\theta)\,d\theta

(the Lebesgue integral of $\operatorname{fejerKernel}(N,\cdot)$ restricted to that two-piece domain) tends to $0$ as $N\to\infty$ : precisely, as $N$ ranges over the natural numbers under the "eventually large" (atTop) filter, this sequence of real numbers converges, in the standard topology on $\mathbb{R}$ , to $0$ . No claim is made about the rate of convergence, about behavior for $\delta\le 0$ or $\delta\ge\pi$ , or about the integral over any other subset of $[-\pi,\pi]$ .

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