theorem RiemannZetaFunction.riemannZeta_eq_tsum_one_div_nat_cpow {s : ℂ} (hs : 1 < s.re) : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s

theorem RiemannZetaFunction.riemannZeta_eulerProduct_hasProd {s : ℂ} (hs : 1 < s.re) : HasProd (fun (p : Nat.Primes) => (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s)

theorem RiemannZetaFunction.riemannZeta_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : riemannZeta s ≠ 0

theorem RiemannZetaFunction.riemannZeta_eulerProduct_and_nonvanishing {s : ℂ} (hs : 1 < s.re) : HasProd (fun (p : Nat.Primes) => (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s) ∧ riemannZeta s ≠ 0

theorem RiemannZetaFunction.riemannZeta_differentiableAt {s : ℂ} (hs : s ≠ 1) : DifferentiableAt ℂ riemannZeta s

theorem RiemannZetaFunction.riemannZeta_residue_eq_one : Filter.Tendsto (fun (s : ℂ) => (s - 1) * riemannZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1)

theorem RiemannZetaFunction.riemannZeta_meromorphic_with_residue : (∀ (s : ℂ), s ≠ 1 → DifferentiableAt ℂ riemannZeta s) ∧ Filter.Tendsto (fun (s : ℂ) => (s - 1) * riemannZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1)

theorem RiemannZetaFunction.mertens_norm_zeta_product_ge_one (x y : ℝ) (hx : 1 < x) : ‖riemannZeta ↑x ^ 3 * riemannZeta (↑x + ↑y * Complex.I) ^ 4 * riemannZeta (↑x + 2 * ↑y * Complex.I)‖ ≥ 1

theorem RiemannZetaFunction.riemannZeta_ne_zero_of_one_le_re {s : ℂ} (hs : 1 ≤ s.re) : riemannZeta s ≠ 0