rpow_const — Mathlib

English

If f has a derivative within s, then f^p has a derivative within s with derivative (p f^{p-1}) f'.

Русский

Если у f есть производная внутри s, то f^p имеет производную внутри s со производной (p f^{p-1}) f'.

LaTeX

$$$ \forall E [\text{NormedAddCommGroup } E] [\text{NormedSpace } \mathbb{R} E] \ {f: E \to \mathbb{R}, f': \text{StrongDual } \mathbb{R} E}, x, s, p:\, \text{HasFDerivWithinAt } f f' s x \Rightarrow (f(x) \neq 0 \lor 1 \le p) \Rightarrow \text{HasFDerivWithinAt} \left( x \mapsto f(x)^p \right) \left( (p f(x)^{p-1}) \cdot f' \right) s x$$

Lean4

@[simp]
theorem rpow_const (hf : DifferentiableAt ℝ f x) (h : f x ≠ 0 ∨ 1 ≤ p) : DifferentiableAt ℝ (fun x => f x ^ p) x :=
  (hf.hasFDerivAt.rpow_const h).differentiableAt

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