Tilted Integration By Parts For Lipschitz Functions

This statement establishes weighted integration by parts for a bounded Lipschitz test.

Let n be a natural number, let U and η be functions on $E=\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n)$, and let L and Lη be nonnegative-real Lipschitz constants. Assume U is L-Lipschitz, η is Lη-Lipschitz, η is bounded by C in norm, and

For every v∈E, both directional derivatives are integrable with respect to $d\nu=e^{-U}dx$, namely $D_vη$ and $ηD_vU$, and

This is a reusable first-order integration-by-parts identity for normalized exponential tilts in finite dimensions.

Formalization Note The functions are only assumed globally Lipschitz; the derivatives are Fréchet derivatives where represented by fderiv, and the tilted measure uses the potential −U.

Original Lean declaration header

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

theorem integral_fderiv_tilted_eq_integral_mul_fderiv_of_bounded_lipschitz {n : ℕ}
    {U eta : EuclideanSpace ℝ (Fin n) → ℝ} {L Leta : NNReal}
    (hU : LipschitzWith L U) (heta : LipschitzWith Leta eta)
    (C : ℝ) (hbound : ∀ x, ‖eta x‖ ≤ C)
    (hnorm : (∫ x, Real.exp (-U x) ∂volume) = 1)
    (v : EuclideanSpace ℝ (Fin n)) :
    Integrable (fun x => fderiv ℝ eta x v) ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U)) ∧
    Integrable (fun x => eta x * fderiv ℝ U x v) ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U)) ∧
    (∫ x, fderiv ℝ eta x v ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U))) =
      ∫ x, eta x * fderiv ℝ U x v ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/LipschitzHessian.

Supporting theorems: HasWeakDerivAlong.mul_of_locally_bounded, hasWeakDerivAlong_exp_neg_of_lipschitz, hasWeakDerivAlong_of_lipschitz, integral_eq_zero_of_integrable_weak_derivative.

Previous: integral_inner_fderiv_gradient_tilted_eq_integral_fderiv_mul.

Source excerpt, lines 238–247 · Frozen source 408915f.