Approximate Eigenvectors at the Bottom of the Operator Spectrum

This is an approximate-eigenvector construction for $A=T^\dagger T$.

Let $H_0,H_1$ be complete real Hilbert spaces, let $T:H_0\to H_1$ be closed with dense domain, and let $\lambda,\eta\in\mathbb{R}$ with $\lambda>0$. Assume:

1. For every $y\in D(T)$ orthogonal to $\ker T$, $\lambda\|y\|^2\le\|Ty\|^2$.
2. $y\in D(T)$ is orthogonal to $\ker T$.
3. $\|y\|=1$.
4. $\|Ty\|^2\le\lambda(1+\eta)$.

Then there exists $z\in D(A)$, orthogonal to $\ker T$, such that

The theorem does not assume $\eta\ge0$ in its type and does not assert the existence of an exact eigenvector.

Original Lean declaration header

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

theorem exists_approx_eigenvector_of_gap (T : H₀ →ₗ.[ℝ] H₁) (hT : T.IsClosed)
    (hd : Dense (T.domain : Set H₀)) {lam η : ℝ} (hlam : 0 < lam)
    (hgap : ∀ y : T.domain, (∀ k : T.domain, T k = 0 → ⟪(y : H₀), (k : H₀)⟫ = 0) →
      lam * ‖(y : H₀)‖ ^ 2 ≤ ‖T y‖ ^ 2)
    (y : T.domain) (hy : ∀ k : T.domain, T k = 0 → ⟪(y : H₀), (k : H₀)⟫ = 0)
    (hy1 : ‖(y : H₀)‖ = 1) (hTy : ‖T y‖ ^ 2 ≤ lam * (1 + η)) :
    ∃ z : (adjointComp T).domain,
      (∀ k : T.domain, T k = 0 → ⟪(z : H₀), (k : H₀)⟫ = 0) ∧
      ‖(y : H₀) - (z : H₀)‖ ≤ Real.sqrt (η / 8) ∧
      ‖adjointComp T z - lam • (z : H₀)‖ ≤ lam * Real.sqrt (η / 2)

Module navigation

Module: Analysis/Semigroup/Generated/ApproximateEigenvector.

Definition modules: Analysis/Semigroup/AdjointComp.

Source excerpt, lines 55–64 · Frozen source 408915f.