Exact Relaxed Energy On The Closure Domain
ProvedFunctionalInequalities.Energy.PreEnergy.sequentialRelaxation_ofLinearPMap_of_mem_readableThis theorem identifies the sequential relaxation of a closable partial linear operator on the domain of its closure.
Let be a real normed space, let be a complete real Hilbert space, and let be closable. For every ,
The left side is the ENNReal-valued sequential relaxation of the pre-energy PreEnergy.ofLinearPMap T; the right side is the square of the NNReal norm, coerced to ENNReal. The declaration is sequentialRelaxation_ofLinearPMap_of_mem_readable, and the equality is asserted only for points in the closure domain.
Original Lean declaration header
Within namespace FunctionalInequalities.Energy.PreEnergy. Shown in its original module context. Proof omitted.
theorem sequentialRelaxation_ofLinearPMap_of_mem (hT : T.IsClosable) (x : T.closure.domain) :
(ofLinearPMap T).sequentialRelaxation x = (‖T.closure x‖₊ ^ 2 : NNReal)
Module navigation
Module: Energy/Relaxation/LinearPMap.
Definition modules: Energy/Form/Functional, Energy/Relaxation/Basic.
Supporting theorems: mem_closure_domain_of_frequently, sequentialRelaxation_ofLinearPMap_le.
Previous: sequentialRelaxation_ofLinearPMap_of_notMem.
Source excerpt, lines 358–359 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Relaxation_LinearPMap
variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
variable (T : X →ₗ.[ℝ] H)
theorem FunctionalInequalities.Energy.PreEnergy.sequentialRelaxation_ofLinearPMap_of_mem_readable (hT : T.IsClosable) (x : T.closure.domain) :
(ofLinearPMap T).sequentialRelaxation x = (‖T.closure x‖₊ ^ 2 : NNReal) := by sorry