hasStrictFDerivAt_cpow' — Mathlib

English

Same differentiability statement as above, stated in a compact wrapper form.

Русский

Та же идея непрерывности производной cpow, формулированная в компактной форме.

LaTeX

$$$\\forall p \\in \\mathbb{C}^2, \\; \\text{HasStrictFDerivAt } (x \\mapsto x_1^{x_2}) = \\cdot$ (wrapper form)$$

Lean4

theorem hasStrictFDerivAt_cpow' {x y : ℂ} (hp : x ∈ slitPlane) :
    HasStrictFDerivAt (fun x : ℂ × ℂ => x.1 ^ x.2)
      ((y * x ^ (y - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (x ^ y * log x) • ContinuousLinearMap.snd ℂ ℂ ℂ) (x, y) :=
  @hasStrictFDerivAt_cpow (x, y) hp

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