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 : 0s 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 : 𝕜) => (i, (m - i)) * x ^ (m - k)
theorem iter_deriv_zpow {𝕜 : Type u} (m : ) (x : 𝕜) (k : ) :
deriv^[k] (fun (y : 𝕜) => y ^ m) x = (i, (m - i)) * x ^ (m - k)
theorem iter_deriv_pow {𝕜 : Type u} (n : ) (x : 𝕜) (k : ) :
deriv^[k] (fun (x : 𝕜) => x ^ n) x = (i, (n - i)) * x ^ (n - k)
@[simp]
theorem iter_deriv_pow' {𝕜 : Type u} (n : ) (k : ) :
(deriv^[k] fun (x : 𝕜) => x ^ n) = fun (x : 𝕜) => (i, (n - i)) * x ^ (n - k)
theorem iter_deriv_inv {𝕜 : Type u} (k : ) (x : 𝕜) :
deriv^[k] Inv.inv x = (i, (-1 - i)) * x ^ (-1 - k)
@[simp]
theorem iter_deriv_inv' {𝕜 : Type u} (k : ) :
deriv^[k] Inv.inv = fun (x : 𝕜) => (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 : E) => 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 : E) => f x ^ m) a
theorem DifferentiableOn.zpow {𝕜 : Type u} {E : Type v} [] {m : } {f : E𝕜} {t : Set E} (hf : ) (h : (xt, f x 0) 0 m) :
DifferentiableOn 𝕜 (fun (x : E) => 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 : E) => f x ^ m