Weak Compact Variational Estimate

This formalizes part of Lemma A.6 of Letwin (arXiv:2607.24164v1), cited as “Brascamp–Lieb for $\nu$.”

Work on $E=\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$. Let $\nu$ be a probability measure and $U,\eta,v:E\to\mathbb R$. Assume:

1. $\nu=e^{-U}\,dx$ in the Lean tilted-measure sense;
2. $U$ is $C^1$, globally Lipschitz, has Lipschitz gradient, and $\int e^{-U}\,dx=1$;
3. $\nabla^2U(x)$ is positive definite for almost every $x$;
4. $a_i:E\to\mathbb R$ are weak coordinate derivatives of the locally integrable, globally bounded function $\eta$, with $\|\eta(x)\|\le C$;
5. each $a_i$ is locally $L^2$ on compact sets;
6. the inverse-Hessian energy

$$\int_E\sum_{i,j}a_i(x)\bigl((\nabla^2U(x))^{-1}\bigr)_{ij}a_j(x)\,d\nu(x)$$

is integrable; 7. $v$ is smooth of class $C^\infty$ and has compact support.

Then both $\eta(-\mathcal L_Uv)$ and $(\mathcal L_Uv)^2$ are integrable under $\nu$, and

$$2\int_E\eta(x)(-\mathcal L_Uv(x))\,d\nu(x)-\int_E(\mathcal L_Uv(x))^2\,d\nu(x) \le \int_E a(x)^\mathsf T(\nabla^2U(x))^{-1}a(x)\,d\nu(x).$$

The declaration is a weak, finite-energy variational estimate for compactly supported smooth test functions.

Original Lean declaration header

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

theorem compact_weak_variational_estimate {n : ℕ}
    {nu : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))}
    {U eta v : EuclideanSpace ℝ (Fin n) → ℝ}
    (hnuU : (nu : Measure (EuclideanSpace ℝ (Fin n))) =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U))
    (hU : ContDiff ℝ 1 U) {G : NNReal} (hG : LipschitzWith G (gradient U))
    {L : NNReal} (hL : LipschitzWith L U)
    (hnorm : (∫ x, Real.exp (-U x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) = 1)
    (hPD : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), (hessianMatrix U x).PosDef)
    (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))
    (henergy : Integrable (fun x => (fun i => a i x) ⬝ᵥ
      ((hessianMatrix U x)⁻¹ *ᵥ (fun i => a i x))) (nu : Measure (EuclideanSpace ℝ (Fin n))))
    (hv : ContDiff ℝ ∞ v) (hvc : HasCompactSupport v) :
    Integrable (fun x => eta x * (-weightedLaplacian U v x)) (nu : Measure (EuclideanSpace ℝ (Fin n))) ∧
    Integrable (fun x => weightedLaplacian U v x ^ 2) (nu : Measure (EuclideanSpace ℝ (Fin n))) ∧
    2 * (∫ x, eta x * (-weightedLaplacian U v x) ∂(nu : Measure (EuclideanSpace ℝ (Fin n)))) -
      (∫ x, weightedLaplacian U v x ^ 2 ∂(nu : Measure (EuclideanSpace ℝ (Fin n)))) ≤
        ∫ x, (fun i => a i x) ⬝ᵥ ((hessianMatrix U x)⁻¹ *ᵥ (fun i => a i x))
          ∂(nu : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: KLS/LogConcave/WeakBrascampLieb.

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

Supporting theorems: compact_ordinary_diffusion_coercivity_of_lipschitz_gradient, integral_bounded_weak_mul_weightedLaplacian_of_contDiff_one, inverse_quadratic_young.

Next: scalar_brascamp_lieb_weak_finite_energy.

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

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeakBrascampLieb

open MeasureTheory Filter Topology Set InnerProductSpace Matrix
open FunctionalInequalities.Analysis
open FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.Probability.Stein
open scoped ContDiff RealInnerProductSpace
set_option maxHeartbeats 2000000

theorem FunctionalInequalities.KLS.LogConcave.compact_weak_variational_estimate_readable {n : ℕ}
    {nu : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))}
    {U eta v : EuclideanSpace ℝ (Fin n) → ℝ}
    (hnuU : (nu : Measure (EuclideanSpace ℝ (Fin n))) =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-U))
    (hU : ContDiff ℝ 1 U) {G : NNReal} (hG : LipschitzWith G (gradient U))
    {L : NNReal} (hL : LipschitzWith L U)
    (hnorm : (∫ x, Real.exp (-U x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) = 1)
    (hPD : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))), (hessianMatrix U x).PosDef)
    (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))
    (henergy : Integrable (fun x => (fun i => a i x) ⬝ᵥ
      ((hessianMatrix U x)⁻¹ *ᵥ (fun i => a i x))) (nu : Measure (EuclideanSpace ℝ (Fin n))))
    (hv : ContDiff ℝ ∞ v) (hvc : HasCompactSupport v) :
    Integrable (fun x => eta x * (-weightedLaplacian U v x)) (nu : Measure (EuclideanSpace ℝ (Fin n))) ∧
    Integrable (fun x => weightedLaplacian U v x ^ 2) (nu : Measure (EuclideanSpace ℝ (Fin n))) ∧
    2 * (∫ x, eta x * (-weightedLaplacian U v x) ∂(nu : Measure (EuclideanSpace ℝ (Fin n)))) -
      (∫ x, weightedLaplacian U v x ^ 2 ∂(nu : Measure (EuclideanSpace ℝ (Fin n)))) ≤
        ∫ x, (fun i => a i x) ⬝ᵥ ((hessianMatrix U x)⁻¹ *ᵥ (fun i => a i x))
          ∂(nu : Measure (EuclideanSpace ℝ (Fin n))) := by sorry