differentiableAt_const_cpow_of_neZero

English

Let z ∈ ℂ with z ≠ 0. For any t ∈ ℂ, the function s ↦ z^{s} is differentiable at s = t with derivative z^{t} log z.

Русский

Пусть z ∈ ℂ и z ≠ 0. Для любого t ∈ ℂ функция s ↦ z^{s} дифференцируема в точке s = t, производная равна z^{t} log z.

LaTeX

$$$\\text{For }z\\in\\mathbb{C},\\ z\\neq 0,\\ \\text{and }t\\in\\mathbb{C},\\ \\text{the map } s\\mapsto z^{s} \\text{ is differentiable at } s=t\\text{ with } \\frac{d}{ds}z^{s}\\big|_{s=t}=z^{t}\\log z.$$$

Lean4

@[fun_prop]
theorem differentiableAt_const_cpow_of_neZero (z : ℂ) [NeZero z] (t : ℂ) : DifferentiableAt ℂ (fun s : ℂ ↦ z ^ s) t :=
  differentiableAt_id.const_cpow (.inl <| NeZero.ne z)

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