Hessian of a Quadratic Test Function

Let $A$ be a Hermitian real matrix indexed by $\mathrm{Fin}\ n$, let $x_0,b\in\mathbb R^n$, let $c\in\mathbb R$, and let $x\in\mathbb R^n$. For the quadratic test function quadraticAt A x₀ b c, its coordinate Hessian is constant:

This identity is pointwise in $x$ and is used to identify Hessians of quadratic touching functions.

Original Lean declaration header

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

theorem hessianMatrix_quadraticAt {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsHermitian)
    (x₀ b : EuclideanSpace ℝ (Fin n)) (c : ℝ) (x : EuclideanSpace ℝ (Fin n)) :
    hessianMatrix (quadraticAt A x₀ b c) x = A

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/Convex/Alexandrov, Analysis/BakryEmery/HessianOperator, Analysis/Operator/Coordinates.

Previous: det_hessianMatrix_le_of_lower_touch · Next: posDef_and_det_eq_of_quadratic_expansion.

Source excerpt, lines 833–835 · Frozen source 408915f.