differentiableAt_completedZeta — Mathlib

English

The completed Riemann zeta function Λ is differentiable away from s = 0 and s = 1.

Русский

Функция Λ(s) дифференцируема за исключением точек s = 0 и s = 1.

LaTeX

$$$\\text{Differentiable at } s: s\\neq 0, s\\neq 1\\; \\Rightarrow \\; \\text{Differentiable}(\\Lambda,s)$$$

Lean4

/-- The completed Riemann zeta function `Λ(s)` is differentiable away from `s = 0` and `s = 1`. -/
theorem differentiableAt_completedZeta {s : ℂ} (hs : s ≠ 0) (hs' : s ≠ 1) : DifferentiableAt ℂ completedRiemannZeta s :=
  differentiableAt_completedHurwitzZetaEven 0 (Or.inl hs) hs'

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