Nonnegativity Of A Compact-Test Dual Constant

This theorem states the sign condition needed for a compact-test dual gradient bound.

Let $n\ge1$, let $m$ be an additive Haar measure on $E=\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$, let $\nu$ be a probability measure, and let $W:E\to\mathbb R$ be continuous with $\nu=m.\operatorname{tilted}(-W)$. If $F:E\to\mathbb R$ and $K\in\mathbb R$ satisfy, for every smooth compactly supported $h$,

then

The conclusion requires positive dimension $n\ge1$ and uses no convexity assumption on $W$. The derivative is the Fréchet derivative fderiv ℝ h and the energy has no factor $1/2$.

Original Lean declaration header

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

theorem nonneg_of_forall_sq_integral_le_mul_integral_norm_fderiv_sq {n : ℕ} (hn : 0 < n)
    (m : Measure (EuclideanSpace ℝ (Fin n))) [m.IsAddHaarMeasure]
    {ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))}
    {W : EuclideanSpace ℝ (Fin n) → ℝ} (hνW : (ν : Measure _) = m.tilted (-W))
    (hW : Continuous W) {F : EuclideanSpace ℝ (Fin n) → ℝ} {K : ℝ}
    (hK : ∀ h : EuclideanSpace ℝ (Fin n) → ℝ, ContDiff ℝ ∞ h → HasCompactSupport h →
      (∫ x, F x * h x ∂(ν : Measure _)) ^ 2 ≤
        K * ∫ x, ‖fderiv ℝ h x‖ ^ 2 ∂(ν : Measure _)) :
    0 ≤ K

Module navigation

Module: KLS/LogConcave/HminusOne.

Next: sum_integral_norm_fderiv_partial_sq_le_integral_weightedLaplacian_sq.

Source excerpt, lines 30–38 · Frozen source 408915f.