Derivative of (f x) ^ n, n : ℕ#

In this file we prove that (x ^ n)' = n * x ^ (n - 1), where n is a natural number.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of Analysis/Calculus/Deriv/Basic.

Keywords #

derivative, power

Derivative of x ↦ x^n for n : ℕ#

theorem hasStrictDerivAt_pow {𝕜 : Type u} (n : ) (x : 𝕜) :
HasStrictDerivAt (fun (x : 𝕜) => x ^ n) (n * x ^ (n - 1)) x
theorem hasDerivAt_pow {𝕜 : Type u} (n : ) (x : 𝕜) :
HasDerivAt (fun (x : 𝕜) => x ^ n) (n * x ^ (n - 1)) x
theorem hasDerivWithinAt_pow {𝕜 : Type u} (n : ) (x : 𝕜) (s : Set 𝕜) :
HasDerivWithinAt (fun (x : 𝕜) => x ^ n) (n * x ^ (n - 1)) s x
theorem differentiableAt_pow {𝕜 : Type u} {x : 𝕜} (n : ) :
DifferentiableAt 𝕜 (fun (x : 𝕜) => x ^ n) x
theorem differentiableWithinAt_pow {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (n : ) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => x ^ n) s x
theorem differentiable_pow {𝕜 : Type u} (n : ) :
Differentiable 𝕜 fun (x : 𝕜) => x ^ n
theorem differentiableOn_pow {𝕜 : Type u} {s : Set 𝕜} (n : ) :
DifferentiableOn 𝕜 (fun (x : 𝕜) => x ^ n) s
theorem deriv_pow {𝕜 : Type u} {x : 𝕜} (n : ) :
deriv (fun (x : 𝕜) => x ^ n) x = n * x ^ (n - 1)
@[simp]
theorem deriv_pow' {𝕜 : Type u} (n : ) :
(deriv fun (x : 𝕜) => x ^ n) = fun (x : 𝕜) => n * x ^ (n - 1)
theorem derivWithin_pow {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} (n : ) (hxs : ) :
derivWithin (fun (x : 𝕜) => x ^ n) s x = n * x ^ (n - 1)
theorem HasDerivWithinAt.pow {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {c : 𝕜𝕜} {c' : 𝕜} (n : ) (hc : HasDerivWithinAt c c' s x) :
HasDerivWithinAt (fun (y : 𝕜) => c y ^ n) (n * c x ^ (n - 1) * c') s x
theorem HasDerivAt.pow {𝕜 : Type u} {x : 𝕜} {c : 𝕜𝕜} {c' : 𝕜} (n : ) (hc : HasDerivAt c c' x) :
HasDerivAt (fun (y : 𝕜) => c y ^ n) (n * c x ^ (n - 1) * c') x
theorem derivWithin_pow' {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {c : 𝕜𝕜} (n : ) (hc : ) (hxs : ) :
derivWithin (fun (x : 𝕜) => c x ^ n) s x = n * c x ^ (n - 1) * derivWithin c s x
@[simp]
theorem deriv_pow'' {𝕜 : Type u} {x : 𝕜} {c : 𝕜𝕜} (n : ) (hc : ) :
deriv (fun (x : 𝕜) => c x ^ n) x = n * c x ^ (n - 1) * deriv c x