cpow — Mathlib

English

The map (x,y) ↦ x^y from ℂ×ℂ to ℂ is Frechet differentiable at points with x ≠ 0 on slitPlane, with a derivative given by the standard cpow formula.

Русский

Отображение (x,y) ↦ x^y с ℂ×ℂ в ℂ дифференцируемо в точках с x ≠ 0 на slitPlane, производная дана стандартной формулой cpow.

LaTeX

$$$\\\\forall p \\\\in \\\\text{slitPlane}, \\\\text{HasStrictFDerivAt } (p \\mapsto p_1^{p_2}) = (p_2 p_1^{p_2-1}) \\\\cdot fst + (p_1^{p_2} \\\\log p_1) \\\\cdot snd$$$

Lean4

@[fun_prop]
theorem cpow (hf : DifferentiableAt ℂ f x) (hg : DifferentiableAt ℂ g x) (h0 : f x ∈ slitPlane) :
    DifferentiableAt ℂ (fun x => f x ^ g x) x :=
  (hf.hasFDerivAt.cpow hg.hasFDerivAt h0).differentiableAt

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