Continuous Differentiability of the Moment Potential

This formalizes the regularity statement associated with Klartag's result, cited as Lemma 2.2 in Letwin (arXiv:2607.24164v1), with the reviewed relation recorded as partial.

Let $E$ be a nontrivial finite-dimensional real inner-product space with its Borel measurable structure. Let $u:E\to\mathbb R$ be Lipschitz and convex, and assume:

1. $\int_E e^{-u(x)}\,d\operatorname{vol}(x)=1$.
2. $K\subseteq E$ is compact, convex, and has nonempty interior.
3. $V:E\to\mathbb R$ is continuous.
4. The push-forward of the tilted volume measure by $\nabla u$ equals the measure with density $1_K(p)\operatorname{ofReal}(e^{-V(p)})$.

Then

formalized as ContDiff ℝ 1 u.

This is the regularity conclusion used for the moment potential in the finite-dimensional compact-target setting.

Formalization Note The statement proves ContDiff of order $1$ on the whole finite-dimensional space; it does not state positive-definite Hessian, a global diffeomorphism, or a pointwise Monge–Ampère equation.

Original Lean declaration header

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

theorem contDiff_one_of_map_gradient
    [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E] [BorelSpace E]
    {u : E → ℝ} {L : NNReal} (hu : LipschitzWith L u) (hconv : ConvexOn ℝ univ u)
    (hnorm : ∫ x, Real.exp (-u x) ∂(volume : Measure E) = 1)
    {K : Set E} (hK : IsCompact K) (hKc : Convex ℝ K) (hKint : (interior K).Nonempty)
    {V : E → ℝ} (hV : Continuous V)
    (hmap : ((volume : Measure E).tilted (-u)).map (gradient u) =
      (volume : Measure E).withDensity (K.indicator fun p => ENNReal.ofReal (Real.exp (-V p)))) :
    ContDiff ℝ 1 u

Module navigation

Module: Analysis/Convex/Caffarelli.

Selected supporting theorems: contDiff_one_of_convexOn_of_differentiable, convexOn_truncatedConjugate, eq_of_contact_of_sublevel_bounds, exists_inverse_subgradient_volume_bounds, exists_subgradient_slope_le_inner_add.

Previous: strictConvexOn_of_map_gradient.

Source excerpt, lines 2156–2164 · Frozen source 408915f.