hasFDerivAt_cpow — Mathlib

English

The map x ↦ x^y is Frechet differentiable with derivative given by the same combination as strict derivative.

Русский

Отображение x ↦ x^y различимо по Фреше с производной по тем же формулам.

LaTeX

$$$\\\\forall p \\, (hp), HasFDerivAt (\\\\lambda x, x_1^{x_2}) ( ... ) p$$$

Lean4

theorem hasFDerivAt_cpow {p : ℂ × ℂ} (hp : p.1 ∈ slitPlane) :
    HasFDerivAt (fun x : ℂ × ℂ => x.1 ^ x.2)
      ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ)
      p :=
  (hasStrictFDerivAt_cpow hp).hasFDerivAt

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