Poincaré Constant Bounded By A Form-Domain Gap

This statement converts a form-domain Poincaré inequality into an upper bound for the intrinsic literature constant.

Let $V$ be finite-dimensional, let $\nu$ be log-concave with nonempty support interior, and let $m$ be an additive Haar measure. Let $C\in[0,\infty)$ be represented by a NNReal. Suppose every $u$ in the domain of the closed weighted operator satisfies

$$\|\operatorname{center}_\nu u\|^2\le C\,\|\overline{\nabla}u\|^2.$$

Then

$$C_P(\nu)\le C,$$

where the right-hand side is interpreted as the coercion of $C$ to $[0,\infty]$.

This is a general comparison interface between a domain-level energy gap and the intrinsic Poincaré constant. It does not assert the converse in this declaration.

Formalization Note. The conclusion is an inequality in ENNReal; the hypothesis is real-valued.

Original Lean declaration header

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

theorem literatureConstant_le_of_gap (C : NNReal)
    (hgap : ∀ u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain,
      ‖L2.center ν (u : Lp ℝ 2 (ν : Measure V))‖ ^ 2 ≤
        (C : ℝ) * ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi u‖ ^ 2) :
    Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal)

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Probability/LogConcave, Poincare/LocalSlope/Basic, L2/MeanVariance.

Selected supporting theorems: admissible_iff_memLp_gradient, apply_eq_norm_gradient, lowerSemicontinuous_sequentialRelaxation, sequentialRelaxation_ofLinearPMap_of_mem, sequentialRelaxation_ofLinearPMap_of_notMem.

Previous: norm_center_sq_sub_le · Next: literatureConstant_le_inv_of_tendsto.

Source excerpt, lines 345–349 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

open MeasureTheory Filter Topology InnerProductSpace
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 2 U)

theorem FunctionalInequalities.KLS.LogConcave.literatureConstant_le_of_gap_readable (C : NNReal)
    (hgap : ∀ u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain,
      ‖L2.center ν (u : Lp ℝ 2 (ν : Measure V))‖ ^ 2 ≤
        (C : ℝ) * ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi u‖ ^ 2) :
    Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal) := by sorry