mathlib3 documentation

analysis.calculus.deriv.zpow

Derivatives of x ^ m, m : ℤ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 has_strict_deriv_at_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (m : ) (x : 𝕜) (h : x 0 0 m) :
has_strict_deriv_at (λ (x : 𝕜), x ^ m) (m * x ^ (m - 1)) x
theorem has_deriv_at_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (m : ) (x : 𝕜) (h : x 0 0 m) :
has_deriv_at (λ (x : 𝕜), x ^ m) (m * x ^ (m - 1)) x
theorem has_deriv_within_at_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (m : ) (x : 𝕜) (h : x 0 0 m) (s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), x ^ m) (m * x ^ (m - 1)) s x
theorem differentiable_at_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {m : } :
differentiable_at 𝕜 (λ (x : 𝕜), x ^ m) x x 0 0 m
theorem differentiable_within_at_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {s : set 𝕜} (m : ) (x : 𝕜) (h : x 0 0 m) :
differentiable_within_at 𝕜 (λ (x : 𝕜), x ^ m) s x
theorem differentiable_on_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (m : ) (s : set 𝕜) (h : 0 s 0 m) :
differentiable_on 𝕜 (λ (x : 𝕜), x ^ m) s
theorem deriv_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (m : ) (x : 𝕜) :
deriv (λ (x : 𝕜), x ^ m) x = m * x ^ (m - 1)
@[simp]
theorem deriv_zpow' {𝕜 : Type u} [nontrivially_normed_field 𝕜] (m : ) :
deriv (λ (x : 𝕜), x ^ m) = λ (x : 𝕜), m * x ^ (m - 1)
theorem deriv_within_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} {m : } (hxs : unique_diff_within_at 𝕜 s x) (h : x 0 0 m) :
deriv_within (λ (x : 𝕜), x ^ m) s x = m * x ^ (m - 1)
@[simp]
theorem iter_deriv_zpow' {𝕜 : Type u} [nontrivially_normed_field 𝕜] (m : ) (k : ) :
deriv^[k] (λ (x : 𝕜), x ^ m) = λ (x : 𝕜), (finset.range k).prod (λ (i : ), m - i) * x ^ (m - k)
theorem iter_deriv_zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (m : ) (x : 𝕜) (k : ) :
deriv^[k] (λ (y : 𝕜), y ^ m) x = (finset.range k).prod (λ (i : ), m - i) * x ^ (m - k)
theorem iter_deriv_pow {𝕜 : Type u} [nontrivially_normed_field 𝕜] (n : ) (x : 𝕜) (k : ) :
deriv^[k] (λ (x : 𝕜), x ^ n) x = (finset.range k).prod (λ (i : ), n - i) * x ^ (n - k)
@[simp]
theorem iter_deriv_pow' {𝕜 : Type u} [nontrivially_normed_field 𝕜] (n k : ) :
deriv^[k] (λ (x : 𝕜), x ^ n) = λ (x : 𝕜), (finset.range k).prod (λ (i : ), n - i) * x ^ (n - k)
theorem iter_deriv_inv {𝕜 : Type u} [nontrivially_normed_field 𝕜] (k : ) (x : 𝕜) :
deriv^[k] has_inv.inv x = (finset.range k).prod (λ (i : ), -1 - i) * x ^ (-1 - k)
@[simp]
theorem iter_deriv_inv' {𝕜 : Type u} [nontrivially_normed_field 𝕜] (k : ) :
deriv^[k] has_inv.inv = λ (x : 𝕜), (finset.range k).prod (λ (i : ), -1 - i) * x ^ (-1 - k)
theorem differentiable_within_at.zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {E : Type v} [normed_add_comm_group E] [normed_space 𝕜 E] {m : } {f : E 𝕜} {t : set E} {a : E} (hf : differentiable_within_at 𝕜 f t a) (h : f a 0 0 m) :
differentiable_within_at 𝕜 (λ (x : E), f x ^ m) t a
theorem differentiable_at.zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {E : Type v} [normed_add_comm_group E] [normed_space 𝕜 E] {m : } {f : E 𝕜} {a : E} (hf : differentiable_at 𝕜 f a) (h : f a 0 0 m) :
differentiable_at 𝕜 (λ (x : E), f x ^ m) a
theorem differentiable_on.zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {E : Type v} [normed_add_comm_group E] [normed_space 𝕜 E] {m : } {f : E 𝕜} {t : set E} (hf : differentiable_on 𝕜 f t) (h : ( (x : E), x t f x 0) 0 m) :
differentiable_on 𝕜 (λ (x : E), f x ^ m) t
theorem differentiable.zpow {𝕜 : Type u} [nontrivially_normed_field 𝕜] {E : Type v} [normed_add_comm_group E] [normed_space 𝕜 E] {m : } {f : E 𝕜} (hf : differentiable 𝕜 f) (h : ( (x : E), f x 0) 0 m) :
differentiable 𝕜 (λ (x : E), f x ^ m)