differentiableAt_sinZeta — Mathlib

English

For every a in the unit circle, the map s ↦ sinZeta(a, s) is differentiable as a function of the complex variable s; i.e., sinZeta(a) is differentiable on ℂ for each a.

Русский

Для каждого a из единичного круга отображение s ↦ sinZeta(a, s) дифференцируемо по комплексной переменной s; то есть sinZeta(a) дифференцируема наℂ для каждого a.

LaTeX

$$$$ \dfrac{d}{ds}\sinZeta(a,s) \text{ существует для всех } a\in\,\mathrm{UnitAddCircle},\; s\in\mathbb{C}. $$$$

Lean4

/-- The sine zeta function is differentiable everywhere. -/
theorem differentiableAt_sinZeta (a : UnitAddCircle) : Differentiable ℂ (sinZeta a) :=
  (differentiable_completedSinZeta a).mul <|
    differentiable_Gammaℝ_inv.comp <| differentiable_id.add <| differentiable_const _

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