differentiableAt_riemannZeta — Mathlib

English

The Riemann zeta function is complex-differentiable at every point s with s ≠ 1 (i.e., away from 1).

Русский

Задача дзета Римана: она комплексно дифференцируема во всех точках, кроме s = 1.

LaTeX

$$$\\forall s \\in \\mathbb{C},\\ s \\neq 1 \\Rightarrow \\text{Differentiable}( \\riemannZeta, s)$$$

Lean4

/-- The Riemann zeta function is differentiable away from `s = 1`. -/
theorem differentiableAt_riemannZeta {s : ℂ} (hs' : s ≠ 1) : DifferentiableAt ℂ riemannZeta s :=
  differentiableAt_hurwitzZetaEven _ hs'

Похожие утверждения