deriv_fun_pow — Mathlib

English

For DifferentiableWithinAt h, the formula for derivWithin of pow holds with deriv f s x.

Русский

Для DifferentiableWithinAt h формула derivWithin для f^n сохраняется с deriv f s x.

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]
theorem deriv_fun_pow (h : DifferentiableAt 𝕜 f x) (n : ℕ) :
    deriv (fun x => f x ^ n) x = n * f x ^ (n - 1) * deriv f x :=
  (h.hasDerivAt.pow n).deriv

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