pow — Mathlib

English

The HasStrictFDerivAt.pow' lemma provides the explicit derivative of the power function f^n in the strict Fréchet sense, given a differentiable f and its derivative f'.

Русский

Лемма HasStrictFDerivAt.pow' даёт явную производную функции x ↦ f(x)^n в строгом смысле Фрете, когда дано дифференцируемое f и производная f'.

LaTeX

$$$\\text{HasStrictFDerivAt}\\ f f' x \\Rightarrow \\text{HasStrictFDerivAt}\\ (f^n)\\ (\\sum_{i=0}^{n-1} f(x)^{n-1-i} \\; f' \\; f(x)^i)\\ x$$$

Lean4

@[fun_prop]
theorem pow (hf : DifferentiableWithinAt 𝕜 f s x) : ∀ n : ℕ, DifferentiableWithinAt 𝕜 (f ^ n) s x :=
  hf.fun_pow

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