# Documentation

Mathlib.Analysis.Calculus.Deriv.ZPow

# Derivatives of x ^ m, m : ℤ#

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 hasStrictDerivAt_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (h : x 0 0 m) :
HasStrictDerivAt (fun x => x ^ m) (m * x ^ (m - 1)) x
theorem hasDerivAt_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (h : x 0 0 m) :
HasDerivAt (fun x => x ^ m) (m * x ^ (m - 1)) x
theorem hasDerivWithinAt_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (h : x 0 0 m) (s : Set 𝕜) :
HasDerivWithinAt (fun x => x ^ m) (m * x ^ (m - 1)) s x
theorem differentiableAt_zpow {𝕜 : Type u} {x : 𝕜} {m : } :
DifferentiableAt 𝕜 (fun x => x ^ m) x x 0 0 m
theorem differentiableWithinAt_zpow {𝕜 : Type u} {s : Set 𝕜} (m : ) (x : 𝕜) (h : x 0 0 m) :
DifferentiableWithinAt 𝕜 (fun x => x ^ m) s x
theorem differentiableOn_zpow {𝕜 : Type u} (m : ) (s : Set 𝕜) (h : ¬0 s 0 m) :
DifferentiableOn 𝕜 (fun x => x ^ m) s
theorem deriv_zpow {𝕜 : Type u} (m : ) (x : 𝕜) :
deriv (fun x => x ^ m) x = m * x ^ (m - 1)
@[simp]
theorem deriv_zpow' {𝕜 : Type u} (m : ) :
(deriv fun x => x ^ m) = fun x => m * x ^ (m - 1)
theorem derivWithin_zpow {𝕜 : Type u} {x : 𝕜} {s : Set 𝕜} {m : } (hxs : ) (h : x 0 0 m) :
derivWithin (fun x => x ^ m) s x = m * x ^ (m - 1)
@[simp]
theorem iter_deriv_zpow' {𝕜 : Type u} (m : ) (k : ) :
(deriv^[k] fun x => x ^ m) = fun x => (Finset.prod () fun i => m - i) * x ^ (m - k)
theorem iter_deriv_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (k : ) :
(𝕜𝕜)^[deriv] k (fun y => y ^ m) x = (Finset.prod () fun i => m - i) * x ^ (m - k)
theorem iter_deriv_pow {𝕜 : Type u} (n : ) (x : 𝕜) (k : ) :
(𝕜𝕜)^[deriv] k (fun x => x ^ n) x = (Finset.prod () fun i => n - i) * x ^ (n - k)
@[simp]
theorem iter_deriv_pow' {𝕜 : Type u} (n : ) (k : ) :
(deriv^[k] fun x => x ^ n) = fun x => (Finset.prod () fun i => n - i) * x ^ (n - k)
theorem iter_deriv_inv {𝕜 : Type u} (k : ) (x : 𝕜) :
(𝕜𝕜)^[deriv] k Inv.inv x = (Finset.prod () fun i => -1 - i) * x ^ (-1 - k)
@[simp]
theorem iter_deriv_inv' {𝕜 : Type u} (k : ) :
deriv^[k] Inv.inv = fun x => (Finset.prod () fun i => -1 - i) * x ^ (-1 - k)
theorem DifferentiableWithinAt.zpow {𝕜 : Type u} {E : Type v} [] {m : } {f : E𝕜} {t : Set E} {a : E} (hf : ) (h : f a 0 0 m) :
DifferentiableWithinAt 𝕜 (fun x => f x ^ m) t a
theorem DifferentiableAt.zpow {𝕜 : Type u} {E : Type v} [] {m : } {f : E𝕜} {a : E} (hf : ) (h : f a 0 0 m) :
DifferentiableAt 𝕜 (fun x => f x ^ m) a
theorem DifferentiableOn.zpow {𝕜 : Type u} {E : Type v} [] {m : } {f : E𝕜} {t : Set E} (hf : ) (h : (∀ (x : E), x tf x 0) 0 m) :
DifferentiableOn 𝕜 (fun x => f x ^ m) t
theorem Differentiable.zpow {𝕜 : Type u} {E : Type v} [] {m : } {f : E𝕜} (hf : ) (h : (∀ (x : E), f x 0) 0 m) :
Differentiable 𝕜 fun x => f x ^ m