Graph Convergence Transfers Through a Closed Operator

This is a graph-convergence lemma for $T^\dagger T$.

Let $H_0,H_1$ be real inner-product spaces, let $T:H_0\to H_1$ be a linear partial map, and assume that $D(T)$ is dense in $H_0$. Let $x_n\in D(T^\dagger T)$ and $y\in D(T^\dagger T)$. If

1. $x_n\to y$ in $H_0$, and
2. $T^\dagger T x_n\to T^\dagger T y$ in $H_0$,

then

This is a technical von Neumann-type continuity statement for the graph of $T^\dagger T$.

Formalization Note. The sequence is indexed by $\mathbb N$, and the operator values are represented using subtype witnesses for domain membership.

Original Lean declaration header

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

theorem tendsto_apply_of_tendsto_adjointComp {T : H₀ →ₗ.[ℝ] H₁}
    (hd : Dense (T.domain : Set H₀)) {x : ℕ → (adjointComp T).domain}
    {y : (adjointComp T).domain} (h0 : Tendsto (fun n => (x n : H₀)) atTop (𝓝 (y : H₀)))
    (h1 : Tendsto (fun n => adjointComp T (x n)) atTop (𝓝 (adjointComp T y))) :
    Tendsto (fun n => T ⟨(x n : H₀), (x n).2.2⟩) atTop (𝓝 (T ⟨(y : H₀), y.2.2⟩))

Module navigation

Module: Analysis/Semigroup/VonNeumann.

Definition modules: Analysis/Semigroup/AdjointComp.

Source excerpt, lines 203–207 · Frozen source 408915f.