Differentiability of the norm in a real normed vector space

This file provides basic results about the differentiability of the norm in a real vector space. Most are of the following kind: if the norm has some differentiability property (DifferentiableAt, ContDiffAt, HasStrictFDerivAt, HasFDerivAt) at x, then so it has at t • x when t ≠ 0.

Main statements

• ContDiffAt.contDiffAt_norm_smul: If the norm is continuously differentiable up to order n at x, then so it is at t • x when t ≠ 0.
• differentiableAt_norm_smul: If t ≠ 0, the norm is differentiable at x if and only if it is at t • x.
• HasFDerivAt.hasFDerivAt_norm_smul: If the norm has a Fréchet derivative f at x and t ≠ 0, then it has (SignType t) • f as a Fréchet derivative at t · x.
• fderiv_norm_smul : fderiv ℝ (‖·‖) (t • x) = (SignType.sign t : ℝ) • (fderiv ℝ (‖·‖) x), this holds without any differentiability assumptions.
• DifferentiableAt.fderiv_norm_self: if the norm is differentiable at x, then fderiv ℝ (‖·‖) x x = ‖x‖.
• norm_fderiv_norm: if the norm is differentiable at x then the operator norm of its derivative is 1 (on a non trivial space).

Tags

differentiability, norm

theorem not_differentiableAt_norm_zero (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] : ¬DifferentiableAt ℝ (fun (x : E) => ‖x‖) 0

theorem ContDiffAt.contDiffAt_norm_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {x : E} {t : ℝ} (ht : t ≠ 0) (h : ContDiffAt ℝ n (fun (x : E) => ‖x‖) x) : ContDiffAt ℝ n (fun (x : E) => ‖x‖) (t • x)

theorem contDiffAt_norm_smul_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {x : E} {t : ℝ} (ht : t ≠ 0) : ContDiffAt ℝ n (fun (x : E) => ‖x‖) x ↔ ContDiffAt ℝ n (fun (x : E) => ‖x‖) (t • x)

theorem ContDiffAt.contDiffAt_norm_of_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {x : E} {t : ℝ} (h : ContDiffAt ℝ n (fun (x : E) => ‖x‖) (t • x)) : ContDiffAt ℝ n (fun (x : E) => ‖x‖) x

theorem HasStrictFDerivAt.hasStrictFDerivAt_norm_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E →L[ℝ] ℝ} {x : E} {t : ℝ} (ht : t ≠ 0) (h : HasStrictFDerivAt (fun (x : E) => ‖x‖) f x) : HasStrictFDerivAt (fun (x : E) => ‖x‖) (↑(SignType.sign t) • f) (t • x)

theorem HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E →L[ℝ] ℝ} {x : E} {t : ℝ} (ht : t < 0) (h : HasStrictFDerivAt (fun (x : E) => ‖x‖) f x) : HasStrictFDerivAt (fun (x : E) => ‖x‖) (-f) (t • x)

theorem HasStrictFDerivAt.hasStrictDerivAt_norm_smul_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E →L[ℝ] ℝ} {x : E} {t : ℝ} (ht : 0 < t) (h : HasStrictFDerivAt (fun (x : E) => ‖x‖) f x) : HasStrictFDerivAt (fun (x : E) => ‖x‖) f (t • x)

theorem HasFDerivAt.hasFDerivAt_norm_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E →L[ℝ] ℝ} {x : E} {t : ℝ} (ht : t ≠ 0) (h : HasFDerivAt (fun (x : E) => ‖x‖) f x) : HasFDerivAt (fun (x : E) => ‖x‖) (↑(SignType.sign t) • f) (t • x)

theorem HasFDerivAt.hasFDerivAt_norm_smul_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E →L[ℝ] ℝ} {x : E} {t : ℝ} (ht : t < 0) (h : HasFDerivAt (fun (x : E) => ‖x‖) f x) : HasFDerivAt (fun (x : E) => ‖x‖) (-f) (t • x)

theorem HasFDerivAt.hasFDerivAt_norm_smul_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E →L[ℝ] ℝ} {x : E} {t : ℝ} (ht : 0 < t) (h : HasFDerivAt (fun (x : E) => ‖x‖) f x) : HasFDerivAt (fun (x : E) => ‖x‖) f (t • x)

theorem differentiableAt_norm_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {t : ℝ} (ht : t ≠ 0) : DifferentiableAt ℝ (fun (x : E) => ‖x‖) x ↔ DifferentiableAt ℝ (fun (x : E) => ‖x‖) (t • x)

theorem DifferentiableAt.differentiableAt_norm_of_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {t : ℝ} (h : DifferentiableAt ℝ (fun (x : E) => ‖x‖) (t • x)) : DifferentiableAt ℝ (fun (x : E) => ‖x‖) x

theorem DifferentiableAt.fderiv_norm_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} (h : DifferentiableAt ℝ (fun (x : E) => ‖x‖) x) : (fderiv ℝ (fun (x : E) => ‖x‖) x) x = ‖x‖

theorem fderiv_norm_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) (t : ℝ) : fderiv ℝ (fun (x : E) => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun (x : E) => ‖x‖) x

theorem fderiv_norm_smul_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {t : ℝ} (ht : 0 < t) : fderiv ℝ (fun (x : E) => ‖x‖) (t • x) = fderiv ℝ (fun (x : E) => ‖x‖) x

theorem fderiv_norm_smul_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {t : ℝ} (ht : t < 0) : fderiv ℝ (fun (x : E) => ‖x‖) (t • x) = -fderiv ℝ (fun (x : E) => ‖x‖) x

theorem norm_fderiv_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} [Nontrivial E] (h : DifferentiableAt ℝ (fun (x : E) => ‖x‖) x) : ‖fderiv ℝ (fun (x : E) => ‖x‖) x‖ = 1