Fréchet 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 fderiv_pow'),
where the result is instead ∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i.
For detailed documentation of the Fréchet derivative,
see the module docstring of Mathlib/Analysis/Calculus/FDeriv/Basic.lean.
Keywords #
derivative, power
theorem
HasStrictFDerivAt.fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
(h : HasStrictFDerivAt f f' x)
(n : ℕ)
:
HasStrictFDerivAt (fun (x : E) => f x ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') x
theorem
HasStrictFDerivAt.pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
(h : HasStrictFDerivAt f f' x)
(n : ℕ)
:
HasStrictFDerivAt (f ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') x
theorem
hasStrictFDerivAt_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{x : 𝔸}
:
HasStrictFDerivAt (fun (x : 𝔸) => x ^ n)
(∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸) x
theorem
HasFDerivWithinAt.fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
{s : Set E}
(h : HasFDerivWithinAt f f' s x)
(n : ℕ)
:
HasFDerivWithinAt (fun (x : E) => f x ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') s
x
theorem
HasFDerivWithinAt.pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
{s : Set E}
(h : HasFDerivWithinAt f f' s x)
(n : ℕ)
:
HasFDerivWithinAt (f ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') s x
theorem
hasFDerivWithinAt_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{x : 𝔸}
{s : Set 𝔸}
:
HasFDerivWithinAt (fun (x : 𝔸) => x ^ n)
(∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸) s x
theorem
HasFDerivAt.fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
(h : HasFDerivAt f f' x)
(n : ℕ)
:
HasFDerivAt (fun (x : E) => f x ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') x
theorem
HasFDerivAt.pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
(h : HasFDerivAt f f' x)
(n : ℕ)
:
HasFDerivAt (f ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') x
theorem
hasFDerivAt_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{x : 𝔸}
:
HasFDerivAt (fun (x : 𝔸) => x ^ n)
(∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸) x
theorem
DifferentiableWithinAt.fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
{s : Set E}
(hf : DifferentiableWithinAt 𝕜 f s x)
(n : ℕ)
:
DifferentiableWithinAt 𝕜 (fun (x : E) => f x ^ n) s x
theorem
DifferentiableWithinAt.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
{s : Set E}
(hf : DifferentiableWithinAt 𝕜 f s x)
(n : ℕ)
:
DifferentiableWithinAt 𝕜 (f ^ n) s x
theorem
differentiableWithinAt_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{x : 𝔸}
{s : Set 𝔸}
:
DifferentiableWithinAt 𝕜 (fun (x : 𝔸) => x ^ n) s x
@[simp]
theorem
DifferentiableAt.fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
(hf : DifferentiableAt 𝕜 f x)
(n : ℕ)
:
DifferentiableAt 𝕜 (fun (x : E) => f x ^ n) x
@[simp]
theorem
DifferentiableAt.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
(hf : DifferentiableAt 𝕜 f x)
(n : ℕ)
:
DifferentiableAt 𝕜 (f ^ n) x
theorem
differentiableAt_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{x : 𝔸}
:
DifferentiableAt 𝕜 (fun (x : 𝔸) => x ^ n) x
theorem
DifferentiableOn.fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{s : Set E}
(hf : DifferentiableOn 𝕜 f s)
(n : ℕ)
:
DifferentiableOn 𝕜 (fun (x : E) => f x ^ n) s
theorem
DifferentiableOn.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{s : Set E}
(hf : DifferentiableOn 𝕜 f s)
(n : ℕ)
:
DifferentiableOn 𝕜 (f ^ n) s
theorem
differentiableOn_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{s : Set 𝔸}
:
DifferentiableOn 𝕜 (fun (x : 𝔸) => x ^ n) s
@[simp]
theorem
Differentiable.fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
(hf : Differentiable 𝕜 f)
(n : ℕ)
:
Differentiable 𝕜 fun (x : E) => f x ^ n
@[simp]
theorem
Differentiable.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
(hf : Differentiable 𝕜 f)
(n : ℕ)
:
Differentiable 𝕜 (f ^ n)
theorem
differentiable_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
:
Differentiable 𝕜 fun (x : 𝔸) => x ^ n
theorem
fderiv_fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
(n : ℕ)
(hf : DifferentiableAt 𝕜 f x)
:
theorem
fderiv_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
(n : ℕ)
(hf : DifferentiableAt 𝕜 f x)
:
theorem
fderiv_pow_ring'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{x : 𝔸}
(n : ℕ)
:
fderiv 𝕜 (fun (x : 𝔸) => x ^ n) x = ∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸
theorem
fderivWithin_fun_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
{s : Set E}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(n : ℕ)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
fderivWithin 𝕜 (fun (x : E) => f x ^ n) s x = ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • fderivWithin 𝕜 f s x
theorem
fderivWithin_pow'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
{s : Set E}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(n : ℕ)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
fderivWithin 𝕜 (f ^ n) s x = ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • fderivWithin 𝕜 f s x
theorem
fderivWithin_pow_ring'
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{s : Set 𝔸}
{x : 𝔸}
(n : ℕ)
(hxs : UniqueDiffWithinAt 𝕜 s x)
:
fderivWithin 𝕜 (fun (x : 𝔸) => x ^ n) s x = ∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸
theorem
HasStrictFDerivAt.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
(h : HasStrictFDerivAt f f' x)
(n : ℕ)
:
theorem
hasStrictFDerivAt_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{x : 𝔸}
:
HasStrictFDerivAt (fun (x : 𝔸) => x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) x
theorem
HasFDerivWithinAt.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
{s : Set E}
(h : HasFDerivWithinAt f f' s x)
(n : ℕ)
:
theorem
hasFDerivWithinAt_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{x : 𝔸}
{s : Set 𝔸}
:
HasFDerivWithinAt (fun (x : 𝔸) => x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) s x
theorem
HasFDerivAt.pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{f' : E →L[𝕜] 𝔸}
{x : E}
(h : HasFDerivAt f f' x)
(n : ℕ)
:
theorem
hasFDerivAt_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
(n : ℕ)
{x : 𝔸}
:
HasFDerivAt (fun (x : 𝔸) => x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) x
theorem
fderiv_fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
(n : ℕ)
(hf : DifferentiableAt 𝕜 f x)
:
theorem
fderiv_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
(n : ℕ)
(hf : DifferentiableAt 𝕜 f x)
:
theorem
fderiv_pow_ring
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{x : 𝔸}
(n : ℕ)
:
theorem
fderivWithin_fun_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
{s : Set E}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(n : ℕ)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
theorem
fderivWithin_pow
{𝕜 : Type u_1}
{𝔸 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAddCommGroup E]
[NormedAlgebra 𝕜 𝔸]
[NormedSpace 𝕜 E]
{f : E → 𝔸}
{x : E}
{s : Set E}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(n : ℕ)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
theorem
fderivWithin_pow_ring
{𝕜 : Type u_1}
{𝔸 : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedCommRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{s : Set 𝔸}
{x : 𝔸}
(n : ℕ)
(hxs : UniqueDiffWithinAt 𝕜 s x)
: