Concave Tilting Preserves Log-Concavity

This statement asserts that a continuous concave tilt of a log-concave probability law remains log-concave.

Let $E$ be a finite-dimensional real inner-product normed space equipped with its Borel measurable structure, and let $μ$ and $ν$ be probability measures on $E$. Assume:

1. $μ$ is log-concave.
2. $φ : E → ℝ$ is continuous.
3. $φ$ is concave on all of $E$.
4. As measures on $E$, $ν$ equals the tilt of $μ$ by $φ$, expressed in Lean by Measure.tilted:

$$ν = \operatorname{tilted}(μ,φ).$$

Then $ν$ is log-concave:

$$ν\text{ is log-concave}.$$

The result is useful for transporting log-concavity through exponential weights, including laws supported on proper affine subspaces and the zero-dimensional case.

Formalization Note The log-concavity predicate is KLS.LogConcave. The statement imposes finite dimensionality but no positive-dimension assumption, and the equality of measures is interpreted through the canonical coercions from probability measures to measures.

Original Lean declaration header

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

theorem logConcave_of_concave_tilt (μ ν : ProbabilityMeasure E) (hLC : KLS.LogConcave μ)
    (φ : E → ℝ) (hφ : Continuous φ) (hconc : ConcaveOn ℝ univ φ)
    (hν : (ν : Measure E) = (μ : Measure E).tilted φ) : KLS.LogConcave ν

Module navigation

Module: KLS/LogConcave/Density/ConcaveTilt.

Definition modules: Probability/LogConcave.

Supporting theorems: integrable_exp_neg_of_eq_tilted, isBorellDensity_of_concave_tilt, map_affineIsometry, affineSupport_intrinsicMeasure.

Previous: isBorellDensity_of_concave_tilt.

Source excerpt, lines 81–83 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_ConcaveTilt

open MeasureTheory Set Filter Topology FunctionalInequalities
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

theorem FunctionalInequalities.KLS.LogConcave.logConcave_of_concave_tilt_readable (μ ν : ProbabilityMeasure E) (hLC : KLS.LogConcave μ)
    (φ : E → ℝ) (hφ : Continuous φ) (hconc : ConcaveOn ℝ univ φ)
    (hν : (ν : Measure E) = (μ : Measure E).tilted φ) : KLS.LogConcave ν := by sorry