differentiable_completedHurwitzZetaEven₀

English

For every a on the unit circle, the function s ↦ completedHurwitzZetaEven0 a is differentiable as a function of the complex variable s.

Русский

Для каждого a на единичном окружности функция s ↦ completedHurwitzZetaEven0 a является дифференцируемой по комплексной переменной s.

LaTeX

$$$\\forall a \\in \\text{UnitAddCircle},\\ \\mathrm{Differentiable}_{\\mathbb{C}}(\\mathrm{completedHurwitzZetaEven_0}(a)).$$$

Lean4

theorem differentiable_completedHurwitzZetaEven₀ (a : UnitAddCircle) : Differentiable ℂ (completedHurwitzZetaEven₀ a) :=
  ((hurwitzEvenFEPair a).differentiable_Λ₀.comp (differentiable_id.div_const _)).div_const _

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