Weak Symmetry of the Inverse-Hessian Generator

This formalizes the weak form of equation (2.2) in Letwin (arXiv:2607.24164v1), with a reviewed relation to Theorem 2.5.

Let $u,V,w,\eta$ be functions on $\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))$. Assume:

1. $u$ and $w$ are $C^1$;
2. $\nabla u$ and $\nabla w$ are Lipschitz;
3. $V$ is $C^1$;
4. $-u+V\circ\nabla u$ is Lipschitz;
5. almost everywhere,

$$\det(\operatorname{hessianMatrix}(u,x))=e^{-u(x)+V(\nabla u(x))};$$

6. $\eta$ is $C^2$ and compactly supported.

Then

$$\int \eta(x)\left(\operatorname{tr}\bigl(H_u(x)^{-1}H_w(x)\bigr)-DV(\nabla u(x))[\nabla w(x)]\right)e^{-u(x)}\,dx$$ $$=-\int\left(\sum_{i,j}(H_u(x)^{-1})_{ij}\,D\eta(x)[e_i]\,Dw(x)[e_j]\right)e^{-u(x)}\,dx.$$

The formula is an integration-by-parts identity for the weak inverse-Hessian generator. It uses ordinary Lebesgue integrals and an almost-everywhere determinant identity; it does not claim the main Hessian-energy estimate or any KLS bound.

Original Lean declaration header

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

theorem integral_mul_generator_eq_neg_energy {n : ℕ} {u V w η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) {G : NNReal} (hG : LipschitzWith G (gradient u)) (hV : ContDiff ℝ 1 V)
    {LF : NNReal} (hF : LipschitzWith LF (fun x => -u x + V (gradient u x)))
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (-u x + V (gradient u x)))
    (hw : ContDiff ℝ 1 w) {Gw : NNReal} (hGw : LipschitzWith Gw (gradient w))
    (hη : ContDiff ℝ 2 η) (hηc : HasCompactSupport η) :
    ∫ x, η x * (((hessianMatrix u x)⁻¹ * hessianMatrix w x).trace -
        fderiv ℝ V (gradient u x) (gradient w x)) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) =
      -∫ x, (∑ i, ∑ j, (hessianMatrix u x)⁻¹ i j *
          fderiv ℝ η x (EuclideanSpace.basisFun (Fin n) ℝ i) *
          fderiv ℝ w x (EuclideanSpace.basisFun (Fin n) ℝ j)) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/InverseHessian/Weak.

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

Supporting theorems: integrable_inv_hessianMatrix_mul_of_bounded_compact, exists_lipschitzWith_smul_of_locallyLipschitz, assemble_generator.

Previous: assemble_generator · Next: integral_mul_generator_eq_neg_energy'.

Source excerpt, lines 770–783 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_Weak

open MeasureTheory Set Filter
open FunctionalInequalities.Probability.Stein

theorem FunctionalInequalities.Analysis.integral_mul_generator_eq_neg_energy_readable {n : ℕ} {u V w η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : ContDiff ℝ 1 u) {G : NNReal} (hG : LipschitzWith G (gradient u)) (hV : ContDiff ℝ 1 V)
    {LF : NNReal} (hF : LipschitzWith LF (fun x => -u x + V (gradient u x)))
    (hdet : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      (hessianMatrix u x).det = Real.exp (-u x + V (gradient u x)))
    (hw : ContDiff ℝ 1 w) {Gw : NNReal} (hGw : LipschitzWith Gw (gradient w))
    (hη : ContDiff ℝ 2 η) (hηc : HasCompactSupport η) :
    ∫ x, η x * (((hessianMatrix u x)⁻¹ * hessianMatrix w x).trace -
        fderiv ℝ V (gradient u x) (gradient w x)) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) =
      -∫ x, (∑ i, ∑ j, (hessianMatrix u x)⁻¹ i j *
          fderiv ℝ η x (EuclideanSpace.basisFun (Fin n) ℝ i) *
          fderiv ℝ w x (EuclideanSpace.basisFun (Fin n) ℝ j)) * Real.exp (-u x)
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) := by sorry