deLaValleePoussin_trig_kernel_nonneg
plain-language theorem explainer
The theorem establishes nonnegativity of the trigonometric kernel 3 + 4 cos θ + cos 2θ for every real angle θ. Number theorists building classical zero-free regions for the Riemann zeta function cite this elementary positivity fact. The proof reduces the expression to twice the square of (cos θ + 1) by algebraic identity and concludes via nonnegativity of squares.
Claim. For all real numbers θ, 3 + 4 cos θ + cos(2θ) ≥ 0.
background
The module ClassicalZeroFreeRegion tracks track B1 of the RH unconditional-closure plan. Mathlib supplies the boundary result riemannZeta_ne_zero_of_one_le_re but lacks a formal Hadamard-de la Vallee-Poussin logarithmic zero-free strip. This module isolates the elementary trigonometric positivity kernel 3 + 4 cos θ + cos 2θ and shows it equals 2(cos θ + 1)^2.
proof idea
The proof first rewrites the kernel via its algebraic identity to twice the square of (cos θ + 1). It then applies nlinarith to the nonnegativity of that square.
why it matters
This supplies the trig_kernel_nonneg field inside the ClassicalZeroFreeRegionAttackSurface definition. It fills the elementary positivity step required for the classical zero-free region construction described in the module documentation. The result touches the open question of supplying a Mathlib-grade inhabitant for the full LogZeroFreeStrip structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.