Centered Difference Bound for Moment-Map Potentials

This formalizes the centered-difference estimate associated with regularity of the moment map, cited in Lemma 2.2 of Letwin (arXiv:2607.24164v1) (Klartag [41]).

Let $u,V:\mathbb R^n\to\mathbb R$, let $L\in[0,\infty)$, and assume:

1. $u$ is $L$-Lipschitz and convex;
2. $\int e^{-u(x)}\,dx=1$;
3. $K\subset\mathbb R^n$ is compact and convex;
4. $V$ is $C^1$ and $V(y)-\frac\kappa2\|y\|^2$ is convex for some $\kappa>0$;
5. the pushforward of the tilted volume measure with density $e^{-u}$ under $\nabla u$ equals the measure with density $e^{-V}$ on $K$;
6. $u$ is $C^1$.

Then, for every $x,h\in\mathbb R^n$,

This exports the exact coefficient used in the subsequent Lipschitz-gradient regularity argument.

Original Lean declaration header

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

theorem secondDifference_le_of_map_gradient {n : ℕ} {u V : EuclideanSpace ℝ (Fin n) → ℝ}
    {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u)
    (hnorm : ∫ x, Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n))) = 1)
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : IsCompact K) (hKc : Convex ℝ K)
    (hV : ContDiff ℝ 1 V) {κ : ℝ} (hκ : 0 < κ)
    (hstrong : ConvexOn ℝ univ (fun y => V y - (κ / 2) * ‖y‖ ^ 2))
    (hmap : ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)).map (gradient u) =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity
        (K.indicator fun p => ENNReal.ofReal (Real.exp (-V p))))
    (hC1 : ContDiff ℝ 1 u) :
    ∀ x h : EuclideanSpace ℝ (Fin n),
      u (x + h) + u (x - h) - 2 * u x ≤ (4 / κ) * ‖h‖ ^ 2

Module navigation

Module: Analysis/Convex/GradientLipschitz.

Selected supporting theorems: ae_exists_quadraticAt_expansion, exists_forall_le_and_isCompact_sublevel_of_convexOn_integrable_exp_neg, exists_penalized_maximum_with_comparison, posDef_and_convolution_le_log_det_hessianMatrix, posDef_and_det_eq_of_quadratic_expansion.

Source excerpt, lines 89–100 · Frozen source 408915f.