Frequently Bounded Approximations Lie In The Closure Domain

This theorem applies the closed-graph selection principle to a closable partially defined linear map.

Let $X$ be a real normed space, let $H$ be a complete real Hilbert space, and let $T:X\dashrightarrow H$ be a closable partial linear map. Let $x\in X$ and let $(f_n)$ be an approximating sequence for $x$ in the pre-energy generated by $T$. Assume that for some $L\in[0,\infty)$, represented by NNReal,

holds frequently along $n\to\infty$. Then $x$ belongs to the domain of the closure $\overline T$, and the closure value obeys

The declaration is mem_closure_domain_of_frequently_readable. The norm bound is stated using the nonnegative norm nnnorm; the conclusion includes both domain membership and the corresponding bound.

Original Lean declaration header

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

theorem mem_closure_domain_of_frequently (hT : T.IsClosable) {x : X}
    (f : (ofLinearPMap T).ApproximatingSequence x) {L : NNReal}
    (hL : ∃ᶠ n in atTop, ‖T (f.1 n)‖₊ ≤ L) :
    ∃ hx : x ∈ T.closure.domain, ‖T.closure ⟨x, hx⟩‖₊ ≤ L

Module navigation

Module: Energy/Relaxation/LinearPMap.

Definition modules: Energy/Relaxation/Basic.

Supporting theorems: exists_mem_of_isClosed_of_frequently_norm_le.

Previous: sequentialRelaxation_ofLinearPMap_le · Next: sequentialRelaxation_ofLinearPMap_of_notMem.

Source excerpt, lines 318–321 · Frozen source 408915f.