Piola Identity for Smooth Hessian Adjugates

This is the smooth Piola identity for Hessian adjugates.

Let $n\in\mathbb N$, let $u:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$ be $C^3$, and let $x$ be a point and $i<n$ a row index. If $H(y)=\operatorname{hessianMatrix}(u,y)$, then

where $e_j$ is the standard coordinate vector. The declaration sum_fderiv_adjugate_hessianMatrix_eq_zero_readable states that each row of the adjugate Hessian is divergence-free. It is the smooth input for later weak Piola identities.

Original Lean declaration header

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

theorem sum_fderiv_adjugate_hessianMatrix_eq_zero {n : ℕ} {u : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 3 u) (x : EuclideanSpace ℝ (Fin n)) (i : Fin n) :
    ∑ j, fderiv ℝ (fun y => (hessianMatrix u y).adjugate i j) x
      (EuclideanSpace.basisFun (Fin n) ℝ j) = 0

Module navigation

Module: Analysis/Matrix/Piola.

Definition modules: Analysis/BakryEmery/HessianOperator.

Supporting theorems: fderiv_det_updateRow.

Previous: fderiv_det_updateRow · Next: sum_integral_adjugate_hessianMatrix_mul_fderiv_eq_zero_of_lipschitz.

Source excerpt, lines 135–138 · Frozen source 408915f.