one_sub_eulerPrimePowerComplex_ne_zero

formal source

 447
 448/-- Therefore the factor `(1 - p^{-s})` never vanishes on the open right
 449half-plane. -/
 450theorem one_sub_eulerPrimePowerComplex_ne_zero {s : ℂ} (hs : 0 < s.re)
 451    (p : Nat.Primes) :
 452    1 - eulerPrimePowerComplex p s ≠ 0 := by
 453  have hone : eulerPrimePowerComplex p s ≠ 1 := by
 454    intro h
 455    have hnorm : ‖eulerPrimePowerComplex p s‖ = 1 := by
 456      simpa [h]
 457    have hlt := norm_eulerPrimePowerComplex_lt_one hs p
 458    linarith
 459  exact sub_ne_zero.mpr (by simpa [eq_comm] using hone)
 460
 461/-- Each regularized Euler factor is nonzero on the open right half-plane. -/
 462theorem eulerDet2FactorComplex_ne_zero {s : ℂ} (hs : 0 < s.re)
 463    (p : Nat.Primes) :
 464    eulerDet2FactorComplex p s ≠ 0 := by
 465  unfold eulerDet2FactorComplex
 466  refine mul_ne_zero ?_ (Complex.exp_ne_zero _)
 467  exact one_sub_eulerPrimePowerComplex_ne_zero hs p
 468
 469/-- Away from the pole at `1` and away from zeros of `ζ`, the reciprocal zeta
 470function is genuinely holomorphic. This gives the actual analytic object that a
 471future phase-lift witness should sample on circles. -/
 472theorem zetaReciprocal_differentiableAt {s : ℂ}
 473    (hs1 : s ≠ 1) (hz : riemannZeta s ≠ 0) :
 474    DifferentiableAt ℂ zetaReciprocal s := by
 475  simpa [zetaReciprocal] using (differentiableAt_riemannZeta hs1).inv hz
 476
 477/-! ### §5c. Complex carrier derivative bounds -/
 478
 479/-- The norm of the Euler eigenvalue equals the real `rpow` eigenvalue at `σ = Re(s)`.
 480This bridges the complex and real carrier theories. -/