Borell Density Under a Concave Tilt

This states stability of Borell densities under continuous concave tilting.

Let $E$ be a real inner-product space with Borel measurable structure. Let $\mu$ and $\nu$ be probability measures, let $m$ be a measure, and let $\rho:E\to\mathbb R$ be a Borell density of $\mu$ with respect to $m$. Let $\phi:E\to\mathbb R$ be continuous and concave on all of $E$, and assume

Then $\nu$ has Borell density

with respect to $m$. The definition permits zeros of $\rho$. This result is a measure-theoretic closure property for the log-concave class and does not assume finite dimensionality in its Lean type.

Original Lean declaration header

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

theorem isBorellDensity_of_concave_tilt (μ ν : ProbabilityMeasure E)
    (m : Measure E) {ρ : E → ℝ} (hρ : KLS.IsBorellDensity (μ : Measure E) m ρ)
    (φ : E → ℝ) (hφ : Continuous φ) (hconc : ConcaveOn ℝ univ φ)
    (hν : (ν : Measure E) = (μ : Measure E).tilted φ) :
    KLS.IsBorellDensity (ν : Measure E) m
      (fun x => ρ x * (Real.exp (φ x) / ∫ y, Real.exp (φ y) ∂(μ : Measure E)))

Module navigation

Module: KLS/LogConcave/Density/ConcaveTilt.

Definition modules: KLS/LogConcave/Density/BorellRepresentation/Basic.

Supporting theorems: integrable_exp_neg_of_eq_tilted, rpow_mul_rpow_le_of_convexOn.

Next: logConcave_of_concave_tilt.

Source excerpt, lines 40–45 · Frozen source 408915f.