Weak Finite-Energy Scalar Brascamp–Lieb Inequality

This formalizes the scalar finite-energy form of Lemma A.6 of Letwin (arXiv:2607.24164v1), cited as “Brascamp–Lieb for $\nu$.”

Let $\nu$ be a log-concave probability measure on $E=\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$, with $\nu=e^{-U}\,dx$ in the tilted-measure sense. Assume that $U$ is $C^1$, globally Lipschitz, has Lipschitz gradient, and satisfies $\int e^{-U}\,dx=1$; assume also that $\nabla^2U(x)$ is positive definite almost everywhere. Let $\eta:E\to\mathbb R$ be locally integrable and globally bounded by $C$, and let $a_i$ be its weak derivatives along the coordinate basis, locally in $L^2$ on compact sets. Finally assume the inverse-Hessian energy is integrable. Then

The inequality is stated for weakly differentiable bounded tests and explicitly requires finite inverse-Hessian energy; it does not assert a bound for arbitrary unbounded or infinite-energy tests.

Original Lean declaration header

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

theorem scalar_brascamp_lieb_weak_finite_energy {n : ℕ}
    {nu : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))} (hnu : KLS.LogConcave nu)
    {U eta : 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)))) :
    ProbabilityTheory.variance eta (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, Probability/LogConcave, Analysis/WeakDerivative/Basic.

Supporting theorems: centered_mem_closure_compactSmoothDiffusionImage, compact_weak_variational_estimate, inner_center_left_of_mean_zero, norm_sq_le_of_mem_closure_quadratic_bound.

Previous: compact_weak_variational_estimate.

Source excerpt, lines 119–138 · Frozen source 408915f.