@[reducible, inline]

noncomputable abbrev hessian {X : Type u} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (f : X → ℝ) (x : X) : X →L[ℝ] X

The Hessian of f at x, viewed intrinsically as the derivative of the gradient map.

@[reducible, inline]

noncomputable abbrev hessianMatrix {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : Matrix (Fin n) (Fin n) ℝ

Definition 1.4.16: if f : ℝⁿ → ℝ, the Hessian of f at x is the matrix of the derivative of the gradient map in the standard orthonormal basis of ℝⁿ.

def Gradient.«term∇²» : Lean.ParserDescr

Definition 1.4.16: if f : ℝⁿ → ℝ, the Hessian of f at x is the matrix of the derivative of the gradient map in the standard orthonormal basis of ℝⁿ.

theorem hessianMatrix_apply {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) (i j : Fin n) : hessianMatrix f x i j = inner ℝ ((EuclideanSpace.basisFun (Fin n) ℝ) i) ((hessian f x) ((EuclideanSpace.basisFun (Fin n) ℝ) j))

The (i,j) entry of the Hessian matrix is the inner product of the ith standard basis vector with the Hessian operator applied to the jth standard basis vector.

theorem gradient_coordinate_eq_inner_basis {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (i : Fin n) : (fun (y : EuclideanSpace ℝ (Fin n)) => (gradient f y).ofLp i) = fun (y : EuclideanSpace ℝ (Fin n)) => inner ℝ ((EuclideanSpace.basisFun (Fin n) ℝ) i) (gradient f y)

Helper for Definition 1.4.16: the ith coordinate of the Euclidean gradient is the inner product with the ith standard basis vector.

theorem hasFDerivAt_gradient_coordinate {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) (i : Fin n) (hgrad : DifferentiableAt ℝ (gradient f) x) : HasFDerivAt (fun (y : EuclideanSpace ℝ (Fin n)) => (gradient f y).ofLp i) ((innerSL ℝ) ((EuclideanSpace.basisFun (Fin n) ℝ) i) ∘SL hessian f x) x

Helper for Definition 1.4.16: the derivative of a gradient coordinate is obtained by composing the Hessian operator with the corresponding coordinate functional.

theorem fderiv_gradient_coordinate_apply_basis {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) (i j : Fin n) (hgrad : DifferentiableAt ℝ (gradient f) x) : (fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin n)) => (gradient f y).ofLp i) x) ((EuclideanSpace.basisFun (Fin n) ℝ) j) = inner ℝ ((EuclideanSpace.basisFun (Fin n) ℝ) i) ((hessian f x) ((EuclideanSpace.basisFun (Fin n) ℝ) j))

Helper for Definition 1.4.16: evaluating the derivative of the ith gradient coordinate on the jth standard basis vector gives the corresponding Hessian inner-product entry.

theorem hessianMatrix_apply_eq_fderiv_gradient_coordinate {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) (i j : Fin n) (hgrad : DifferentiableAt ℝ (gradient f) x) : hessianMatrix f x i j = (fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin n)) => (gradient f y).ofLp i) x) ((EuclideanSpace.basisFun (Fin n) ℝ) j)

Under differentiability of the gradient at x, the (i,j) entry of the Hessian matrix is the derivative of the ith gradient coordinate in the jth standard basis direction, i.e. the textbook second partial derivative.

theorem hessianMatrix_toEuclideanLin {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : Matrix.toEuclideanLin (hessianMatrix f x) = ↑(hessian f x)

Turning the Hessian matrix back into its Euclidean linear action recovers the intrinsic Hessian operator.