derivWithin_pow — Mathlib

English

DifferentiableWithinAt h of f s x implies the equation for derWithin of f^n with derivative in the sum.

Русский

Дифференцируемость внутри h отличается тем, что derivWithin 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 derivWithin_pow (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) :
    derivWithin (f ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x :=
  derivWithin_fun_pow h n

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