fun_pow — Mathlib

English

If f is differentiable with a strict derivative at x, then for every n, HasStrictDerivAt of f^n at x equals the sum ∑_{i=0}^{n-1} f(x)^{n-1-i} (f') f(x)^i with the appropriate interpretation of f' as the derivative value.

Русский

Если f имеет строгое производное в x, то для любого n производная f(x)^n в x равна сумме ∑_{i=0}^{n-1} f(x)^{n-1-i} f'(x) f(x)^i.

LaTeX

$$$$\text{HasStrictDerivAt}(f^n,\; n\cdot f(x)^{n-1}\cdot f',\; x) $$$$

Lean4

nonrec theorem fun_pow (h : HasStrictDerivAt f f' x) (n : ℕ) :
    HasStrictDerivAt (fun x ↦ f x ^ n) (n * f x ^ (n - 1) * f') x :=
  by
  unfold HasStrictDerivAt
  convert h.pow n
  ext
  simp [mul_assoc]

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