differentiable_completedCosZeta₀

English

For every a on the unit circle, completedCosZeta0 a is differentiable as a function of s over the complex plane.

Русский

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

LaTeX

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

Lean4

theorem differentiable_completedCosZeta₀ (a : UnitAddCircle) : Differentiable ℂ (completedCosZeta₀ a) :=
  ((hurwitzEvenFEPair a).symm.differentiable_Λ₀.comp (differentiable_id.div_const _)).div_const _

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