fun_pow' — Mathlib

English

If a function f has strict derivative f' at x, then for any n, the derivative of f^n at x is the sum over i of f(x)^{n-1-i} f' f(x)^i, i from 0 to n-1.

Русский

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

LaTeX

$$$HasStrictDerivAt\left(f, f', x\right) \Rightarrow \forall n, HasStrictDerivAt\left(f^n, \left(\sum_{i=0}^{n-1} f(x)^{n-1-i} \cdot f' \cdot f(x)^i\right), x\right)$$$

Lean4

nonrec theorem fun_pow' (h : HasStrictDerivAt f f' x) (n : ℕ) :
    HasStrictDerivAt (fun x ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x :=
  by
  unfold HasStrictDerivAt
  convert h.pow' n
  ext
  simp

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