Conditional Reduction From Isotropic Log-Concave Laws to Regular Laws

This is a conditional reduction of an isotropic log-concave Poincaré bound to a bound on isotropic regular laws in the same space.

Let $E$ be a finite-dimensional complete real inner product space with its Borel measurable structure, and fix $K\in[0,\infty)$. Assume that for every $V:E\to\mathbb R$, $a,b\in\mathbb R$, and $h_V:$ KLS.RegularPotential V a b,

Then every probability measure $\mu$ on $E$ that is both log-concave (KLS.LogConcave) and isotropic (KLS.Isotropic) satisfies

Isotropy requires finite second moment, zero mean, and identity centered covariance. The law in the hypothesis is RegularPotential.law; $C_P^{\mathrm{lit}}$ is Poincare.LocalSlope.Intrinsic.constant.

This reduction preserves a supplied bound $K$; it does not establish the regular-law hypothesis or the existence of such a bound.

Formalization Note $K$ is NNReal, and both inequalities use its coercion to ENNReal. The statement concerns one fixed space $E$ and includes dimension zero.

Original Lean declaration header

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

theorem localSlope_le_of_regular_isotropic_bound {K : NNReal}
    (hBound : ∀ {V : E → ℝ} {a b : ℝ} (hV : KLS.RegularPotential V a b),
      0 < b → KLS.Isotropic hV.law →
        Poincare.LocalSlope.Intrinsic.constant hV.law ≤ (K : ENNReal))
    (μ : ProbabilityMeasure E) (hLC : KLS.LogConcave μ) (hiso : KLS.Isotropic μ) :
    Poincare.LocalSlope.Intrinsic.constant μ ≤ (K : ENNReal)

Module navigation

Module: KLS/LogConcave/IsotropicReduction.

Definition modules: Probability/LogConcave, KLS/Isotropic, KLS/LogConcave/Regular/Basic, Poincare/LocalSlope/Basic.

Selected supporting theorems: convexOn_of_hessian_ge, exists_metric_diagonal, relaxation_eq_ofLinearPMap, relaxation_le_mul_lipschitz, relaxation_mapContinuousLinearEquiv.

Source excerpt, lines 60–65 · Frozen source 408915f.