def riemannzeta' : Lean.ParserDescr

Equations

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

def derivriemannzeta' : Lean.ParserDescr

Equations

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

theorem ZetaNoZerosOn1Line' (t : ℝ) : riemannZeta (1 + ↑t * Complex.I) ≠ 0

theorem ZetaCont' : ContinuousOn riemannZeta (Set.univ \ {1})

theorem ZetaNoZerosInBox' (T : ℝ) : ∃ (σ : ℝ) (_ : σ < 1), ∀ (t : ℝ), |t| ≤ T → ∀ σ' ≥ σ, riemannZeta (↑σ' + ↑t * Complex.I) ≠ 0

theorem LogDerivZetaHoloOn' {S : Set ℂ} (s_ne_one : 1 ∉ S) (nonzero : ∀ s ∈ S, riemannZeta s ≠ 0) : HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) S

theorem LogDerivZetaHolcSmallT' : ∃ (σ₂ : ℝ) (_ : σ₂ < 1), HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) (Set.uIcc σ₂ 2 ×ℂ Set.uIcc (-3) 3 \ {1})

theorem LogDerivZetaHolcLargeT' : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)), ∀ (T : ℝ), 3 ≤ T → HolomorphicOn (fun (s : ℂ) => deriv riemannZeta s / riemannZeta s) (Set.Icc (1 - A / Real.log T ^ 1) 2 ×ℂ Set.Icc (-T) T \ {1})