rpow_const — Mathlib

English

If f has a strict derivative and p is real, then x ↦ f(x)^p is strictly differentiable with derivative (p f(x)^{p-1}) f'(x) at the point.

Русский

Если функция f имеет строгую производную, то x ↦ f(x)^p дифференцируема строго, её производная равна (p f(x)^{p-1}) f'(x) в точке.

LaTeX

$$$ \forall f:\,E\to\mathbb{R}, f', x, p:\, \text{HasStrictFDerivAt } f f' x \Rightarrow (f(x) \neq 0 \lor 1 \le p) \Rightarrow \text{HasStrictFDerivAt} \left( x \mapsto f(x)^p \right) \left( (p f(x)^{p-1}) \cdot f' \right) x $$$

Lean4

theorem rpow_const (hf : HasStrictFDerivAt f f' x) (h : f x ≠ 0 ∨ 1 ≤ p) :
    HasStrictFDerivAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • f') x :=
  (hasStrictDerivAt_rpow_const h).comp_hasStrictFDerivAt x hf

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