derivWithin_pow' — Mathlib

English

DifferentiableWithinAt h of f at x implies the derivative of f^n within s obeys the same rule with derivWithin f s x in place of f'.

Русский

Если f дифференцируема внутри s в x, то производная f^n внутри s следует той же схеме, но вместо производной функция использует derivWithin f s x.

LaTeX

$$$$\\text{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 derivWithin_pow' (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) :
    derivWithin (f ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i :=
  derivWithin_fun_pow' h n

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