Derivatives and norms

A map whose norm is locally constant has derivative orthogonal to its value. In particular, the derivative of a map into a sphere is tangent to the sphere. Away from the origin, a vanishing derivative of a norm-composition forces the one-dimensional profile derivative to vanish.

theorem TauCeti.deriv_eq_zero_of_fderiv_comp_norm_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : ℝ → ℝ} {x : E} (hx : x ≠ 0) (hcrit : fderiv ℝ (fun (y : E) => v ‖y‖) x = 0) : deriv v ‖x‖ = 0

Away from the origin, a vanishing totalized derivative of a radial function forces its one-dimensional profile derivative to vanish. The profile need not be differentiable.

theorem TauCeti.inner_fderiv_eq_zero_of_eventually_norm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ψ : E → F} {w : E} (hψ : ∀ᶠ (y : E) in nhds w, ‖ψ y‖ = ‖ψ w‖) (u : E) : inner ℝ (ψ w) ((fderiv ℝ ψ w) u) = 0

A map whose norm is constant near w has Fréchet derivative at w orthogonal to its value. In particular, the derivative of a map into a sphere is tangent to the sphere. At nondifferentiable points, the Fréchet derivative is zero by definition.

theorem TauCeti.hasFDerivAt_norm_sq_sub {G : Type u_3} [NormedAddCommGroup G] [InnerProductSpace ℝ G] (x₀ x : G) : HasFDerivAt (fun (y : G) => ‖y - x₀‖ ^ 2) (2 • (innerSL ℝ) (x - x₀)) x

The Fréchet derivative of y ↦ ‖y - x₀‖ ^ 2 at x is 2 • innerSL ℝ (x - x₀).