Weak Divergence Identity for the Inverse Hessian

This is the weak inverse-Hessian divergence identity, supporting the inverse-Hessian integration-by-parts route.

Let $u,F:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$. Assume:

1. $u$ is $C^1$ and has Lipschitz gradient.
2. $F$ is Lipschitz.
3. Almost everywhere,

$$\det(\operatorname{hessianMatrix}(u,x))=e^{F(x)}.$$

4. $\psi$ is Lipschitz and compactly supported.

For every $i<n$,

$$\sum_{j<n}\int H(x)^{-1}_{ij}\,D\psi(x)e_j\,dx =\sum_{j<n}\int H(x)^{-1}_{ij}\,DF(x)e_j\,\psi(x)\,dx,$$

where $H(x)=\operatorname{hessianMatrix}(u,x)$ and all integrals use Lebesgue measure. The statement does not assume pointwise positive definiteness of $H$; matrix inversion is the Lean matrix inverse and the determinant identity is only almost everywhere.

Original Lean declaration header

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

theorem sum_integral_inv_hessianMatrix_mul_fderiv_eq {n : ℕ}
    {u F : EuclideanSpace ℝ (Fin n) → ℝ} (hu : ContDiff ℝ 1 u) {G : NNReal}
    (hG : LipschitzWith G (gradient u)) {LF : NNReal} (hF : LipschitzWith LF F)
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (F x))
    {ψ : EuclideanSpace ℝ (Fin n) → ℝ} {Lψ : NNReal} (hψ : LipschitzWith Lψ ψ)
    (hψc : HasCompactSupport ψ) (i : Fin n) :
    ∑ j, ∫ x, (hessianMatrix u x)⁻¹ i j * fderiv ℝ ψ x (EuclideanSpace.basisFun (Fin n) ℝ j)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) =
      ∑ j, ∫ x, (hessianMatrix u x)⁻¹ i j * fderiv ℝ F x (EuclideanSpace.basisFun (Fin n) ℝ j) * ψ x
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/Matrix/Piola.

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

Supporting theorems: sum_integral_adjugate_hessianMatrix_mul_fderiv_eq_zero_of_lipschitz.

Previous: sum_integral_adjugate_hessianMatrix_mul_fderiv_eq_zero_of_lipschitz · Next: integrable_inv_hessianMatrix_mul_of_bounded_compact.

Source excerpt, lines 916–926 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Piola

open FunctionalInequalities.Probability.Stein
open MeasureTheory Set Filter

theorem FunctionalInequalities.Analysis.sum_integral_inv_hessianMatrix_mul_fderiv_eq_readable {n : ℕ}
    {u F : EuclideanSpace ℝ (Fin n) → ℝ} (hu : ContDiff ℝ 1 u) {G : NNReal}
    (hG : LipschitzWith G (gradient u)) {LF : NNReal} (hF : LipschitzWith LF F)
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (F x))
    {ψ : EuclideanSpace ℝ (Fin n) → ℝ} {Lψ : NNReal} (hψ : LipschitzWith Lψ ψ)
    (hψc : HasCompactSupport ψ) (i : Fin n) :
    ∑ j, ∫ x, (hessianMatrix u x)⁻¹ i j * fderiv ℝ ψ x (EuclideanSpace.basisFun (Fin n) ℝ j)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) =
      ∑ j, ∫ x, (hessianMatrix u x)⁻¹ i j * fderiv ℝ F x (EuclideanSpace.basisFun (Fin n) ℝ j) * ψ x
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) := by sorry