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