Log-Concavity of a Regular-Class Density

This statement proves log-concavity from a regular-class density representation.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure, let $μ$ be a probability measure, and let $K\subseteq E$. Assume:

1. $K$ is closed and convex;
2. $W:E\to\mathbb R$ is continuous;
3. $κ>0$;
4. $y\mapsto W(y)-(κ/2)\|y\|^2$ is convex on $E$;
5. as measures,

Then LogConcave μ holds. This result converts the analytic regular-class description into the abstract log-concavity predicate.

Original Lean declaration header

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

theorem logConcave_of_eq_regularClass
    (μ : ProbabilityMeasure E) {K : Set E} (hK : IsClosed K) (hKc : Convex ℝ K)
    {W : E → ℝ} (hW : Continuous W) {κ : ℝ} (hκ : 0 < κ)
    (hstrong : ConvexOn ℝ univ (fun y => W y - (κ / 2) * ‖y‖ ^ 2))
    (hμ : (μ : Measure E) = (volume : Measure E).withDensity
      (K.indicator fun x => ENNReal.ofReal (Real.exp (-W x)))) :
    FunctionalInequalities.KLS.LogConcave μ

Module navigation

Module: KLS/LogConcave/Density/Tilted.

Definition modules: Probability/LogConcave.

Supporting theorems: rpow_mul_rpow_le_of_convexOn.

Previous: convexOn_of_eq_tilted.

Source excerpt, lines 294–300 · Frozen source 408915f.