Local-Slope Constant Bound From the Intrinsic Covariance Constant

This is a comparison between two intrinsic Poincaré constants of a log-concave probability law.

Let $E$ be a finite-dimensional complete real inner product space with its Borel measurable structure and a second-countable topology. Let $\mu$ be a log-concave probability measure (KLS.LogConcave), and let $K\in[0,\infty)$ satisfy

$$C_{\mathrm{cov}}^{\mathrm{int}}(\mu)\le K.$$

Here $C_{\mathrm{cov}}^{\mathrm{int}}$ denotes Poincare.CovarianceGradient.Intrinsic.constant. Write $C_P^{\mathrm{lit}}$ for Poincare.LocalSlope.Intrinsic.constant and $\Sigma_\mu$ for the covariance operator Covariance.operator.

Then

$$C_P^{\mathrm{lit}}(\mu)\le K\,\operatorname{ofReal}(\|\Sigma_\mu\|).$$

This comparison transfers a finite covariance-gradient bound to a literature local-slope bound for the same law.

Formalization Note Both constants and the displayed product take values in $[0,\infty]$ (ENNReal); $K$ is supplied as NNReal and coerced to ENNReal. No isotropy or positive-dimension hypothesis is imposed.

Original Lean declaration header

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

theorem localSlope_le_mul_intrinsicCovariance {μ : ProbabilityMeasure E}
    (hμ : LogConcave μ) {K : NNReal} (hK : Poincare.CovarianceGradient.Intrinsic.constant μ ≤ (K : ENNReal)) :
    Poincare.LocalSlope.Intrinsic.constant μ ≤ (K : ENNReal) * ENNReal.ofReal ‖Covariance.operator (μ : Measure E)‖

Module navigation

Module: KLS/LogConcave/Isotropic.

Definition modules: Probability/Covariance/Basic, Poincare/CovarianceGradient/Intrinsic, Probability/LogConcave, Poincare/LocalSlope/Basic.

Selected supporting theorems: opNorm_operator_intrinsic, relaxation_le_mul_lipschitz, exists_ambient_extension, memLp_id_two, Holds.of_energy_le_mul.

Previous: exists_isotropic_localSlope_constant_eq.

Source excerpt, lines 256–258 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Isotropic

open MeasureTheory Filter Topology InnerProductSpace
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]

theorem FunctionalInequalities.KLS.LogConcave.localSlope_le_mul_intrinsicCovariance_readable {μ : ProbabilityMeasure E}
    (hμ : LogConcave μ) {K : NNReal} (hK : Poincare.CovarianceGradient.Intrinsic.constant μ ≤ (K : ENNReal)) :
    Poincare.LocalSlope.Intrinsic.constant μ ≤ (K : ENNReal) * ENNReal.ofReal ‖Covariance.operator (μ : Measure E)‖ := by sorry