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) :
theorem
has_deriv_at_zpow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(m : ℤ)
(x : 𝕜)
(h : x ≠ 0 ∨ 0 ≤ m) :
theorem
has_deriv_within_at_zpow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(m : ℤ)
(x : 𝕜)
(h : x ≠ 0 ∨ 0 ≤ m)
(s : set 𝕜) :
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_within_zpow
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{m : ℤ}
(hxs : unique_diff_within_at 𝕜 s x)
(h : x ≠ 0 ∨ 0 ≤ m) :
@[simp]
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)