Derivative of (f x) ^ n, n : ℕ #
In this file we prove that the Fréchet derivative of fun x => f x ^ n,
where n is a natural number, is n * f x ^ (n - 1) * f'.
Additionally, we prove the case for non-commutative rings (with primed names like deriv_pow'),
where the result is instead ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i.
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
theorem
HasStrictDerivAt.fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
(h : HasStrictDerivAt f f' x)
(n : ℕ)
:
HasStrictDerivAt (fun (x : 𝕜) => f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x
theorem
HasStrictDerivAt.pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
(h : HasStrictDerivAt f f' x)
(n : ℕ)
:
HasStrictDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x
theorem
HasDerivWithinAt.fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
{s : Set 𝕜}
(h : HasDerivWithinAt f f' s x)
(n : ℕ)
:
HasDerivWithinAt (fun (x : 𝕜) => f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x
theorem
HasDerivWithinAt.pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
{s : Set 𝕜}
(h : HasDerivWithinAt f f' s x)
(n : ℕ)
:
HasDerivWithinAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x
theorem
HasDerivAt.fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
(h : HasDerivAt f f' x)
(n : ℕ)
:
HasDerivAt (fun (x : 𝕜) => f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x
theorem
HasDerivAt.pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
(h : HasDerivAt f f' x)
(n : ℕ)
:
HasDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x
@[simp]
theorem
derivWithin_fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{x : 𝕜}
{s : Set 𝕜}
(h : DifferentiableWithinAt 𝕜 f s x)
(n : ℕ)
:
derivWithin (fun (x : 𝕜) => f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i
@[simp]
theorem
derivWithin_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{x : 𝕜}
{s : Set 𝕜}
(h : DifferentiableWithinAt 𝕜 f s x)
(n : ℕ)
:
@[simp]
theorem
deriv_fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{x : 𝕜}
(h : DifferentiableAt 𝕜 f x)
(n : ℕ)
:
@[simp]
theorem
deriv_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{x : 𝕜}
(h : DifferentiableAt 𝕜 f x)
(n : ℕ)
:
theorem
HasStrictDerivAt.fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
(h : HasStrictDerivAt f f' x)
(n : ℕ)
:
theorem
HasStrictDerivAt.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
(h : HasStrictDerivAt f f' x)
(n : ℕ)
:
theorem
HasDerivWithinAt.fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
{s : Set 𝕜}
(h : HasDerivWithinAt f f' s x)
(n : ℕ)
:
theorem
HasDerivWithinAt.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
{s : Set 𝕜}
(h : HasDerivWithinAt f f' s x)
(n : ℕ)
:
theorem
HasDerivAt.fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
(h : HasDerivAt f f' x)
(n : ℕ)
:
theorem
HasDerivAt.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{f' : 𝔸}
{x : 𝕜}
(h : HasDerivAt f f' x)
(n : ℕ)
:
@[simp]
theorem
derivWithin_fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{x : 𝕜}
{s : Set 𝕜}
(h : DifferentiableWithinAt 𝕜 f s x)
(n : ℕ)
:
@[simp]
theorem
derivWithin_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{x : 𝕜}
{s : Set 𝕜}
(h : DifferentiableWithinAt 𝕜 f s x)
(n : ℕ)
:
@[simp]
theorem
deriv_fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{x : 𝕜}
(h : DifferentiableAt 𝕜 f x)
(n : ℕ)
:
@[simp]
theorem
deriv_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : 𝕜 → 𝔸}
{x : 𝕜}
(h : DifferentiableAt 𝕜 f x)
(n : ℕ)
:
@[deprecated deriv_fun_pow (since := "2025-07-16")]
theorem
deriv_fun_pow''
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{c : 𝕜 → 𝕜}
(n : ℕ)
(hc : DifferentiableAt 𝕜 c x)
:
@[deprecated deriv_pow (since := "2025-07-16")]
theorem
deriv_pow''
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{c : 𝕜 → 𝕜}
(n : ℕ)
(hc : DifferentiableAt 𝕜 c x)
:
theorem
hasStrictDerivAt_pow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
(n : ℕ)
(x : 𝕜)
:
HasStrictDerivAt (fun (x : 𝕜) => x ^ n) (↑n * x ^ (n - 1)) x
theorem
hasDerivWithinAt_pow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{s : Set 𝕜}
(n : ℕ)
(x : 𝕜)
:
HasDerivWithinAt (fun (x : 𝕜) => x ^ n) (↑n * x ^ (n - 1)) s x
theorem
hasDerivAt_pow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
(n : ℕ)
(x : 𝕜)
:
HasDerivAt (fun (x : 𝕜) => x ^ n) (↑n * x ^ (n - 1)) x
theorem
derivWithin_pow_field
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
(h : UniqueDiffWithinAt 𝕜 s x)
(n : ℕ)
: