differentiable_hurwitzZetaOdd — Mathlib

English

The odd Hurwitz zeta function is differentiable everywhere with respect to the complex variable s.

Русский

Нечетная часть Хёрвитца ζ-функции дифференцируема повсюду по переменной s.

LaTeX

$$$$ \text{The map } s \mapsto \operatorname{hurwitzZetaOdd}(a,s) \text{ is differentiable on } \mathbb{C}. $$$$

Lean4

/-- The odd Hurwitz zeta function is differentiable everywhere. -/
theorem differentiable_hurwitzZetaOdd (a : UnitAddCircle) : Differentiable ℂ (hurwitzZetaOdd a) :=
  (differentiable_completedHurwitzZetaOdd a).mul <|
    differentiable_Gammaℝ_inv.comp <| differentiable_id.add <| differentiable_const _

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