deLaValleePoussin_trig_kernel_eq_square

formal source

  32
  33/-- The classical nonnegative trigonometric kernel used in the
  34Hadamard-de la Vallee-Poussin argument. -/
  35theorem deLaValleePoussin_trig_kernel_eq_square (θ : ℝ) :
  36    3 + 4 * Real.cos θ + Real.cos (2 * θ) =
  37      2 * (Real.cos θ + 1) ^ 2 := by
  38  rw [Real.cos_two_mul]
  39  ring
  40
  41/-- Positivity of the de la Vallee-Poussin trigonometric kernel. -/
  42theorem deLaValleePoussin_trig_kernel_nonneg (θ : ℝ) :
  43    0 ≤ 3 + 4 * Real.cos θ + Real.cos (2 * θ) := by
  44  rw [deLaValleePoussin_trig_kernel_eq_square θ]
  45  nlinarith [sq_nonneg (Real.cos θ + 1)]
  46
  47/-! ## 2. Exact analytic input needed for the logarithmic strip -/
  48
  49/-- The classical Hadamard-de la Vallee-Poussin zero-free strip, stated in the
  50same shape as `StripZeroFreeRegion.LogZeroFreeStrip`.
  51
  52This is intentionally a structure, not an axiom. Supplying an inhabitant is the
  53real Mathlib-grade analytic work: logarithmic derivative estimates for `ζ`,
  54the positivity kernel above, and control of the pole at `s = 1`. -/
  55structure DeLaValleePoussinZeroFreeRegion where
  56  c : ℝ
  57  T : ℝ
  58  c_pos : 0 < c
  59  T_gt_one : 1 < T
  60  zero_free :
  61    ∀ s : ℂ, T ≤ |s.im| →
  62      1 - c / Real.log |s.im| < s.re →
  63        riemannZeta s ≠ 0
  64
  65/-- The classical zero-free-region input directly inhabits the Phase 5