Variance Bound From Partial Dual Estimates

This formalizes the $H^{-1}$ variance inequality of Letwin (arXiv:2607.24164v1) (Proposition 2.8, partial relation).

Let $n\in\mathbb N$, let $m$ be an additive Haar measure on $E=\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$, and let $\nu$ be log-concave with

$$\nu=m.\operatorname{tilted}(-W).$$

Assume:

1. $W$ is $C^2$ and convex on all of $E$.
2. $f:E\to\mathbb R$ is $C^1$ and belongs to $L^2(\nu)$.
3. Every coordinate derivative $x\mapsto Df(x)[e_i]$ belongs to $L^2(\nu)$, where $e_i=\operatorname{single}(i,1)$.
4. For each $i$ and every smooth compactly supported $h$,

$$\left(\int_E Df(x)[e_i]h(x)\,d\nu(x)\right)^2 \le K_i\int_E\|Dh(x)\|^2\,d\nu(x).$$

Then

$$\operatorname{Var}_\nu(f)\le\sum_{i=1}^n K_i.$$

The theorem is finite-dimensional and retains the explicit $C^2$ convexity, $L^2$, and coordinate-derivative hypotheses. It is a variance assembly result from the separate compact-test dual bounds.

Original Lean declaration header

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

theorem variance_le_sum_of_partial_dual_bounds {n : ℕ}
    (m : Measure (EuclideanSpace ℝ (Fin n))) [m.IsAddHaarMeasure]
    {ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))} (hν : FunctionalInequalities.KLS.LogConcave ν)
    {W : EuclideanSpace ℝ (Fin n) → ℝ} (hνW : (ν : Measure _) = m.tilted (-W))
    (hW : ContDiff ℝ 2 W) (hWc : ConvexOn ℝ Set.univ W)
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ContDiff ℝ 1 f) (hf2 : MemLp f 2 (ν : Measure _))
    (hdf2 : ∀ i, MemLp (fun x => fderiv ℝ f x (EuclideanSpace.single i 1)) 2 (ν : Measure _))
    (K : Fin n → ℝ)
    (hK : ∀ i (h : EuclideanSpace ℝ (Fin n) → ℝ), ContDiff ℝ ∞ h → HasCompactSupport h →
      (∫ x, fderiv ℝ f x (EuclideanSpace.single i 1) * h x ∂(ν : Measure _)) ^ 2 ≤
        K i * ∫ x, ‖fderiv ℝ h x‖ ^ 2 ∂(ν : Measure _)) :
    variance f (ν : Measure _) ≤ ∑ i, K i

Module navigation

Module: KLS/LogConcave/HminusOne.

Definition modules: Probability/LogConcave.

Selected supporting theorems: sum_integral_norm_fderiv_partial_sq_le_integral_weightedLaplacian_sq, centered_mem_closure_compactSmoothDiffusionImage, compact_pairing_identity, inner_center_left_of_mean_zero, nonneg_of_forall_sq_integral_le_mul_integral_norm_fderiv_sq.

Previous: sum_integral_norm_fderiv_partial_sq_le_integral_weightedLaplacian_sq.

Source excerpt, lines 456–467 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HminusOne

open MeasureTheory
open scoped ContDiff
open ProbabilityTheory InnerProductSpace

theorem FunctionalInequalities.KLS.LogConcave.variance_le_sum_of_partial_dual_bounds_readable {n : ℕ}
    (m : Measure (EuclideanSpace ℝ (Fin n))) [m.IsAddHaarMeasure]
    {ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))} (hν : FunctionalInequalities.KLS.LogConcave ν)
    {W : EuclideanSpace ℝ (Fin n) → ℝ} (hνW : (ν : Measure _) = m.tilted (-W))
    (hW : ContDiff ℝ 2 W) (hWc : ConvexOn ℝ Set.univ W)
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ContDiff ℝ 1 f) (hf2 : MemLp f 2 (ν : Measure _))
    (hdf2 : ∀ i, MemLp (fun x => fderiv ℝ f x (EuclideanSpace.single i 1)) 2 (ν : Measure _))
    (K : Fin n → ℝ)
    (hK : ∀ i (h : EuclideanSpace ℝ (Fin n) → ℝ), ContDiff ℝ ∞ h → HasCompactSupport h →
      (∫ x, fderiv ℝ f x (EuclideanSpace.single i 1) * h x ∂(ν : Measure _)) ^ 2 ≤
        K i * ∫ x, ‖fderiv ℝ h x‖ ^ 2 ∂(ν : Measure _)) :
    variance f (ν : Measure _) ≤ ∑ i, K i := by sorry