differentiable_completedSinZeta — Mathlib

English

The function a ↦ completedSinZeta(a) is differentiable in the complex sense for all a.

Русский

Функция a ↦ completedSinZeta(a) комплексно дифференцируема для всех a.

LaTeX

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

Lean4

theorem differentiable_completedSinZeta (a : UnitAddCircle) : Differentiable ℂ (completedSinZeta a) :=
  ((hurwitzOddFEPair a).symm.differentiable_Λ.comp ((differentiable_id.add_const 1).div_const 2)).div_const 2

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