boundaryZeroFreeCert

formal source

  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
  68/-- The strip theorem as the next named bridge. -/
  69def StripZeroFreeBridge : Prop :=
  70  Nonempty LogZeroFreeStrip
  71
  72/-- Any strip bridge gives the corresponding zero-free conclusion. -/
  73theorem riemannZeta_ne_zero_in_log_strip
  74    (bridge : StripZeroFreeBridge) :
  75    ∃ c T : ℝ, 0 < c ∧ 1 < T ∧
  76      ∀ s : ℂ, T ≤ |s.im| →