The Hessian of the squared norm

The squared norm z ↦ ‖z‖ ^ 2 on a real inner product space is the model of a nondegenerate minimum. Its second derivative is the constant bilinear form 2 ⟪v, w⟫ (TauCeti.fderiv_fderiv_norm_sq_apply), so its Hessian quadratic form is v ↦ 2 * ‖v‖ ^ 2 at every point and its Morse index vanishes everywhere.

These are the real inputs for the Levi form and the inertia of the squared norm of a complex inner product space, the basic strictly plurisubharmonic function.

Main results

• TauCeti.hessianQuadraticForm_norm_sq: its Hessian quadratic form is 2 * ‖v‖ ^ 2.
• TauCeti.morseIndex_norm_sq: its Morse index vanishes at every point.

theorem TauCeti.hessianQuadraticForm_norm_sq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x v : F) : (hessianQuadraticForm (fun (z : F) => ‖z‖ ^ 2) x) v = 2 * ‖v‖ ^ 2

The Hessian quadratic form of the squared norm is v ↦ 2 * ‖v‖ ^ 2, at every point.

@[simp]

theorem TauCeti.morseIndex_norm_sq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (x : F) : morseIndex (fun (z : F) => ‖z‖ ^ 2) x = 0

The squared norm has Morse index zero at every point.