Log-Concavity Under Affine Isometric Pushforward

This proves preservation of compact-set log-concavity under an affine isometric embedding.

Let $F$ and $E$ be real normed spaces with Borel measurable structures, assume $F$ is complete, and let $\nu$ be a log-concave probability measure on $F$. Let $\mu$ be a probability measure on $E$ and let $f:F\to E$ be an affine isometric embedding. If

then $\mu$ is log-concave:

The conclusion allows the image of $f$ to be lower-dimensional and requires no density assumption. This provides the affine-isometric transport direction for the library's compact-set definition of log-concavity.

Original Lean declaration header

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

theorem map_affineIsometry [CompleteSpace F]
    (ν : ProbabilityMeasure F) (hν : LogConcave ν)
    (μ : ProbabilityMeasure E) (f : F →ᵃⁱ[ℝ] E)
    (hmap : (μ : Measure E) = (ν : Measure F).map f) :
    LogConcave μ

Module navigation

Module: KLS/LogConcave/Transport.

Definition modules: Probability/LogConcave.

Next: cond.

Source excerpt, lines 66–70 · Frozen source 408915f.