Isotropic Log-Concave Reduction with Equal Intrinsic Constant

This is the isotropic reduction for a log-concave law.

Let $E$ be a finite-dimensional real inner-product normed space with Borel and second-countable structure, and let $\mu$ be a log-concave probability measure on $E$. Then there exists a probability measure $\nu'$ on the direction space of $\operatorname{affineSupport}(\mu)$ such that:

1. $\nu'$ is log-concave;
2. $\nu'$ is isotropic, including finite second moment, zero mean, and identity covariance operator;
3. the intrinsic covariance-gradient Poincaré constant of $\mu$ equals the intrinsic local-slope constant of $\nu'$:

The conclusion is existential and may place $\nu'$ on a lower-dimensional affine direction space; it does not assert finiteness of the common constant.

Original Lean declaration header

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

theorem exists_isotropic_localSlope_constant_eq {μ : ProbabilityMeasure E}
    (hμ : LogConcave μ) :
    ∃ ν' : ProbabilityMeasure (affineSupport μ).direction,
      LogConcave ν' ∧ Isotropic ν' ∧ Poincare.CovarianceGradient.Intrinsic.constant μ = Poincare.LocalSlope.Intrinsic.constant ν'

Module navigation

Module: KLS/LogConcave/Isotropic.

Definition modules: Poincare/CovarianceGradient/Intrinsic, Probability/LogConcave, KLS/Isotropic, Probability/AffineSupport, Poincare/LocalSlope/Basic.

Selected supporting theorems: intrinsic_operator_inner_self_pos, Covariance.operator_map_continuousLinearEquiv, relaxation_eq_ofLinearPMap, relaxation_mapContinuousLinearEquiv, relaxation_translateLaw.

Previous: of_continuousLinearEquiv_map · Next: localSlope_le_mul_intrinsicCovariance.

Source excerpt, lines 199–202 · Frozen source 408915f.