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

• x ↦ ‖x‖ ^ p should be C^n for p > n.

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 : F → E} (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) ∘SL 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 : F → E} (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 : F → E} (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 enorm_fderiv_norm_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : F → E} (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 : F → E} (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 : F → E} (hf : Differentiable ℝ f) {p : ℝ} (hp : 1 < p) : Differentiable ℝ fun (x : F) => ‖f x‖ ^ p