Smooth Relaxation Bound by Asymptotic-Lipschitz Energy

This statement formalizes the smooth-recovery inequality for a globally Lipschitz test.

Let $V$ be a finite-dimensional real inner-product space with complete Borel measurable and second-countable structure. Let $\nu$ be a probability measure on $V$, let $g:V\to\mathbb R$, and let $K\in[0,\infty)$. Assume:

1. $g$ is globally $K$-Lipschitz, expressed by LipschitzWith K g.
2. $g$ belongs to $L^2(\nu)$, expressed by MemLp g 2 (\nu : Measure V).

Then the smooth-gradient relaxation of the $L^2(\nu)$ class of $g$ is bounded above by its asymptotic-Lipschitz energy:

Both sides are extended-valued energies in $[0,\infty]$. This is a reusable smooth-recovery estimate for globally Lipschitz functions.

Original Lean declaration header

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

theorem relaxation_le_asymptoticLipschitz_of_lipschitzWith (ν : ProbabilityMeasure V)
    {g : V → ℝ} {K : ℝ≥0} (hlip : LipschitzWith K g) (hmem : MemLp g 2 (ν : Measure V)) :
    relaxation ν (hmem.toLp g) ≤ AsymptoticLipschitz.energy ν g

Module navigation

Module: Energy/Euclidean/Slope/Recovery.

Definition modules: Energy/Form/Functional, Energy/LocalSlope/Relaxation, Energy/SmoothGradient/Basic.

Supporting theorems: limsup_enorm_gradient_mollify_le.

Previous: limsup_enorm_gradient_mollify_le.

Source excerpt, lines 559–561 · Frozen source 408915f.