riemannZeta_ne_zero_re_gt_one

formal source

  34  riemannZeta_ne_zero_of_one_le_re hs
  35
  36/-- The corresponding strict half-plane theorem. -/
  37theorem riemannZeta_ne_zero_re_gt_one {s : ℂ} (hs : 1 < s.re) :
  38    riemannZeta s ≠ 0 :=
  39  riemannZeta_ne_zero_of_one_lt_re hs
  40
  41/-- Certificate for the proved boundary zero-free region. -/
  42structure BoundaryZeroFreeCert where
  43  ge_one : ∀ s : ℂ, 1 ≤ s.re → riemannZeta s ≠ 0
  44  gt_one : ∀ s : ℂ, 1 < s.re → riemannZeta s ≠ 0
  45
  46def boundaryZeroFreeCert : BoundaryZeroFreeCert where
  47  ge_one := fun _ hs => riemannZeta_ne_zero_re_ge_one hs
  48  gt_one := fun _ hs => riemannZeta_ne_zero_re_gt_one hs
  49
  50/-! ## 2. The true strip target -/
  51
  52/-- A logarithmic zero-free strip with constants `c` and `T`.
  53
  54For `|Im(s)| ≥ T`, the region
  55`Re(s) > 1 - c / log(|Im(s)|)` is zero-free. This is the classical
  56Hadamard-de la Vallée-Poussin shape, stated as the exact bridge needed by
  57the RS program. -/
  58structure LogZeroFreeStrip where
  59  c : ℝ
  60  T : ℝ
  61  c_pos : 0 < c
  62  T_gt_one : 1 < T
  63  zero_free :
  64    ∀ s : ℂ, T ≤ |s.im| →
  65      1 - c / Real.log |s.im| < s.re →
  66        riemannZeta s ≠ 0
  67