Derivative of (f x) ^ n, n : ℕ #
In this file we prove that (x ^ n)' = n * x ^ (n - 1), where n is a natural number.
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^n for n : ℕ #
theorem
hasStrictDerivAt_pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
(n : ℕ)
(x : 𝕜)
:
HasStrictDerivAt (fun (x : 𝕜) => x ^ n) (↑n * x ^ (n - 1)) x
theorem
hasDerivAt_pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
(n : ℕ)
(x : 𝕜)
:
HasDerivAt (fun (x : 𝕜) => x ^ n) (↑n * x ^ (n - 1)) x
theorem
hasDerivWithinAt_pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
(n : ℕ)
(x : 𝕜)
(s : Set 𝕜)
:
HasDerivWithinAt (fun (x : 𝕜) => x ^ n) (↑n * x ^ (n - 1)) s x
theorem
differentiableAt_pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
(n : ℕ)
:
DifferentiableAt 𝕜 (fun (x : 𝕜) => x ^ n) x
theorem
differentiableWithinAt_pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
(n : ℕ)
:
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => x ^ n) s x
theorem
differentiable_pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
(n : ℕ)
:
Differentiable 𝕜 fun (x : 𝕜) => x ^ n
theorem
differentiableOn_pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{s : Set 𝕜}
(n : ℕ)
:
DifferentiableOn 𝕜 (fun (x : 𝕜) => x ^ n) s
theorem
derivWithin_pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
(n : ℕ)
(hxs : UniqueDiffWithinAt 𝕜 s x)
:
theorem
HasDerivWithinAt.pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{c : 𝕜 → 𝕜}
{c' : 𝕜}
(n : ℕ)
(hc : HasDerivWithinAt c c' s x)
:
theorem
HasDerivAt.pow
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{c : 𝕜 → 𝕜}
{c' : 𝕜}
(n : ℕ)
(hc : HasDerivAt c c' x)
:
theorem
derivWithin_pow'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{c : 𝕜 → 𝕜}
(n : ℕ)
(hc : DifferentiableWithinAt 𝕜 c s x)
(hxs : UniqueDiffWithinAt 𝕜 s x)
:
derivWithin (fun (x : 𝕜) => c x ^ n) s x = ↑n * c x ^ (n - 1) * derivWithin c s x
@[simp]
theorem
deriv_pow''
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{c : 𝕜 → 𝕜}
(n : ℕ)
(hc : DifferentiableAt 𝕜 c x)
: