def riemannzeta1 : Lean.ParserDescr

Equations

• riemannzeta1 = Lean.ParserDescr.node `riemannzeta1 1024 (Lean.ParserDescr.symbol "ζ")

def derivriemannzeta1 : Lean.ParserDescr

Equations

• derivriemannzeta1 = Lean.ParserDescr.node `derivriemannzeta1 1024 (Lean.ParserDescr.symbol "ζ'")

theorem Z0bound_aux : (fun (delta : ℝ) => -(deriv riemannZeta / riemannZeta) (1 + ↑delta) - 1 / ↑delta) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1

theorem Z0bound : (fun (delta : ℝ) => -logDerivZeta (1 + ↑delta) - 1 / ↑delta) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1