eulerDet2FactorComplex_ne_zero

formal source

 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. -/
 481theorem norm_eulerPrimePowerComplex_eq_rpow (p : Nat.Primes) (s : ℂ) :
 482    ‖eulerPrimePowerComplex p s‖ = (p : ℝ) ^ (-s.re) := by
 483  rw [norm_eulerPrimePowerComplex,
 484      Real.rpow_def_of_pos (by exact_mod_cast p.prop.pos : (0 : ℝ) < p)]
 485  congr 1; simp [primeLog]; ring
 486
 487/-- Norm bound for the per-prime complex log-derivative contribution.
 488The numerator uses `norm_mul`/`norm_pow`/`norm_ofReal`, and the denominator
 489uses the reverse triangle inequality `1 − ‖z‖ ≤ ‖1 − z‖`. -/
 490theorem norm_eulerPrimeLogDerivTermComplex_le {s : ℂ} (hs : 0 < s.re)
 491    (p : Nat.Primes) :
 492    ‖eulerPrimeLogDerivTermComplex p s‖ ≤