Infinite Relaxed Energy Outside The Closure Domain

Proved

FunctionalInequalities.Energy.PreEnergy.sequentialRelaxation_ofLinearPMap_of_notMem_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem identifies the relaxed energy away from the domain of a closed operator.

Let $X$ be a real normed space, let $H$ be a complete real Hilbert space, and let $T:X\dashrightarrow H$ be closable. If $x\in X$ does not belong to the domain of the closure $\overline T$ , then the sequential relaxation of the pre-energy generated by $T$ is infinite:

x\notin\operatorname{dom}(\overline T) \quad\Longrightarrow\quad \operatorname{sequentialRelaxation}_{T}(x)=\top.

The value $\top$ is the top element of ENNReal, namely $+\infty$ . The declaration is sequentialRelaxation_ofLinearPMap_of_notMem_readable; it makes no assertion about points inside the closure domain.

Original Lean declaration header

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

theorem sequentialRelaxation_ofLinearPMap_of_notMem (hT : T.IsClosable) {x : X}
    (hx : x ∉ T.closure.domain) : (ofLinearPMap T).sequentialRelaxation x = ⊤

Module navigation

Module: Energy/Relaxation/LinearPMap.

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

Supporting theorems: mem_closure_domain_of_frequently.

Previous: mem_closure_domain_of_frequently · Next: sequentialRelaxation_ofLinearPMap_of_mem.

Source excerpt, lines 338–339 · Frozen source 408915f.

Preamble

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)

Formal statement


theorem FunctionalInequalities.Energy.PreEnergy.sequentialRelaxation_ofLinearPMap_of_notMem_readable (hT : T.IsClosable) {x : X}
    (hx : x ∉ T.closure.domain) : (ofLinearPMap T).sequentialRelaxation x = ⊤ := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Relaxation/LinearPMap.lean#L337-L355 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Relaxation.LinearPMap`, declaration `FunctionalInequalities.Energy.PreEnergy.sequentialRelaxation_ofLinearPMap_of_notMem`; the repository is private at upload time).

View graph