Quadratic Form of the Coordinate Hessian

This is a coordinate-identification lemma for the Hessian matrix.

Let $n\in\mathbb N$, let $\psi:\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))\to\mathbb R$, let $x$ be a point in that space, and let $v$ be a vector. The quadratic form associated with hessianMatrix ψ x satisfies

where the right-hand side is expressed in Lean as the iterated Fréchet derivative (fderiv ℝ (fderiv ℝ ψ) x) v v.

The lemma connects the coordinate Hessian representation used by the formalization with the second Fréchet derivative and is intended for later viscosity calculations.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

private lemma hessianMatrix_quadratic
    {n : ℕ} {ψ : EuclideanSpace ℝ (Fin n) → ℝ}
    {x : EuclideanSpace ℝ (Fin n)}
    (v : EuclideanSpace ℝ (Fin n)) :
    ⟪v, Matrix.toEuclideanLin (hessianMatrix ψ x) v⟫ =
      (fderiv ℝ (fderiv ℝ ψ) x) v v

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/BakryEmery/HessianOperator.

Previous: posSemidef_hessianMatrix_of_upper_touch · Next: local_taylor_two.

Source excerpt, lines 209–214 · Frozen source 408915f.