# 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

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem differentiableWithinAt_pow {𝕜 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] (n : ℕ) {x : 𝔸} {s : Set 𝔸} :
DifferentiableWithinAt 𝕜 (fun (x : 𝔸) => x ^ n) s x
source
@[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
source
@[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
source
theorem differentiableAt_pow {𝕜 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] (n : ℕ) {x : 𝔸} :
DifferentiableAt 𝕜 (fun (x : 𝔸) => x ^ n) x
source
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
source
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
source
theorem differentiableOn_pow {𝕜 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] (n : ℕ) {s : Set 𝔸} :
DifferentiableOn 𝕜 (fun (x : 𝔸) => x ^ n) s
source
@[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
source
@[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)
source
theorem differentiable_pow {𝕜 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] (n : ℕ) :
Differentiable 𝕜 fun (x : 𝔸) => x ^ n
source
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) :
fderiv 𝕜 (fun (x : E) => f x ^ n) x = ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • fderiv 𝕜 f x
source
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) :
fderiv 𝕜 (f ^ n) x = ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • fderiv 𝕜 f x
source
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 𝕜 𝔸
source
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
source
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
source
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 𝕜 𝔸
source
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 : ℕ) :
HasStrictFDerivAt (fun (x : E) => f x ^ n) ((n • f x ^ (n - 1)) • f') x
source
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
source
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 : ℕ) :
HasFDerivWithinAt (fun (x : E) => f x ^ n) ((n • f x ^ (n - 1)) • f') s x
source
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
source
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 : ℕ) :
HasFDerivAt (fun (x : E) => f x ^ n) ((n • f x ^ (n - 1)) • f') x
source
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
source
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) :
fderiv 𝕜 (fun (x : E) => f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x
source
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) :
fderiv 𝕜 (fun (x : E) => f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x
source
theorem fderiv_pow_ring {𝕜 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕜] [NormedCommRing 𝔸] [NormedAlgebra 𝕜 𝔸] {x : 𝔸} (n : ℕ) :
fderiv 𝕜 (fun (x : 𝔸) => x ^ n) x = (n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸
source
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) :
fderivWithin 𝕜 (fun (x : E) => f x ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x
source
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) :
fderivWithin 𝕜 (f ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x
source
theorem fderivWithin_pow_ring {𝕜 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕜] [NormedCommRing 𝔸] [NormedAlgebra 𝕜 𝔸] {s : Set 𝔸} {x : 𝔸} (n : ℕ) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun (x : 𝔸) => x ^ n) s x = (n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸