Concrete Test Below A Strict Relaxed-Energy Bound

This is an approximation-selection lemma for sequential relaxation.

Let $X$ be a pseudometric space, let $P$ be a pre-energy on $X$, let $x\in X$, and let $B\in[0,\infty]$ be an ENNReal bound. Assume the relaxed energy is strictly below $B$:

For every real radius $\varepsilon>0$, there exists a concrete test $f\in P.\operatorname{Test}$ such that

The Lean declaration is exists_test_near_of_relaxation_lt_readable. The strict relaxed-energy hypothesis and strict energy conclusion are essential parts of the statement; it does not assert attainment of a minimum.

Original Lean declaration header

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

theorem exists_test_near_of_relaxation_lt {x : X} {bound : ENNReal}
    (hbound : P.sequentialRelaxation x < bound) {ε : ℝ} (hε : 0 < ε) :
    ∃ f : P.Test, dist (P.toAmbient f) x < ε ∧ (P.energy f : ENNReal) < bound

Module navigation

Module: Energy/Relaxation/Approximation.

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

Source excerpt, lines 31–33 · Frozen source 408915f.