Integrability of Weak Inverse-Hessian Generator Densities

This is an integrability component related to Theorem 2.5 of Letwin (arXiv:2607.24164v1).

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

1. $u$ is continuous and has Lipschitz gradient;
2. $V$ is $C^1$;
3. $x\mapsto-u(x)+V(\nabla u(x))$ is continuous and, almost everywhere, $\det H_u(x)=e^{-u(x)+V(\nabla u(x))}$;
4. $w$ is continuous with Lipschitz gradient;
5. $\eta$ is $C^2$ and compactly supported.

Then each of the following is integrable with respect to volume:

$$\eta\left(\operatorname{tr}(H_u^{-1}H_w)-DV(\nabla u)(\nabla w)\right)e^{-u},$$ $$w\left(\operatorname{tr}(H_u^{-1}H_\eta)-DV(\nabla u)(\nabla\eta)\right)e^{-u},$$

and

$$\left|\eta+\operatorname{tr}(H_u^{-1}H_\eta)-DV(\nabla u)(\nabla\eta)\right|e^{-u}.$$

Here $H_u$ denotes hessianMatrix u; all determinant hypotheses are a.e. statements. The result establishes integrability needed for weak generator identities, not those identities themselves.

Original Lean declaration header

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

theorem integrable_weak_generator_densities {n : ℕ}
    {u V w η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : Continuous u) {G : NNReal} (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V)
    (hF : Continuous (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 : Continuous w) {Gw : NNReal} (hGw : LipschitzWith Gw (gradient w))
    (hη : ContDiff ℝ 2 η) (hηc : HasCompactSupport η) :
    Integrable (fun 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))) ∧
    Integrable (fun x => w x *
      (((hessianMatrix u x)⁻¹ * hessianMatrix η x).trace -
        fderiv ℝ V (gradient u x) (gradient η x)) * Real.exp (-u x))
      (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
    Integrable (fun x =>
      |η x + (((hessianMatrix u x)⁻¹ * hessianMatrix η x).trace -
        fderiv ℝ V (gradient u x) (gradient η x))| * 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, norm_hessianMatrix_entry_le_of_lipschitz_gradient.

Previous: integral_mul_generator_eq_neg_energy' · Next: hasWeakDerivAlong_inverse_hessian_of_logdet.

Source excerpt, lines 889–909 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_InverseHessian_Weak

open MeasureTheory Set Filter
open FunctionalInequalities.Probability.Stein

theorem FunctionalInequalities.Analysis.integrable_weak_generator_densities_readable {n : ℕ}
    {u V w η : EuclideanSpace ℝ (Fin n) → ℝ}
    (hu : Continuous u) {G : NNReal} (hG : LipschitzWith G (gradient u))
    (hV : ContDiff ℝ 1 V)
    (hF : Continuous (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 : Continuous w) {Gw : NNReal} (hGw : LipschitzWith Gw (gradient w))
    (hη : ContDiff ℝ 2 η) (hηc : HasCompactSupport η) :
    Integrable (fun 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))) ∧
    Integrable (fun x => w x *
      (((hessianMatrix u x)⁻¹ * hessianMatrix η x).trace -
        fderiv ℝ V (gradient u x) (gradient η x)) * Real.exp (-u x))
      (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
    Integrable (fun x =>
      |η x + (((hessianMatrix u x)⁻¹ * hessianMatrix η x).trace -
        fderiv ℝ V (gradient u x) (gradient η x))| * Real.exp (-u x))
      (volume : Measure (EuclideanSpace ℝ (Fin n))) := by sorry