mathlib3 documentation

analysis.calculus.deriv.pow

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 has_strict_deriv_at_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (n : ) (x : 𝕜) :
has_strict_deriv_at (λ (x : 𝕜), x ^ n) (n * x ^ (n - 1)) x
theorem has_deriv_at_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (n : ) (x : 𝕜) :
has_deriv_at (λ (x : 𝕜), x ^ n) (n * x ^ (n - 1)) x
theorem has_deriv_within_at_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (n : ) (x : 𝕜) (s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), x ^ n) (n * x ^ (n - 1)) s x
theorem differentiable_at_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} (n : ) :
differentiable_at 𝕜 (λ (x : 𝕜), x ^ n) x
theorem differentiable_within_at_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} (n : ) :
differentiable_within_at 𝕜 (λ (x : 𝕜), x ^ n) s x
theorem differentiable_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (n : ) :
differentiable 𝕜 (λ (x : 𝕜), x ^ n)
theorem differentiable_on_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {s : set 𝕜} (n : ) :
differentiable_on 𝕜 (λ (x : 𝕜), x ^ n) s
theorem deriv_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} (n : ) :
deriv (λ (x : 𝕜), x ^ n) x = n * x ^ (n - 1)
@[simp]
theorem deriv_pow' {𝕜 : Type u} [nontrivially_normed_field 𝕜] (n : ) :
deriv (λ (x : 𝕜), x ^ n) = λ (x : 𝕜), n * x ^ (n - 1)
theorem deriv_within_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} (n : ) (hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (x : 𝕜), x ^ n) s x = n * x ^ (n - 1)
theorem has_deriv_within_at.pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} {c : 𝕜 𝕜} {c' : 𝕜} (n : ) (hc : has_deriv_within_at c c' s x) :
has_deriv_within_at (λ (y : 𝕜), c y ^ n) (n * c x ^ (n - 1) * c') s x
theorem has_deriv_at.pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {c : 𝕜 𝕜} {c' : 𝕜} (n : ) (hc : has_deriv_at c c' x) :
has_deriv_at (λ (y : 𝕜), c y ^ n) (n * c x ^ (n - 1) * c') x
theorem deriv_within_pow' {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} {c : 𝕜 𝕜} (n : ) (hc : differentiable_within_at 𝕜 c s x) (hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (x : 𝕜), c x ^ n) s x = n * c x ^ (n - 1) * deriv_within c s x
@[simp]
theorem deriv_pow'' {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {c : 𝕜 𝕜} (n : ) (hc : differentiable_at 𝕜 c x) :
deriv (λ (x : 𝕜), c x ^ n) x = n * c x ^ (n - 1) * deriv c x