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 : ℤ #

source
theorem hasStrictDerivAt_zpow {𝕜 : Type u} [NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
HasStrictDerivAt (fun (x : 𝕜) => x ^ m) (↑m * x ^ (m - 1)) x
source
theorem hasDerivAt_zpow {𝕜 : Type u} [NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
HasDerivAt (fun (x : 𝕜) => x ^ m) (↑m * x ^ (m - 1)) x
source
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
source
theorem differentiableAt_zpow {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {m : ℤ} :
DifferentiableAt 𝕜 (fun (x : 𝕜) => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m
source
theorem differentiableWithinAt_zpow {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => x ^ m) s x
source
theorem differentiableOn_zpow {𝕜 : Type u} [NontriviallyNormedField 𝕜] (m : ℤ) (s : Set 𝕜) (h : 0 ∉ s ∨ 0 ≤ m) :
DifferentiableOn 𝕜 (fun (x : 𝕜) => x ^ m) s
source
theorem deriv_zpow {𝕜 : Type u} [NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜) :
deriv (fun (x : 𝕜) => x ^ m) x = ↑m * x ^ (m - 1)
source
@[simp]
theorem deriv_zpow' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (m : ℤ) :
(deriv fun (x : 𝕜) => x ^ m) = fun (x : 𝕜) => ↑m * x ^ (m - 1)
source
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)
source
@[simp]
theorem iter_deriv_zpow' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (m : ℤ) (k : ℕ) :
(deriv^[k] fun (x : 𝕜) => x ^ m) = fun (x : 𝕜) => (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
source
theorem iter_deriv_zpow {𝕜 : Type u} [NontriviallyNormedField 𝕜] (m : ℤ) (x : 𝕜) (k : ℕ) :
deriv^[k] (fun (y : 𝕜) => y ^ m) x = (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
source
theorem iter_deriv_pow {𝕜 : Type u} [NontriviallyNormedField 𝕜] (n : ℕ) (x : 𝕜) (k : ℕ) :
deriv^[k] (fun (x : 𝕜) => x ^ n) x = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)
source
@[simp]
theorem iter_deriv_pow' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (n : ℕ) (k : ℕ) :
(deriv^[k] fun (x : 𝕜) => x ^ n) = fun (x : 𝕜) => (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)
source
theorem iter_deriv_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) (x : 𝕜) :
deriv^[k] Inv.inv x = (∏ i ∈ Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k)
source
@[simp]
theorem iter_deriv_inv' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) :
deriv^[k] Inv.inv = fun (x : 𝕜) => (∏ i ∈ Finset.range k, (-1 - ↑i)) * x ^ (-1 - ↑k)
source
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
source
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
source
theorem DifferentiableOn.zpow {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {m : ℤ} {f : E → 𝕜} {t : Set E} (hf : DifferentiableOn 𝕜 f t) (h : (∀ x ∈ t, f x ≠ 0) ∨ 0 ≤ m) :
DifferentiableOn 𝕜 (fun (x : E) => f x ^ m) t
source
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