Prove2Me

Nonnegativity of the Fejér kernel

Proved
Fejer.fejerKernel_nonneg

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

fourier-seriesharmonic-analysis

FN(θ)≥0F_N(\theta) \ge 0 for every NN and every θ\theta.

Formal statement
import Mathlib
import Definitions.Def_Fejer_fejerKernel

namespace Fejer

/-- **Nonnegativity of the Fejér kernel.** `F_N(θ) ≥ 0` for every `N` and every `θ`. -/
theorem fejerKernel_nonneg (N : ℕ) (θ : ℝ) : 0 ≤ fejerKernel N θ := 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 states that for every natural number NN and every real number θ\theta — with no hypothesis constraining θ\theta in any way — the quantity fejerKernel N θ, i.e. ∑n=−NN(1−∣n∣N+1)cos⁡(nθ)\sum_{n=-N}^{N}\left(1 - \frac{|n|}{N+1}\right)\cos(n\theta), satisfies 0≤fejerKernel N θ0 \le \text{fejerKernel}\ N\ \theta. In particular, this claim is made unconditionally for all real θ\theta, including values θ=2πk\theta = 2\pi k for integer kk — precisely the values that the hypothesis hθ in fejerKernel_closed_form excludes — as well as all other reals; there is no case distinction or side condition of any kind in this statement.

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