The Fejér–Jackson inequality

Every partial sum ∑_{k=1}^{M} sin(kθ)/k is strictly positive for θ ∈ (0, π).

The proof is the classical interior-minimum argument. The derivative is the shifted Dirichlet kernel, handled without division: 2 sin(θ/2) ∑_{k=1}^M cos(kθ) = sin((M + ½)θ) - sin(θ/2). At an interior minimum the derivative vanishes, which forces sin(Mθ) ≥ 0, so the minimum is at least the previous partial sum, positive by induction; the boundary values are 0.

Main definitions

• Dilog.fejerSum M θ: ∑_{k=1}^M sin(kθ)/k.

Main results

• Dilog.dirichlet_telescope: the telescoped Dirichlet kernel.
• Dilog.fejerSum_pos: the Fejér–Jackson inequality.

References

• D. Jackson, Über eine trigonometrische Summe, Rend. Circ. Mat. Palermo 32 (1911) 257–262.

noncomputable def Dilog.fejerSum (M : ℕ) (θ : ℝ) : ℝ

The Fejér–Jackson partial sum ∑_{k=1}^{M} sin(kθ)/k (indexed k ∈ range M with summand sin((k+1)θ)/(k+1)).

Equations

• Dilog.fejerSum M θ = ∑ k ∈ Finset.range M, Real.sin ((↑k + 1) * θ) / (↑k + 1)

@[simp]

theorem Dilog.fejerSum_zero_arg (M : ℕ) : fejerSum M 0 = 0

@[simp]

theorem Dilog.fejerSum_pi (M : ℕ) : fejerSum M Real.pi = 0

theorem Dilog.continuous_fejerSum (M : ℕ) : Continuous (fejerSum M)

theorem Dilog.hasDerivAt_fejerSum (M : ℕ) (θ : ℝ) : HasDerivAt (fejerSum M) (∑ k ∈ Finset.range M, Real.cos ((↑k + 1) * θ)) θ

Termwise differentiation: fejerSum M has derivative the shifted Dirichlet kernel ∑_{k=1}^M cos(kθ).

theorem Dilog.dirichlet_telescope (M : ℕ) (θ : ℝ) : 2 * Real.sin (θ / 2) * ∑ k ∈ Finset.range M, Real.cos ((↑k + 1) * θ) = Real.sin ((↑M + 1 / 2) * θ) - Real.sin (θ / 2)

The multiplicative (division-free) Dirichlet kernel identity: 2 sin(θ/2) · ∑_{k=1}^M cos(kθ) = sin((M+½)θ) − sin(θ/2), by telescoping.

theorem Dilog.sin_last_nonneg_at_localMin {M : ℕ} {θ₀ : ℝ} (h0 : 0 < θ₀) (hπ : θ₀ < Real.pi) (hmin : IsLocalMin (fejerSum M) θ₀) : 0 ≤ Real.sin (↑M * θ₀)

The critical-point dichotomy: at an interior local minimum of fejerSum M, the "last term" sine sin(Mθ₀) is nonnegative — the two branches of the equality sin((M+½)θ₀) = sin(θ₀/2) give sin(Mθ₀) = 0 or sin(Mθ₀) = sin θ₀ > 0.

theorem Dilog.fejerSum_pos (M : ℕ) : 1 ≤ M → ∀ {θ : ℝ}, 0 < θ → θ < Real.pi → 0 < fejerSum M θ

The Fejér–Jackson inequality (Fejér 1910, Jackson 1911): every partial sum ∑_{k=1}^{M} sin(kθ)/k with M ≥ 1 is strictly positive on (0, π).