Relaxed Gradient Constants Imply Local-Slope Constants

This theorem transfers a Poincaré constant from the identity-weighted Lipschitz-gradient relaxation to the locally Lipschitz local-slope class.

Let $V$ be a finite-dimensional complete real inner-product normed space with its Borel measurable structure and second-countable topology. Let $\nu$ be a probability measure on $V$, let $m$ be an additive Haar measure, and assume

1. $\nu\ll m$;
2. $\nu(\partial\operatorname{supp}\nu)=0$;
3. for $C\in[0,\infty)$ represented by NNReal, the predicate Poincare.L2Energy.Holds ν (relaxation ν m (ν ≪ m)) C holds.

Then

The Lean declaration is localSlope_holds_of_relaxation_readable. The statement is an implication between the named formal predicates and does not claim that any Poincaré inequality holds without the stated hypothesis.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.LipschitzGradient. Shown in its original module context. Proof omitted.

theorem localSlope_holds_of_relaxation (hac : (ν : Measure V) ≪ m)
    (hfr : (ν : Measure V) (frontier (ν : Measure V).support) = 0) {C : NNReal}
    (h : Poincare.L2Energy.Holds ν (relaxation ν m hac) C) :
    Poincare.LocalSlope.Holds ν C

Module navigation

Module: Poincare/LipschitzGradient/Comparison.

Definition modules: Poincare/LocalSlope/Basic, Poincare/L2/Energy.

Supporting theorems: admissible_iff_memLp_gradient, apply_eq_norm_gradient.

Previous: holds_ofPreEnergy_of_localSlope · Next: constant_eq_lipschitz.

Source excerpt, lines 94–97 · Frozen source 408915f.