fderiv_norm_rpow — Mathlib

English

For differentiable f, the derivative formula for the function x ↦ ‖f(x)‖^p is given by the chain rule with inner derivatives.

Русский

Для дифференцируемой f формула производной по x функции x ↦ ‖f(x)‖^p выражается через цепное правило с внутренней производной.

LaTeX

$$fderiv Real (x ↦ ‖f x‖^p) x = (p‖f x‖^{p-2}) • (innerSL (f x) ∘ f' x)$$

Lean4

theorem fderiv_norm_rpow {f : F → E} (hf : Differentiable ℝ f) {x : F} {p : ℝ} (hp : 1 < p) :
    fderiv ℝ (fun x ↦ ‖f x‖ ^ p) x = (p * ‖f x‖ ^ (p - 2)) • (innerSL ℝ (f x)).comp (fderiv ℝ f x) :=
  hasFDerivAt_norm_rpow (f x) hp |>.comp x (hf x).hasFDerivAt |>.fderiv

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