Documentation

Mathlib.Analysis.InnerProductSpace.NormPow

Properties about the powers of the norm #

In this file we prove that x ↦ ‖x‖ ^ p is continuously differentiable for an inner product space and for a real number p > 1.

TODO #

theorem hasFDerivAt_norm_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] (x : E) {p : } (hp : 1 < p) :
HasFDerivAt (fun (x : E) => x ^ p) ((p * x ^ (p - 2)) (innerSL ) x) x
theorem differentiable_norm_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {p : } (hp : 1 < p) :
Differentiable fun (x : E) => x ^ p
theorem hasDerivAt_norm_rpow (x : ) {p : } (hp : 1 < p) :
HasDerivAt (fun (x : ) => x ^ p) (p * x ^ (p - 2) * x) x
theorem hasDerivAt_abs_rpow (x : ) {p : } (hp : 1 < p) :
HasDerivAt (fun (x : ) => |x| ^ p) (p * |x| ^ (p - 2) * x) x
theorem fderiv_norm_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] (x : E) {p : } (hp : 1 < p) :
fderiv (fun (x : E) => x ^ p) x = (p * x ^ (p - 2)) (innerSL ) x
theorem Differentiable.fderiv_norm_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {f : FE} (hf : Differentiable f) {x : F} {p : } (hp : 1 < p) :
fderiv (fun (x : F) => f x ^ p) x = (p * f x ^ (p - 2)) ((innerSL ) (f x)).comp (fderiv f x)
theorem norm_fderiv_norm_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {f : FE} (hf : Differentiable f) {x : F} {p : } (hp : 1 < p) :
fderiv (fun (x : F) => f x ^ p) x p * f x ^ (p - 1) * fderiv f x
theorem norm_fderiv_norm_id_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] (x : E) {p : } (hp : 1 < p) :
fderiv (fun (x : E) => x ^ p) x = p * x ^ (p - 1)
theorem nnnorm_fderiv_norm_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {f : FE} (hf : Differentiable f) {x : F} {p : NNReal} (hp : 1 < p) :
fderiv (fun (x : F) => f x ^ p) x‖₊ p * f x‖₊ ^ (p - 1) * fderiv f x‖₊
theorem contDiff_norm_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {p : } (hp : 1 < p) :
ContDiff 1 fun (x : E) => x ^ p
theorem ContDiff.norm_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {f : FE} (hf : ContDiff 1 f) {p : } (hp : 1 < p) :
ContDiff 1 fun (x : F) => f x ^ p
theorem Differentiable.norm_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {f : FE} (hf : Differentiable f) {p : } (hp : 1 < p) :
Differentiable fun (x : F) => f x ^ p