Swapped Weak Generator Integration Identity

This formalizes the weak inverse-Hessian generator identity with the roles of the test functions exchanged.

Let $u,V,w,\eta:\mathbb R^n\to\mathbb R$. Assume: (1) $u,w\in C^1$, $\eta\in C^2$, and $\eta$ has compact support; (2) $\nabla u$ and $\nabla w$ are globally Lipschitz; (3) $V\in C^1$; (4) $-u+V\circ\nabla u$ is Lipschitz; and (5) almost everywhere,

Then, with all integrals over Lebesgue volume on $\mathbb R^n$,

This is a supporting weak integration-by-parts formula; it does not assert a KLS bound or additional regularity of $u$ or $w$.

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, w x * (((hessianMatrix u x)⁻¹ * hessianMatrix η x).trace -
        fderiv ℝ V (gradient u x) (gradient η 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, assemble_generator, smooth_test_derivative.

Previous: integral_mul_generator_eq_neg_energy · Next: integrable_weak_generator_densities.

Source excerpt, lines 798–811 · Frozen source 408915f.