feat: basic results about the differentiability of the norm

[EtienneC30]

Provide basic results about the differentiability of the norm in a real vector space.
Give the links between differentiability as x and t • x.
Prove that if the norm is differentiable at x then fderiv ℝ (‖·‖) x x = ‖x‖ and ‖fderiv ℝ (‖·‖) x‖ = 1.

---

• depends on: [Merged by Bors] - feat: derivative of absolute value #17149

[github-actions]

PR summary a25518b084

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Calculus.FDeriv.Norm	1934

---

Declarations diff

+ ContDiffAt.contDiffAt_norm_of_smul
+ ContDiffAt.contDiffAt_norm_smul
+ DifferentiableAt.differentiableAt_norm_of_smul
+ DifferentiableAt.fderiv_norm_self
+ HasFDerivAt.hasFDerivAt_norm_smul
+ HasFDerivAt.hasFDerivAt_norm_smul_neg
+ HasFDerivAt.hasFDerivAt_norm_smul_pos
+ HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg
+ HasStrictFDerivAt.hasStrictDerivAt_norm_smul_pos
+ HasStrictFDerivAt.hasStrictFDerivAt_norm_smul
+ ae_differentiableAt_norm
+ contDiffAt_norm_smul_iff
+ differentiableAt_norm_smul
+ fderiv_norm_smul
+ fderiv_norm_smul_neg
+ fderiv_norm_smul_pos
+ norm_fderiv_norm
+ not_differentiableAt_norm_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: derivative of absolute value #17149
  By Dependent Issues (🤖). Happy coding!