Strict Convexity From Compact Target Push-Forward

This states strict convexity of a moment potential under a compact-target push-forward hypothesis.

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

Let $K\subseteq E$ be compact, convex, and nonempty. Let $V:E\to\mathbb R$ be continuous. Assume that the push-forward of the tilted volume measure by $\nabla u$ equals the volume measure with density $1_K(p)\operatorname{ofReal}(e^{-V(p)})$. Then

The result packages the contact-set argument into a global strict-convexity conclusion. It does not assert differentiability.

Original Lean declaration header

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

theorem strictConvexOn_of_map_gradient {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [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) (hKne : 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)))) :
    StrictConvexOn ℝ univ u

Module navigation

Module: Analysis/Convex/Caffarelli.

Supporting theorems: eq_of_contact_of_sublevel_bounds, exists_forall_le_and_isCompact_sublevel_of_convexOn_integrable_exp_neg, strictConvexOn_of_contact_eq, volume_subgradientImage_eq_lintegral_of_isOpen.

Previous: eq_of_contact_of_sublevel_bounds · Next: contDiff_one_of_map_gradient.

Source excerpt, lines 1987–1995 · Frozen source 408915f.