deriv_fun_pow' — Mathlib

English

If f is differentiableWithinAt at x, then derivWithin (f^n) within s at x equals the sum with derivWithin f s x replacing the derivative.

Русский

Если f дифференцируема внутри x, то производная f^n внутри s в x равна сумме, где производная f внутри s заменяет производную функции.

LaTeX

$$$$\\operatorname{derivWithin}\\bigl(f(x)^n\\bigr)\\, s\\ x = \\sum_{i=0}^{n-1} f(x)^{\,n-1-i}\\, (\\operatorname{derivWithin} f\\, s\\ x)\\, f(x)^{\,i}. $$$$

Lean4

@[simp low]
theorem deriv_fun_pow' (h : DifferentiableAt 𝕜 f x) (n : ℕ) :
    deriv (fun x => f x ^ n) x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * deriv f x * f x ^ i :=
  (h.hasDerivAt.pow' n).deriv

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