Convexity of a Continuous Tilt Potential

This statement shows that a continuous potential representing a log-concave tilted law is convex.

Let $V$ be a finite-dimensional real inner-product space, let $m$ be an additive Haar measure, and let $\nu$ be a log-concave probability measure. Suppose

$$\nu=m\mathbin{.}\mathrm{tilted}(-U)$$

for a continuous function $U:V\to\mathbb R$. Then $U$ is convex on all of $V$:

$$\operatorname{ConvexOn}(\mathbb R,\mathbb R^n,U).$$

Equivalently, for all $x,y\in V$ and $a,b\ge0$ with $a+b=1$,

$$U(ax+by)\le aU(x)+bU(y).$$

The result supplies the convexity of the potential needed to obtain nonnegative curvature in the heat-model arguments.

Original Lean declaration header

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

theorem convexOn_of_eq_tilted (hν : LogConcave ν) (hνU : (ν : Measure V) = m.tilted (-U))
    (hU : Continuous U) : ConvexOn ℝ Set.univ U

Module navigation

Module: KLS/LogConcave/Density/Tilted.

Definition modules: Probability/LogConcave.

Supporting theorems: integrable_exp_neg_of_eq_tilted, integral_exp_neg_pos_of_eq_tilted, interior_support_nonempty_of_eq_tilted.

Previous: interior_support_nonempty_of_eq_tilted · Next: logConcave_of_eq_regularClass.

Source excerpt, lines 180–181 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_Tilted

open MeasureTheory Set
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {ν : MeasureTheory.ProbabilityMeasure V}
variable [SecondCountableTopology V] (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] {U : V → ℝ}

theorem FunctionalInequalities.KLS.LogConcave.convexOn_of_eq_tilted_readable (hν : LogConcave ν) (hνU : (ν : Measure V) = m.tilted (-U))
    (hU : Continuous U) : ConvexOn ℝ Set.univ U := by sorry