Closed Unit-Gradient Gap From a Literature Poincaré Bound

This statement transfers a finite literature Poincaré bound to the domain of the closed unit gradient.

Let $V$ be a finite-dimensional complete real inner product space with its Borel measurable structure and a second-countable topology. Let $m$ be an additive Haar measure and $\nu$ a log-concave probability measure with $\operatorname{int}(\operatorname{supp}\nu)\ne\varnothing$. Set $T=$ KLS.LogConcave.closedWeightedOperator for $m$ and the identity weight. Assume $C\in[0,\infty)$ and $C_P^{\mathrm{lit}}(\nu)\le C$, where $C_P^{\mathrm{lit}}$ is Poincare.LocalSlope.Intrinsic.constant.

For every $u\in D(T)$,

Here centering is L2.center. This provides the form-domain gap for the actual closed gradient, rather than only for smooth tests.

Formalization Note $C$ is NNReal; its ENNReal coercion occurs in the hypothesis, and its real coercion in the conclusion. There is no factor of $1/2$ in the squared-gradient term.

Original Lean declaration header

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

theorem closedWeightedOperator_id_gap_of_literature_le (C : NNReal)
    (hC : Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
    (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

Module navigation

Module: KLS/LogConcave/WeightedGradient/Poincare.

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

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

Source excerpt, lines 40–44 · Frozen source 408915f.