# mathlib3documentation

analysis.calculus.deriv.zpow

# Derivatives of x ^ m, m : ℤ#

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

In this file we prove theorems about (iterated) derivatives of x ^ m, m : ℤ.

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^m for m : ℤ#

theorem has_strict_deriv_at_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (h : x 0 0 m) :
has_strict_deriv_at (λ (x : 𝕜), x ^ m) (m * x ^ (m - 1)) x
theorem has_deriv_at_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (h : x 0 0 m) :
has_deriv_at (λ (x : 𝕜), x ^ m) (m * x ^ (m - 1)) x
theorem has_deriv_within_at_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (h : x 0 0 m) (s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), x ^ m) (m * x ^ (m - 1)) s x
theorem differentiable_at_zpow {𝕜 : Type u} {x : 𝕜} {m : } :
(λ (x : 𝕜), x ^ m) x x 0 0 m
theorem differentiable_within_at_zpow {𝕜 : Type u} {s : set 𝕜} (m : ) (x : 𝕜) (h : x 0 0 m) :
(λ (x : 𝕜), x ^ m) s x
theorem differentiable_on_zpow {𝕜 : Type u} (m : ) (s : set 𝕜) (h : 0 s 0 m) :
(λ (x : 𝕜), x ^ m) s
theorem deriv_zpow {𝕜 : Type u} (m : ) (x : 𝕜) :
deriv (λ (x : 𝕜), x ^ m) x = m * x ^ (m - 1)
@[simp]
theorem deriv_zpow' {𝕜 : Type u} (m : ) :
deriv (λ (x : 𝕜), x ^ m) = λ (x : 𝕜), m * x ^ (m - 1)
theorem deriv_within_zpow {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {m : } (hxs : x) (h : x 0 0 m) :
deriv_within (λ (x : 𝕜), x ^ m) s x = m * x ^ (m - 1)
@[simp]
theorem iter_deriv_zpow' {𝕜 : Type u} (m : ) (k : ) :
deriv^[k] (λ (x : 𝕜), x ^ m) = λ (x : 𝕜), (finset.range k).prod (λ (i : ), m - i) * x ^ (m - k)
theorem iter_deriv_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (k : ) :
deriv^[k] (λ (y : 𝕜), y ^ m) x = (finset.range k).prod (λ (i : ), m - i) * x ^ (m - k)
theorem iter_deriv_pow {𝕜 : Type u} (n : ) (x : 𝕜) (k : ) :
deriv^[k] (λ (x : 𝕜), x ^ n) x = (finset.range k).prod (λ (i : ), n - i) * x ^ (n - k)
@[simp]
theorem iter_deriv_pow' {𝕜 : Type u} (n k : ) :
deriv^[k] (λ (x : 𝕜), x ^ n) = λ (x : 𝕜), (finset.range k).prod (λ (i : ), n - i) * x ^ (n - k)
theorem iter_deriv_inv {𝕜 : Type u} (k : ) (x : 𝕜) :
= (finset.range k).prod (λ (i : ), -1 - i) * x ^ (-1 - k)
@[simp]
theorem iter_deriv_inv' {𝕜 : Type u} (k : ) :
= λ (x : 𝕜), (finset.range k).prod (λ (i : ), -1 - i) * x ^ (-1 - k)
theorem differentiable_within_at.zpow {𝕜 : Type u} {E : Type v} [ E] {m : } {f : E 𝕜} {t : set E} {a : E} (hf : a) (h : f a 0 0 m) :
(λ (x : E), f x ^ m) t a
theorem differentiable_at.zpow {𝕜 : Type u} {E : Type v} [ E] {m : } {f : E 𝕜} {a : E} (hf : a) (h : f a 0 0 m) :
(λ (x : E), f x ^ m) a
theorem differentiable_on.zpow {𝕜 : Type u} {E : Type v} [ E] {m : } {f : E 𝕜} {t : set E} (hf : t) (h : ( (x : E), x t f x 0) 0 m) :
(λ (x : E), f x ^ m) t
theorem differentiable.zpow {𝕜 : Type u} {E : Type v} [ E] {m : } {f : E 𝕜} (hf : f) (h : ( (x : E), f x 0) 0 m) :
(λ (x : E), f x ^ m)