Log-Concavity Under Inverse Continuous Linear Equivalence

This statement shows that log-concavity pulls back through a continuous linear equivalence when its pushforward law is log-concave.

Let $E$ and $F$ be real normed vector spaces, each equipped with a Borel measurable structure. Let $μ$ be a probability measure on $E$ and let $ν$ be a probability measure on $F$. Assume:

1. $μ$ is log-concave.
2. $T : F → E$ is a continuous linear equivalence over $ℝ$.
3. The pushforward of $ν$ by $T$ is $μ$:

Then $ν$ is log-concave:

This provides a reusable change-of-space principle for log-concave probability laws, without requiring inner-product or finite-dimensional structure in either space.

Formalization Note The conclusion is the predicate KLS.LogConcave; the pushforward equation is Lean's Measure.map equality after coercing the probability measures to measures. The map $T$ is a continuous linear equivalence, so both $T$ and its inverse are continuous and injective.

Original Lean declaration header

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

theorem of_continuousLinearEquiv_map {μ : ProbabilityMeasure E} (hμ : LogConcave μ)
    (ν : ProbabilityMeasure F) (T : F ≃L[ℝ] E)
    (hmap : Measure.map T (ν : Measure F) = (μ : Measure E)) : LogConcave ν

Module navigation

Module: KLS/LogConcave/Isotropic.

Definition modules: Probability/LogConcave.

Next: exists_isotropic_localSlope_constant_eq.

Source excerpt, lines 61–63 · Frozen source 408915f.