Regular Moment Potential

This formalizes part of Lemma 2.2 of Letwin (arXiv:2607.24164v1), with the displayed conclusions restricted to the formalized hypotheses.

Let $n\ge1$, $K\subset\mathbb{R}^n$ be compact, convex, and with nonempty interior, and let $W:\mathbb{R}^n\to\mathbb{R}$ be smooth. Let $\kappa>0$ and assume $y\mapsto W(y)-\frac\kappa2\|y\|^2$ is convex. Let $\mu$ be an isotropic probability measure satisfying

$$\mu=\mathbf{1}_K e^{-W}\,dx$$

in the withDensity sense. Then there exist $u:\mathbb{R}^n\to\mathbb{R}$ and $L\in[0,\infty)$ such that $u$ is convex, $L$-Lipschitz, normalized by $\int e^{-u}=1$, and its tilted measure pushes forward under $\nabla u$ to $\mu$:

$$(e^{-u}dx)\circ(\nabla u)^{-1}=\mu.$$

Moreover, $u\in C^1$, $\nabla u$ is $(16/\kappa)$-Lipschitz, and for almost every $x$ the Hessian $H=\nabla^2u$ is positive definite and satisfies

$$\log\det H(x)=-u(x)+W(\nabla u(x)),$$

and

$$\frac{16}{\kappa}I-H(x)\succeq0.$$

The space is EuclideanSpace ℝ (Fin n) and the almost-everywhere assertions use Lebesgue measure.

Original Lean declaration header

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

theorem exists_regular_moment_potential {n : ℕ} (hn : 0 < n) {K : Set (EuclideanSpace ℝ (Fin n))}
    {W : EuclideanSpace ℝ (Fin n) → ℝ} {κ : ℝ} (hκ : 0 < κ) (hK : IsCompact K) (hKc : Convex ℝ K)
    (hKint : (interior K).Nonempty) (hW : ContDiff ℝ ∞ W)
    (hstrong : ConvexOn ℝ univ (fun y => W y - (κ / 2) * ‖y‖ ^ 2))
    (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hμ : (μ : Measure (EuclideanSpace ℝ (Fin n))) =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity
        (K.indicator fun p => ENNReal.ofReal (Real.exp (-W p))))
    (hiso : KLS.Isotropic μ) :
    ∃ (u : EuclideanSpace ℝ (Fin n) → ℝ) (L : NNReal), ConvexOn ℝ univ u ∧ LipschitzWith L u ∧
      (∫ x, Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) = 1 ∧
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)).map (gradient u) =
        (μ : Measure (EuclideanSpace ℝ (Fin n))) ∧
      ContDiff ℝ 1 u ∧ LipschitzWith (Real.toNNReal (16 / κ)) (gradient u) ∧
      ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
        (hessianMatrix u x).PosDef ∧
        Real.log (hessianMatrix u x).det = -u x + W (gradient u x) ∧
        ((16 / κ) • (1 : Matrix (Fin n) (Fin n) ℝ) - hessianMatrix u x).PosSemidef

Module navigation

Module: KLS/CEK/MomentRegularity/Potential.

Definition modules: Analysis/BakryEmery/HessianOperator, Analysis/Operator/Coordinates, KLS/Isotropic.

Selected supporting theorems: contDiff_one_of_map_gradient, eventually_abs_sub_quadratic_le_of_subgradient_expansion, lipschitzWith_gradient_of_second_difference_le, posDef_and_det_eq_of_quadratic_expansion, secondDifference_le_of_map_gradient.

Source excerpt, lines 32–49 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_CEK_MomentRegularity_Potential

open MeasureTheory Set Filter
open scoped RealInnerProductSpace ContDiff Topology
open FunctionalInequalities.Probability.Stein

theorem FunctionalInequalities.Analysis.exists_regular_moment_potential_readable {n : ℕ} (hn : 0 < n) {K : Set (EuclideanSpace ℝ (Fin n))}
    {W : EuclideanSpace ℝ (Fin n) → ℝ} {κ : ℝ} (hκ : 0 < κ) (hK : IsCompact K) (hKc : Convex ℝ K)
    (hKint : (interior K).Nonempty) (hW : ContDiff ℝ ∞ W)
    (hstrong : ConvexOn ℝ univ (fun y => W y - (κ / 2) * ‖y‖ ^ 2))
    (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hμ : (μ : Measure (EuclideanSpace ℝ (Fin n))) =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity
        (K.indicator fun p => ENNReal.ofReal (Real.exp (-W p))))
    (hiso : KLS.Isotropic μ) :
    ∃ (u : EuclideanSpace ℝ (Fin n) → ℝ) (L : NNReal), ConvexOn ℝ univ u ∧ LipschitzWith L u ∧
      (∫ x, Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) = 1 ∧
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)).map (gradient u) =
        (μ : Measure (EuclideanSpace ℝ (Fin n))) ∧
      ContDiff ℝ 1 u ∧ LipschitzWith (Real.toNNReal (16 / κ)) (gradient u) ∧
      ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
        (hessianMatrix u x).PosDef ∧
        Real.log (hessianMatrix u x).det = -u x + W (gradient u x) ∧
        ((16 / κ) • (1 : Matrix (Fin n) (Fin n) ℝ) - hessianMatrix u x).PosSemidef := by sorry