Smoothed Quadratic Variance Bounded by Latent Product Energy

This is a finite-dimensional Gaussian-smoothing variance estimate.

Let $\mu$ be a probability measure on $E=\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$ such that LogConcave μ and whose affine support is the whole space. Let $u:E\to\mathbb R$ satisfy:

1. $u$ is $C^1$;
2. $u$ is globally Lipschitz with constant $L\in\mathbb{NNReal}$;
3. $\nabla u$ is globally Lipschitz with constant $G\in\mathbb{NNReal}$;
4. $\int_E e^{-u(y)}\,dy=1$;
5. the tilted Lebesgue measure with density proportional to $e^{-u}$, pushed forward by $\nabla u$, equals $\mu$.

Let $S:E\simeq E$ be a continuous linear equivalence, let $Q:E\to E$ be continuous linear and self-adjoint, and let $s>0$. Write $P=\bigl(e^{-u}\,dy\bigr)\otimes\gamma_s$, where $\gamma_s$ is the Gaussian law used by gaussianLaw, and let smoothedLaw denote the corresponding Gaussian-smoothed image law. Then

Here $e_i$ is the $i$th coordinate vector and the displayed right-hand side is exactly the latent product energy in the Lean statement. This provides a technical bridge from smoothed quadratic variance to Hessian-based latent energies.

Original Lean declaration header

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

set_option maxHeartbeats 1000000 in
theorem gaussian_smoothed_quadratic_variance_le_latent_energy {n : ℕ}
    (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hLC : FunctionalInequalities.KLS.LogConcave μ)
    (hfull : Probability.affineSupport μ = ⊤)
    {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))
    (Q : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hQ : IsSelfAdjoint Q) {s : ℝ} (hs : 0 < s) :
    let P := ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)).prod
      (gaussianLaw (V := EuclideanSpace ℝ (Fin n)) s)
    variance (fun x => ⟪Q x,x⟫) (smoothedLaw ((μ : Measure _).map S) s) ≤
      4 * ∑ i : Fin n, ∫ p : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n),
        ‖S (action (hessianMatrix u p.1) (S.toContinuousLinearMap.adjoint
          (Q (EuclideanSpace.single i 1)))) + (2*s)⁻¹ • Q (EuclideanSpace.single i 1)‖ ^ 2 ∂P

Module navigation

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

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

Selected supporting theorems: gaussianLaw_exp_norm_integrable, gaussian_product_compact_dual_bound, of_continuousLinearEquiv_map, variance_le_sum_of_partial_dual_bounds, Probability.affineSupport_mapContinuousLinearEquiv.

Source excerpt, lines 34–53 · Frozen source 408915f.