Operator-Domain Bounds from a Kernel-Complement Gap

This is the norm and energy estimate obtained from a gap inequality.

Let $H_0,H_1$ be real Hilbert spaces, let $T:H_0\to H_1$ be a linear partial map with dense domain, and let $A=T^\dagger T$. Fix $C\in\mathbb{R}$. Assume that every $y\in D(T)$ orthogonal to $\ker T$ satisfies

For every $u\in D(A)$ orthogonal to $\ker T$, the conclusion is

The statement includes the case of arbitrary real $C$; no positivity assumption on $C$ appears in the type.

Original Lean declaration header

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

theorem norm_le_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)
    (u : (adjointComp T).domain)
    (hu : ∀ k : T.domain, T k = 0 → ⟪(u : H₀), (k : H₀)⟫ = 0) :
    ‖(u : H₀)‖ ≤ C * ‖adjointComp T u‖ ∧
      ‖T ⟨(u : H₀), u.2.2⟩‖ ^ 2 = ⟪adjointComp T u, (u : H₀)⟫ ∧
      ⟪adjointComp T u, (u : H₀)⟫ ≤ C * ‖adjointComp T u‖ ^ 2

Module navigation

Module: Analysis/Semigroup/Generated/Inverse.

Definition modules: Analysis/Semigroup/AdjointComp.

Next: exists_adjointComp_eq_of_gap.

Source excerpt, lines 27–34 · Frozen source 408915f.