Spectrum inside the closure of the numerical range (L2.2)

σ(A) ⊆ closure W(A) for a continuous linear operator A on a complex Hilbert space.

Route (task-spec L2.2): if λ ∉ closure W(A), there is d > 0 with d ≤ ‖⟪x, A x⟫_ℂ - λ‖ for every unit vector x, i.e. d ≤ ‖⟪x, B x⟫_ℂ‖ for B = A - λ • 1. By homogeneity and Cauchy–Schwarz this gives d * ‖x‖ ≤ ‖B x‖ for all x (norm_apply_ge_of_forall_unit), and likewise for B†, since ⟪x, B† x⟫_ℂ = conj ⟪x, B x⟫_ℂ. An operator bounded below is injective with closed range, and its adjoint being bounded below makes the range dense; so B is bijective, hence a unit (isUnit_of_forall_norm_le), i.e. λ ∉ σ(A).

Main declarations

• norm_apply_ge_of_forall_unit — a lower bound d ≤ ‖⟪x, B x⟫_ℂ‖ on unit vectors gives d * ‖x‖ ≤ ‖B x‖ for all x.
• isUnit_of_forall_norm_le — an operator bounded below whose adjoint is bounded below is a unit.
• spectrum_subset_closure_numericalRange — σ(A) ⊆ closure W(A).

The proof was written by agent-alpha (.sessions/agent-alpha/SpikeL22.lean) and moved to production, with one rewrite direction fixed, by agent-alpha-2.

Requires [CompleteSpace E] (adjoints and the spectrum of E →L[ℂ] E).

theorem norm_apply_ge_of_forall_unit {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (B : E →L[ℂ] E) {d : ℝ} (h : ∀ (x : E), ‖x‖ = 1 → d ≤ ‖inner ℂ x (B x)‖) (x : E) : d * ‖x‖ ≤ ‖B x‖

A lower bound d ≤ ‖⟪x, B x⟫_ℂ‖ on unit vectors gives d * ‖x‖ ≤ ‖B x‖ for all x (homogeneity of the quadratic form, then Cauchy–Schwarz).

theorem isUnit_of_forall_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B : E →L[ℂ] E) {d : ℝ} (hd : 0 < d) (hB : ∀ (x : E), d * ‖x‖ ≤ ‖B x‖) (hB' : ∀ (x : E), d * ‖x‖ ≤ ‖(ContinuousLinearMap.adjoint B) x‖) : IsUnit B

An operator bounded below (d * ‖x‖ ≤ ‖B x‖, d > 0) whose adjoint is bounded below is a unit: it is injective with closed range, and the range is dense because its orthogonal complement is the kernel of the adjoint.

theorem spectrum_subset_closure_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : spectrum ℂ A ⊆ closure (numericalRange A)

The spectrum of A is contained in the closure of its numerical range.