Uniqueness on the Orthogonal Complement of the Kernel

This is a uniqueness lemma for the operator $A=T^\dagger T$.

Let $H_0,H_1$ be real Hilbert spaces, with $H_0$ complete, and let $T:H_0\to H_1$ be a linear partial map whose domain is dense in $H_0$. Let $u,v$ belong to the domain of adjointComp T, and assume:

1. $u$ is orthogonal to every $k\in D(T)$ satisfying $Tk=0$.
2. $v$ is orthogonal to every such $k$.
3. $Au=Av$, where $A=\operatorname{adjointComp}(T)$.

Then

The conclusion identifies two operator-domain vectors with the same image under $T^\dagger T$ once both are orthogonal to $\ker T$.

Original Lean declaration header

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

theorem eq_of_adjointComp_eq (u v : (adjointComp T).domain)
    (hu : ∀ k : T.domain, T k = 0 → ⟪(u : H₀), (k : H₀)⟫ = 0)
    (hv : ∀ k : T.domain, T k = 0 → ⟪(v : H₀), (k : H₀)⟫ = 0)
    (huv : adjointComp T u = adjointComp T v) : (u : H₀) = v

Module navigation

Module: Analysis/Semigroup/Generated/Inverse.

Definition modules: Analysis/Semigroup/AdjointComp.

Previous: exists_adjointComp_eq_of_gap.

Source excerpt, lines 240–243 · Frozen source 408915f.