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 Mathlib/Analysis/Calculus/Deriv/Basic.lean.

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 : 0 ∉ s ∨ 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 : 𝕜) => (∏ i ∈ Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)

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)

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)

@[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)

theorem iter_deriv_inv {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) (x : 𝕜) : deriv^[k] Inv.inv x = (-1) ^ k * ↑k.factorial * x ^ (-1 - ↑k)

@[simp]

theorem iter_deriv_inv' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) : deriv^[k] Inv.inv = fun (x : 𝕜) => (-1) ^ k * ↑k.factorial * x ^ (-1 - ↑k)

theorem iter_deriv_inv_linear {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) (c d : 𝕜) : (deriv^[k] fun (x : 𝕜) => (c * x + d)⁻¹) = fun (x : 𝕜) => (-1) ^ k * ↑k.factorial * c ^ k * (c * x + d) ^ (-1 - ↑k)

theorem iter_deriv_inv_linear_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] (k : ℕ) (c d : 𝕜) : (deriv^[k] fun (x : 𝕜) => (c * x - d)⁻¹) = fun (x : 𝕜) => (-1) ^ k * ↑k.factorial * c ^ k * (c * x - d) ^ (-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 : (∀ x ∈ t, 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