Relaxed Energy Bounded By The Closed-Operator Energy
ProvedFunctionalInequalities.Energy.PreEnergy.sequentialRelaxation_ofLinearPMap_le_readableThis theorem gives the upper bound for the sequential relaxation of a closable partial linear operator.
Let be a real normed space, let be a real inner-product space, and let be closable. For every in the domain of the closure , the sequential relaxation of the pre-energy generated by satisfies
Here denotes the nonnegative norm represented by NNReal, and the right-hand side is coerced to ENNReal. The declaration is sequentialRelaxation_ofLinearPMap_le_readable; completeness of the Hilbert target is not required in the declaration's explicit type.
Original Lean declaration header
Within namespace FunctionalInequalities.Energy.PreEnergy. Shown in its original module context. Proof omitted.
theorem sequentialRelaxation_ofLinearPMap_le (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.
Previous: exists_mem_of_isClosed_of_frequently_norm_le · Next: mem_closure_domain_of_frequently.
Source excerpt, lines 298–299 · 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)
omit [CompleteSpace H]
theorem FunctionalInequalities.Energy.PreEnergy.sequentialRelaxation_ofLinearPMap_le_readable (hT : T.IsClosable) (x : T.closure.domain) :
(ofLinearPMap T).sequentialRelaxation x ≤ (‖T.closure x‖₊ ^ 2 : NNReal) := by sorry