Solvability of the Adjoint-Composition Equation

This is an existence theorem for the equation $Au=g$ on the orthogonal complement of $\ker T$.

Let $H_0,H_1$ be complete real Hilbert spaces, let $T:H_0\to H_1$ be closed with dense domain, and write $A=T^\dagger T$. Fix $C\in\mathbb{R}$ and assume the gap condition

for every $y\in D(T)$ orthogonal to $\ker T$. If $g\in H_0$ is orthogonal to every $k\in D(T)$ with $Tk=0$, then there exists $u\in D(A)$ such that

This provides existence of an inverse on the kernel complement; uniqueness is supplied by the corresponding uniqueness lemma.

Original Lean declaration header

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

theorem exists_adjointComp_eq_of_gap {C : ℝ}
    (hgap : ∀ y : T.domain, (∀ k : T.domain, T k = 0 → ⟪(y : H₀), (k : H₀)⟫ = 0) →
      ‖(y : H₀)‖ ^ 2 ≤ C * ‖T y‖ ^ 2)
    (g : H₀) (hg : ∀ k : T.domain, T k = 0 → ⟪g, (k : H₀)⟫ = 0) :
    ∃ u : (adjointComp T).domain,
      (∀ k : T.domain, T k = 0 → ⟪(u : H₀), (k : H₀)⟫ = 0) ∧ adjointComp T u = g

Module navigation

Module: Analysis/Semigroup/Generated/Inverse.

Definition modules: Analysis/Semigroup/AdjointComp.

Supporting theorems: mem_closure_range_of_inner_eq_zero, norm_le_of_gap.

Previous: norm_le_of_gap · Next: eq_of_adjointComp_eq.

Source excerpt, lines 153–158 · Frozen source 408915f.