Coordinate Hessian Bound for a Convex Potential

This is the coordinate form of the Bochner bound cited as Proposition 2.8 of Letwin (arXiv:2607.24164v1).

Let $n\in\mathbb N$, let $m$ be an additive Haar measure on $\mathbb R^n\simeq\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$, and let $W$ be a $C^2$ convex function. Let $g$ be smooth and compactly supported. With $\mu=m.\operatorname{tilted}(-W)$ and $e_i$ the standard coordinate vectors,

This is a finite-dimensional coordinate version of the integrated Hessian estimate and is used in dual-gradient and $H^{-1}$ arguments.

Formalization Note. The ambient space is exactly EuclideanSpace ℝ (Fin n); no positivity assumption on $n$ is included.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem sum_integral_norm_fderiv_partial_sq_le_integral_weightedLaplacian_sq [m.IsAddHaarMeasure]
    {W : EuclideanSpace ℝ (Fin n) → ℝ} (hW : ContDiff ℝ 2 W) (hWc : ConvexOn ℝ Set.univ W)
    {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : ContDiff ℝ ∞ g) (hgc : HasCompactSupport g) :
    ∑ i, ∫ x, ‖fderiv ℝ (fun y => fderiv ℝ g y (EuclideanSpace.single i 1)) x‖ ^ 2
        ∂(m.tilted (-W)) ≤
      ∫ x, weightedLaplacian W g x ^ 2 ∂(m.tilted (-W))

Module navigation

Module: KLS/LogConcave/HminusOne.

Definition modules: Analysis/BakryEmery/Laplacian.

Supporting theorems: gammaTwo_eq_hessianSqStdBasis_add, integrable_gamma_weightedLaplacian, integrable_weightedLaplacian_gamma, integral_gamma_weightedLaplacian_eq.

Previous: nonneg_of_forall_sq_integral_le_mul_integral_norm_fderiv_sq · Next: variance_le_sum_of_partial_dual_bounds.

Source excerpt, lines 264–269 · Frozen source 408915f.