differentiableAt_expZeta — Mathlib

English

For a ∈ UnitAddCircle, s ∈ C and with the condition s ≠ 1 or a ≠ 0, the exponential zeta expZeta(a) is differentiable in s.

Русский

Для a ∈ UnitAddCircle и s ∈ C, при условии s ≠ 1 или a ≠ 0, expZeta(a) дифференцируема по переменной s.

LaTeX

$$$\\forall a\\in \\mathrm{UnitAddCircle},\\ \\forall s\\in\\mathbb{C},\\ (s\\neq 1\\lor a\\neq 0)\\Rightarrow \\text{Differentiable}_{\\mathbb{C}}\\bigl( \\expZeta(a,s) \\bigr).$$$

Lean4

theorem differentiableAt_expZeta (a : UnitAddCircle) (s : ℂ) (hs : s ≠ 1 ∨ a ≠ 0) : DifferentiableAt ℂ (expZeta a) s :=
  by
  apply DifferentiableAt.add
  · exact differentiableAt_cosZeta a hs
  · apply (differentiableAt_const _).mul (differentiableAt_sinZeta a s)

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