Covariance Relaxation Bound by Lipschitz Relaxation

This bounds the covariance relaxation by the covariance operator norm times the Lipschitz-gradient relaxation.

Let $V$ be a finite-dimensional complete real inner-product space with its Borel measurable structure, let $\nu$ be a probability measure, and let $m$ be an additive Haar measure. Assume that $\nu\ll m$ and that the frontier of the support of $\nu$ has $\nu$-measure zero. For any $f\in L^2(\nu)$ whose Lipschitz-gradient relaxation is finite,

Here $\|\operatorname{Cov}(\nu)\|_{+}$ is the nonnegative norm value coerced to $[0,\infty]$.

This is an energy comparison, not an assertion that either relaxation is finite or that a Poincaré inequality holds.

Formalization Note The inequality is in ENNReal; the finiteness assumption is precisely that the Lipschitz relaxation is not top.

Original Lean declaration header

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

theorem relaxation_le_mul_lipschitz (hac : (ν : Measure V) ≪ m)
    (hfr : (ν : Measure V) (frontier (ν : Measure V).support) = 0) (f : Lp ℝ 2 (ν : Measure V))
    (hf : Energy.LipschitzGradient.relaxation ν m hac f ≠ ⊤) :
    relaxation ν f ≤
      (‖Covariance.operator (ν : Measure V)‖₊ : ENNReal) * Energy.LipschitzGradient.relaxation ν m hac f

Module navigation

Module: Poincare/LipschitzGradient/Comparison.

Definition modules: Probability/Covariance/Basic, Energy/Form/Functional, Energy/CovarianceGradient/Basic.

Supporting theorems: relaxation_eq_ofLinearPMap, sequentialRelaxation_comp_le_mul, exists_norm_sq_eq_inner_of_isSymmetric.

Previous: constant_eq_lipschitz.

Source excerpt, lines 211–215 · Frozen source 408915f.