Weak Integration By Parts For The Weighted Laplacian

This formalizes part of Lemma A.6 of Letwin (arXiv:2607.24164v1), whose reviewed paper statement is the Brascamp–Lieb inequality for the tilted law.

Let n be a natural number and work on $E=\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n)$. Let U be C¹, let v be smooth, and assume v has compact support. Normalize the exponential weight by

$$\int_E e^{-U(x)}\,dx=1.$$

Let η be locally integrable and globally bounded by C in norm. For each coordinate i, suppose η has weak derivative aᵢ along the i-th Euclidean basis direction, and suppose every aᵢ belongs locally to $L^2$ on compact sets. Then both functions

$$x\mapsto \eta(x)\,\mathcal L_Uv(x)$$

and

$$x\mapsto\sum_i a_i(x)\,D_{e_i}v(x)$$

are integrable with respect to the tilted measure $d\nu=e^{-U}dx$, and

$$\int \eta\,\mathcal L_Uv\,d\nu=-\int\sum_i a_iD_{e_i}v\,d\nu.$$

Here $\mathcal L_Uv=\Delta v-\langle\nabla U,\nabla v\rangle$ is the ordinary weighted Laplacian.

The declaration is a rough integration-by-parts tool for compactly supported tests and weakly differentiable bounded multipliers.

Formalization Note The conclusion is stated for all n, including n=0; the tilted measure is formed from volume measure and the function −U.

Original Lean declaration header

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

theorem integral_bounded_weak_mul_weightedLaplacian_of_contDiff_one {n : ℕ}
    {U v eta : EuclideanSpace ℝ (Fin n) → ℝ}
    (hU : ContDiff ℝ 1 U) (hv : ContDiff ℝ ∞ v) (hvc : HasCompactSupport v)
    (hnorm : (∫ x, Real.exp (-U x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) = 1)
    (a : Fin n → EuclideanSpace ℝ (Fin n) → ℝ) (C : ℝ)
    (heta : LocallyIntegrable eta (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hbound : ∀ x, ‖eta x‖ ≤ C)
    (hweak : ∀ i : Fin n, HasWeakDerivAlong eta (a i) (EuclideanSpace.basisFun (Fin n) ℝ i))
    (ha2 : ∀ i : Fin n, ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp (a i) 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) :
    Integrable (fun x => eta x * weightedLaplacian U v x)
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U)) ∧
    Integrable (fun x => ∑ i : Fin n, a i x *
      fderiv ℝ v x (EuclideanSpace.basisFun (Fin n) ℝ i))
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U)) ∧
    (∫ x, eta x * weightedLaplacian U v x
      ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U))) =
      -(∫ x, (∑ i : Fin n, a i x * fderiv ℝ v x (EuclideanSpace.basisFun (Fin n) ℝ i))
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U)))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/WeakLaplacian.

Definition modules: Analysis/BakryEmery/Laplacian, Analysis/WeakDerivative/Basic.

Supporting theorems: integral_compact_flux_eq_neg_forcing_of_global_bounded_weak_test.

Source excerpt, lines 25–43 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_IntegrationByParts_WeakLaplacian

open MeasureTheory Filter Set Metric
open scoped ContDiff Topology RealInnerProductSpace
open FunctionalInequalities.Analysis.BakryEmery
set_option maxHeartbeats 1000000

theorem FunctionalInequalities.Analysis.integral_bounded_weak_mul_weightedLaplacian_of_contDiff_one_readable {n : ℕ}
    {U v eta : EuclideanSpace ℝ (Fin n) → ℝ}
    (hU : ContDiff ℝ 1 U) (hv : ContDiff ℝ ∞ v) (hvc : HasCompactSupport v)
    (hnorm : (∫ x, Real.exp (-U x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) = 1)
    (a : Fin n → EuclideanSpace ℝ (Fin n) → ℝ) (C : ℝ)
    (heta : LocallyIntegrable eta (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hbound : ∀ x, ‖eta x‖ ≤ C)
    (hweak : ∀ i : Fin n, HasWeakDerivAlong eta (a i) (EuclideanSpace.basisFun (Fin n) ℝ i))
    (ha2 : ∀ i : Fin n, ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
      MemLp (a i) 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)) :
    Integrable (fun x => eta x * weightedLaplacian U v x)
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U)) ∧
    Integrable (fun x => ∑ i : Fin n, a i x *
      fderiv ℝ v x (EuclideanSpace.basisFun (Fin n) ℝ i))
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U)) ∧
    (∫ x, eta x * weightedLaplacian U v x
      ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U))) =
      -(∫ x, (∑ i : Fin n, a i x * fderiv ℝ v x (EuclideanSpace.basisFun (Fin n) ℝ i))
        ∂((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U))) := by sorry