differentiable_completedHurwitzZetaOdd

English

The function a ↦ completedHurwitzZetaOdd(a) is differentiable in the complex sense for every a in UnitAddCircle.

Русский

Функция a ↦ completedHurwitzZetaOdd(a) дифференцируема комплексно для каждого a на единичном круге.

LaTeX

$$$$ \text{For all } a, \ \text{completedHurwitzZetaOdd}(a) \text{ is differentiable as a function of } s \in \mathbb{C}. $$$$

Lean4

theorem differentiable_completedHurwitzZetaOdd (a : UnitAddCircle) : Differentiable ℂ (completedHurwitzZetaOdd a) :=
  ((hurwitzOddFEPair a).differentiable_Λ.comp ((differentiable_id.add_const 1).div_const 2)).div_const 2

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