Orthogonality to the Kernel Implies Closure of the Range

This is a range-closure characterization for $A=T^\dagger T$.

Let $H_0,H_1$ be complete real Hilbert spaces, let $T:H_0\to H_1$ be closed, and assume $D(T)$ is dense in $H_0$. If $g\in H_0$ satisfies

for every $k\in D(A)$ with $Ak=0$, where $A=\operatorname{adjointComp}(T)$, then

The closure is taken in $H_0$. This is a standard Hilbert-space ingredient for approximation by the range of a self-adjoint operator.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Semigroup.Generated. Shown in its original module context. Proof omitted.

theorem mem_closure_range_of_inner_eq_zero (g : H₀)
    (hg : ∀ k : (adjointComp T).domain, adjointComp T k = 0 → ⟪g, (k : H₀)⟫ = 0) :
    g ∈ closure (Set.range fun y : (adjointComp T).domain => adjointComp T y)

Module navigation

Module: Analysis/Semigroup/Generated/Convergence.

Definition modules: Analysis/Semigroup/AdjointComp.

Supporting theorems: exists_mem_adjointComp_domain_of_inner_eq_zero.

Previous: exists_mem_adjointComp_domain_of_inner_eq_zero · Next: tendsto_apply_adjointComp.

Source excerpt, lines 102–104 · Frozen source 408915f.