Gaussian Product Compact Dual Bound

This is a technical compact-test estimate for a Gaussian product coupling in finite-dimensional Euclidean space.

Let $n\in\mathbb N$, let $\mu$ and $\nu$ be probability measures on $E=\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$, and let $u:E\to\mathbb R$ and $L,G\in[0,\infty)$ satisfy:

1. $u$ is $C^1$.
2. $u$ is $L$-Lipschitz.
3. $\nabla u$ is $G$-Lipschitz.
4. $\int_E e^{-u(y)}\,dy=1$.
5. The pushforward of the tilted volume measure $e^{-u}\,dy$ by $\nabla u$ is $\mu$.

For every continuous linear map $S:E\to E$, vector $v\in E$, scalar $s>0$ such that $\nu$ is the $s$-Gaussian smoothing of the pushforward $S_\#\mu$, and every $C^\infty$ compactly supported function $h:E\to\mathbb R$, one has

where $P$ is the product of the tilted source measure and the Gaussian law of variance parameter $s$. Here the derivative term is the operator norm of the Fréchet derivative $Dh$ (written in Lean as fderiv ℝ h x). The statement is reusable as a compact dual Cauchy–Schwarz estimate for this particular latent Gaussian coupling; it does not construct a target Stein kernel or an inverse transport.

Original Lean declaration header

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

set_option maxHeartbeats 800000 in
theorem gaussian_product_compact_dual_bound {n : ℕ}
    (μ ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    {u : EuclideanSpace ℝ (Fin n) → ℝ} {L G : NNReal}
    (hu : ContDiff ℝ 1 u) (hL : LipschitzWith L u)
    (hG : LipschitzWith G (gradient u))
    (hnorm : (∫ y, Real.exp (-u y) ∂volume) = 1)
    (hsource : ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)).map
      (gradient u) = (μ : Measure (EuclideanSpace ℝ (Fin n))))
    (S : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (v : EuclideanSpace ℝ (Fin n)) {s : ℝ} (hs : 0 < s)
    (hν : (ν : Measure (EuclideanSpace ℝ (Fin n))) = smoothedLaw ((μ : Measure _).map S) s)
    (h : EuclideanSpace ℝ (Fin n) → ℝ) (hh : ContDiff ℝ ∞ h) (hhc : HasCompactSupport h) :
    let P := ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)).prod
      (gaussianLaw (V := EuclideanSpace ℝ (Fin n)) s)
    (∫ x, ⟪x,v⟫ * h x ∂(ν : Measure _)) ^ 2 ≤
      (∫ p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n),
        ‖S (action (hessianMatrix u p.1) (S.adjoint v)) + (2*s)⁻¹ • v‖ ^ 2 ∂P) *
      ∫ x, ‖fderiv ℝ h x‖ ^ 2 ∂(ν : Measure _)

Module navigation

Module: KLS/LogConcave/Density/GaussianSmoothing/ProductCoupling.

Definition modules: Analysis/BakryEmery/HessianOperator, KLS/LogConcave/Density/GaussianSmoothing/Basic, Probability/Stein/Kernel.

Supporting theorems: gaussian_product_latent_map, gaussian_product_source_stein_identity, gaussian_product_source_stein_pairings_integrable, compact_linear_pairing_sq_le_of_source_identity.

Previous: gaussian_product_source_stein_identity.

Source excerpt, lines 208–226 · Frozen source 408915f.