Recovery Sequence At A Finite Relaxed-Energy Point
ProvedFunctionalInequalities.Energy.PreEnergy.hasRecoverySequenceAt_sequentialRelaxation_of_finiteAt_readableThis theorem gives a recovery sequence wherever a sequential relaxation is finite.
Let be a pseudometric space, let be a pre-energy, and let . Assume
meaning that the relaxed energy at is not . Then there exists an approximating sequence of concrete tests converging to whose energies converge in the liminf/limsup sense encoded by HasRecoverySequenceAt:
The declaration is hasRecoverySequenceAt_sequentialRelaxation_of_finiteAt_readable. It is a general sequential-relaxation result and assumes neither quadraticity nor a Markov property; finiteness at the point is an explicit hypothesis.
Original Lean declaration header
Within namespace FunctionalInequalities.Energy.PreEnergy. Shown in its original module context. Proof omitted.
theorem hasRecoverySequenceAt_sequentialRelaxation_of_finiteAt {x : X}
(hfinite : P.sequentialRelaxation.FiniteAt x) :
P.HasRecoverySequenceAt P.sequentialRelaxation x
Module navigation
Module: Energy/Relaxation/Recovery.
Definition modules: Energy/Form/Core, Energy/Form/Functional, Energy/Relaxation/Basic.
Supporting theorems: exists_test_near_of_relaxation_lt.
Source excerpt, lines 34–36 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Relaxation_Recovery
universe u
variable {X : Type u} [PseudoMetricSpace X] (P : FunctionalInequalities.Energy.PreEnergy X)
theorem FunctionalInequalities.Energy.PreEnergy.hasRecoverySequenceAt_sequentialRelaxation_of_finiteAt_readable {x : X}
(hfinite : P.sequentialRelaxation.FiniteAt x) :
P.HasRecoverySequenceAt P.sequentialRelaxation x := by sorry