Restricted point spectra and point-spectral subspaces

Let A be an endomorphism of a vector space E over 𝕜 = ℝ or ℂ. This file sets up the basis-free vocabulary in which spectral-subspace perturbation estimates are stated.

• The restricted point spectrum A.restrictedPointSpectrum U of A on a subspace U is the set of real λ for which some nonzero x ∈ U satisfies A x = λ x. The subspace U need not be invariant under A.
• A.PointSpectrumIn U Ω says that this restricted point spectrum is contained in a set Ω ⊆ ℝ.
• The point-spectral subspace A.pointSpectralSubspace Ω is the sum of the eigenspaces of A at the eigenvalues λ ∈ Ω, that is, the span of the eigenvectors with eigenvalue in Ω.

Eigenspaces for distinct eigenvalues are independent, so an eigenvector lying in A.pointSpectralSubspace Ω has its eigenvalue in Ω: the point-spectral subspace selected by Ω carries only point spectrum in Ω (Module.End.pointSpectrumIn_pointSpectralSubspace). This holds for every endomorphism, in any dimension.

For a symmetric operator on a finite-dimensional inner product space, the eigenspaces at real eigenvalues are mutually orthogonal and span E. Hence the point-spectral subspaces selected by Ω and by its complement are orthogonal complements of each other, the point-spectral subspace is the span of the vectors of an ordered eigenbasis whose eigenvalues lie in Ω, and its orthogonal projection is the functional calculus 𝟙_Ω(A) of the indicator function of Ω. When A is moreover injective, its negative and positive spectral subspaces are complementary. The quadratic form x ↦ re ⟪A x, x⟫ is negative definite on the negative spectral subspace A.pointSpectralSubspace (Iio 0) and positive definite on the positive spectral subspace A.pointSpectralSubspace (Ioi 0).

On a finite-dimensional subspace invariant under a symmetric operator, point-spectral containment is equivalent to a quadratic-form bound: the restricted point spectrum lies in (-∞, a] exactly when re ⟪A x, x⟫ ≤ a ‖x‖² on the subspace, and in [a, ∞) exactly when a ‖x‖² ≤ re ⟪A x, x⟫ there. The implication from the form bound to the spectral containment needs neither symmetry, invariance, nor finite dimensionality.

Perturbation bounds for spectral subspaces assume that the spectral data being compared are separated. Three forms of this hypothesis are named here, all stated over restricted point spectra of two operators A on E and B on F: a separation δ ≤ |μ - ν| with no ordering, an ordered gap μ + δ ≤ ν, and an interval/exterior gap, where the spectrum of A lies in [a, b] and that of B outside (a - δ, b + δ). The latter two imply the first. An internal gap additionally records invariance of a subspace and separation of its point spectrum from that of its orthogonal complement.

Main definitions

• Module.End.restrictedPointSpectrum A U: the real eigenvalues of A with an eigenvector in U.
• Module.End.PointSpectrumIn A U Ω: the restricted point spectrum of A on U lies in Ω.
• Module.End.pointSpectralSubspace A Ω: the sum of the eigenspaces of A at eigenvalues in Ω.
• Module.End.PointSpectraSeparated A U B V δ: the restricted point spectra of A on U and of B on V are at distance at least δ.
• Module.End.PointOrderedGap A U B V δ: the first lies below the second with margin δ.
• Module.End.PointIntervalExteriorGap A U B V a b δ: the first lies in [a, b] and the second outside (a - δ, b + δ).
• Module.End.PointInternalGap A U δ: invariance of U together with spectral separation between U and its orthogonal complement.

Main statements

• Module.End.mem_restrictedPointSpectrum_iff: λ lies in the restricted point spectrum on U exactly when A x = λ x for some nonzero x ∈ U.
• Module.End.pointSpectrumIn_pointSpectralSubspace: the point-spectral subspace selected by Ω has restricted point spectrum in Ω.
• Module.End.pointSpectralSubspace_conj: conjugating by a linear equivalence transports the point-spectral subspaces.
• Module.End.map_pointSpectralSubspace_le_of_commute: an endomorphism commuting with A preserves the point-spectral subspaces of A.
• LinearMap.IsSymmetric.orthogonal_pointSpectralSubspace: for symmetric A in finite dimension, (A.pointSpectralSubspace Ω)ᗮ = A.pointSpectralSubspace Ωᶜ.
• LinearMap.IsSymmetric.orthogonal_pointSpectralSubspace_Iio_zero and LinearMap.IsSymmetric.orthogonal_pointSpectralSubspace_Ioi_zero: for injective symmetric A, the negative and positive spectral subspaces are orthogonal complements.
• LinearMap.IsSymmetric.pointSpectralSubspace_eq_eigenvectorSpan: the point-spectral subspace is spanned by the vectors of the ordered eigenbasis whose eigenvalues lie in Ω.
• LinearMap.IsSymmetric.coe_starProjection_pointSpectralSubspace: its orthogonal projection is the functional calculus of the indicator function of Ω.
• LinearMap.IsSymmetric.re_inner_apply_self_lt_zero_of_mem_pointSpectralSubspace and LinearMap.IsSymmetric.re_inner_apply_self_pos_of_mem_pointSpectralSubspace: the quadratic form of a symmetric operator is negative definite on its point-spectral subspaces selected by negative reals, and positive definite on those selected by positive reals.
• LinearMap.IsSymmetric.eq_starProjection_pointSpectralSubspace_Iio_zero: for injective symmetric A, an idempotent commuting with A, with the form of A negative definite on its range and positive definite on its kernel, is the orthogonal projection onto the negative spectral subspace.
• ContinuousLinearMap.abs_le_norm_of_mem_restrictedPointSpectrum: every real eigenvalue of a bounded operator T has absolute value at most ‖T‖.
• LinearMap.IsSymmetric.pointSpectrumIn_Iic_iff, LinearMap.IsSymmetric.pointSpectrumIn_Ici_iff: on a finite-dimensional invariant subspace, point-spectral containment in a half-line is a quadratic-form bound.
• LinearMap.IsSymmetric.re_inner_apply_self_nonneg_of_mem_pointSpectralSubspace: in finite dimensions, the quadratic form of a symmetric operator is positive semidefinite on its point-spectral subspaces selected by nonnegative reals.
• LinearMap.IsSymmetric.norm_apply_sub_smul_le_of_pointSpectrumIn, LinearMap.IsSymmetric.mul_norm_le_norm_apply_sub_smul_of_pointSpectrumIn: on a finite-dimensional invariant subspace, if every eigenvalue lies within r of c then ‖T x - c x‖ ≤ r ‖x‖, and if every eigenvalue is at distance at least r from c then r ‖x‖ ≤ ‖T x - c x‖.
• Module.End.PointOrderedGap.pointSpectraSeparated, Module.End.PointIntervalExteriorGap.pointSpectraSeparated: ordered and interval/exterior gaps are separations.
• Module.End.pointSpectrumIn_orthogonal_pointSpectralSubspace: the orthogonal complement of a point-spectral subspace has no eigenvectors with eigenvalues in the selected set.
• Module.End.pointInternalGap_pointSpectralSubspace: a point-spectral subspace of any endomorphism has an internal gap when its selected and complementary actual eigenvalues are separated by the stated margin.
• Module.End.PointOrderedGap.of_pointSpectrumIn, Module.End.PointOrderedGap.of_re_inner_apply_self: containment on opposite sides of a cut, or opposite quadratic-form bounds, give an ordered gap.
• Module.End.PointIntervalExteriorGap.of_re_inner_apply_self: an upper quadratic-form bound for a bounded operator T on U and a lower one for B on V give an interval/exterior gap with interval [-‖T‖, a].
• Module.End.exists_pos_pointSpectraSeparated_iff_disjoint: in finite dimension, two restricted point spectra are separated by a positive distance exactly when they are disjoint.
• LinearMap.IsSymmetric.eigenvalues_ne_eigenvalues_of_disjoint: for symmetric A and B with disjoint point spectra, eigenbasis eigenvalues of A and of B are distinct.

References

• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970), 1–46.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer (1997), §VII.3.

The restricted point spectrum

def Module.End.restrictedPointSpectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] (A : End 𝕜 E) (U : Submodule 𝕜 E) : Set ℝ

The restricted point spectrum of A on a subspace U: the real numbers λ for which A has an eigenvector in U with eigenvalue λ. The subspace U need not be invariant.

theorem Module.End.mem_restrictedPointSpectrum_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {μ : ℝ} : μ ∈ A.restrictedPointSpectrum U ↔ ∃ x ∈ U, x ≠ 0 ∧ A x = ↑μ • x

A real number lies in the restricted point spectrum of A on U exactly when A x = μ x for some nonzero x ∈ U.

theorem Module.End.mem_restrictedPointSpectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {μ : ℝ} {x : E} (hxU : x ∈ U) (hx0 : x ≠ 0) (hx : A x = ↑μ • x) : μ ∈ A.restrictedPointSpectrum U

A nonzero vector x ∈ U with A x = μ x places μ in the restricted point spectrum of A on U.

theorem Module.End.mem_restrictedPointSpectrum_iff_inf_eigenspace_ne_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {μ : ℝ} : μ ∈ A.restrictedPointSpectrum U ↔ U ⊓ A.eigenspace ↑μ ≠ ⊥

A real number lies in the restricted point spectrum of A on U exactly when U meets the corresponding eigenspace of A nontrivially.

theorem Module.End.restrictedPointSpectrum_mono {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {U V : Submodule 𝕜 E} (hUV : U ≤ V) : A.restrictedPointSpectrum U ⊆ A.restrictedPointSpectrum V

The restricted point spectrum is monotone in the subspace.

@[simp]

theorem Module.End.restrictedPointSpectrum_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} : A.restrictedPointSpectrum ⊥ = ∅

The restricted point spectrum on the zero subspace is empty.

@[simp]

theorem Module.End.restrictedPointSpectrum_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} : A.restrictedPointSpectrum ⊤ = {μ : ℝ | A.HasEigenvalue ↑μ}

The restricted point spectrum on the whole space is the set of real eigenvalues.

Point-spectral containment

def Module.End.PointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] (A : End 𝕜 E) (U : Submodule 𝕜 E) (Ω : Set ℝ) : Prop

A.PointSpectrumIn U Ω says that every real eigenvalue of A carried by an eigenvector in U lies in Ω.

theorem Module.End.pointSpectrumIn_iff_restrictedPointSpectrum_subset {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {Ω : Set ℝ} : A.PointSpectrumIn U Ω ↔ A.restrictedPointSpectrum U ⊆ Ω

Point-spectral containment is equivalent to inclusion of the restricted point spectrum. This provides the subset characterization without unfolding PointSpectrumIn in client modules.

theorem Module.End.pointSpectrumIn_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {Ω : Set ℝ} : A.PointSpectrumIn U Ω ↔ ∀ x ∈ U, x ≠ 0 → ∀ (μ : ℝ), A x = ↑μ • x → μ ∈ Ω

Point-spectral containment in Ω says that A x = μ x with x ∈ U nonzero forces μ ∈ Ω.

theorem Module.End.PointSpectrumIn.mono {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {U V : Submodule 𝕜 E} {Ω Ω' : Set ℝ} (h : A.PointSpectrumIn V Ω) (hUV : U ≤ V) (hΩ : Ω ⊆ Ω') : A.PointSpectrumIn U Ω'

Point-spectral containment passes to smaller subspaces and larger sets of values.

Point-spectral subspaces

def Module.End.pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] (A : End 𝕜 E) (Ω : Set ℝ) : Submodule 𝕜 E

The point-spectral subspace of A selected by Ω ⊆ ℝ: the sum of the eigenspaces of A at the eigenvalues in Ω, that is, the span of the eigenvectors whose eigenvalue lies in Ω (Module.End.pointSpectralSubspace_eq_span).

theorem Module.End.pointSpectralSubspace_eq_iSup {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω : Set ℝ} : A.pointSpectralSubspace Ω = ⨆ μ ∈ Ω, A.eigenspace ↑μ

The point-spectral subspace selected by Ω is the supremum of the eigenspaces of A at the eigenvalues in Ω.

theorem Module.End.pointSpectralSubspace_le_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {V : Submodule 𝕜 E} {Ω : Set ℝ} : A.pointSpectralSubspace Ω ≤ V ↔ ∀ μ ∈ Ω, A.eigenspace ↑μ ≤ V

The point-spectral subspace selected by Ω lies in V exactly when every eigenspace of A at an eigenvalue in Ω does.

theorem Module.End.eigenspace_le_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {μ : ℝ} {Ω : Set ℝ} (hμ : μ ∈ Ω) : A.eigenspace ↑μ ≤ A.pointSpectralSubspace Ω

The eigenspace of A at an eigenvalue in Ω lies in the point-spectral subspace.

theorem Module.End.pointSpectralSubspace_eq_span {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω : Set ℝ} : A.pointSpectralSubspace Ω = Submodule.span 𝕜 {x : E | ∃ μ ∈ Ω, A.HasEigenvector (↑μ) x}

The point-spectral subspace selected by Ω is the span of the eigenvectors of A whose eigenvalues lie in Ω.

theorem Module.End.pointSpectralSubspace_mono {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω Ω' : Set ℝ} (h : Ω ⊆ Ω') : A.pointSpectralSubspace Ω ≤ A.pointSpectralSubspace Ω'

The point-spectral subspace is monotone in the selected set of eigenvalues.

@[simp]

theorem Module.End.pointSpectralSubspace_empty {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} : A.pointSpectralSubspace ∅ = ⊥

The point-spectral subspace selected by the empty set is zero.

@[simp]

theorem Module.End.pointSpectralSubspace_union {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω Ω' : Set ℝ} : A.pointSpectralSubspace (Ω ∪ Ω') = A.pointSpectralSubspace Ω ⊔ A.pointSpectralSubspace Ω'

The point-spectral subspace of a union is the sum of the two point-spectral subspaces.

theorem Module.End.map_pointSpectralSubspace_le_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω : Set ℝ} {B : End 𝕜 E} (h : Commute A B) : Submodule.map B (A.pointSpectralSubspace Ω) ≤ A.pointSpectralSubspace Ω

An endomorphism commuting with A maps each point-spectral subspace of A into itself, since it maps each eigenspace of A into itself.

theorem Module.End.map_pointSpectralSubspace_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω : Set ℝ} : Submodule.map A (A.pointSpectralSubspace Ω) ≤ A.pointSpectralSubspace Ω

An endomorphism maps each of its point-spectral subspaces into itself.

theorem Module.End.map_pointSpectralSubspace_le_of_comp_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {E' : Type u_3} [AddCommGroup E'] [Module 𝕜 E'] {B : End 𝕜 E'} (U : E →ₗ[𝕜] E') (hU : B ∘ₗ U = U ∘ₗ A) (Ω : Set ℝ) : Submodule.map U (A.pointSpectralSubspace Ω) ≤ B.pointSpectralSubspace Ω

A linear map intertwining two endomorphisms carries each point-spectral subspace of the first into the corresponding point-spectral subspace of the second.

theorem Module.End.map_pointSpectralSubspace_of_comp_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {E' : Type u_3} [AddCommGroup E'] [Module 𝕜 E'] {B : End 𝕜 E'} (U : E ≃ₗ[𝕜] E') (hU : B ∘ₗ ↑U = ↑U ∘ₗ A) (Ω : Set ℝ) : Submodule.map (↑U) (A.pointSpectralSubspace Ω) = B.pointSpectralSubspace Ω

A linear equivalence intertwining two endomorphisms carries each point-spectral subspace of the first onto the corresponding point-spectral subspace of the second.

theorem Module.End.disjoint_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω Ω' : Set ℝ} (h : Disjoint Ω Ω') : Disjoint (A.pointSpectralSubspace Ω) (A.pointSpectralSubspace Ω')

Point-spectral subspaces selected by disjoint sets are disjoint, because eigenspaces for distinct eigenvalues are independent.

theorem Module.End.pointSpectrumIn_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] (A : End 𝕜 E) (Ω : Set ℝ) : A.PointSpectrumIn (A.pointSpectralSubspace Ω) Ω

Spectral containment of point-spectral subspaces. An eigenvector of A lying in the point-spectral subspace selected by Ω has its eigenvalue in Ω.

@[simp]

theorem Module.End.pointSpectralSubspace_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω : Set ℝ} : (-A).pointSpectralSubspace Ω = A.pointSpectralSubspace (-Ω)

The point-spectral subspace of -A selected by Ω is the point-spectral subspace of A selected by -Ω.

theorem Module.End.pointSpectralSubspace_conj {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω : Set ℝ} {E' : Type u_3} [AddCommGroup E'] [Module 𝕜 E'] (e : E ≃ₗ[𝕜] E') : (e.conj A).pointSpectralSubspace Ω = Submodule.map (↑e) (A.pointSpectralSubspace Ω)

Conjugating an endomorphism by a linear equivalence transports its point-spectral subspaces: the point-spectral subspace of e ∘ A ∘ e⁻¹ selected by Ω is the image under e of that of A.

theorem Module.End.pointSpectralSubspace_insert_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : End 𝕜 E} {Ω : Set ℝ} (hA : LinearMap.ker A = ⊥) : A.pointSpectralSubspace (insert 0 Ω) = A.pointSpectralSubspace Ω

For an injective endomorphism, also selecting the eigenvalue 0 does not change a point-spectral subspace.

Symmetric operators

theorem LinearMap.IsSymmetric.isOrtho_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} (hA : IsSymmetric A) {Ω Ω' : Set ℝ} (h : Disjoint Ω Ω') : A.pointSpectralSubspace Ω ⟂ A.pointSpectralSubspace Ω'

Point-spectral subspaces of a symmetric operator selected by disjoint sets are orthogonal.

theorem LinearMap.IsSymmetric.pointSpectralSubspace_sup_compl_eq_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) (Ω : Set ℝ) : A.pointSpectralSubspace Ω ⊔ A.pointSpectralSubspace Ωᶜ = ⊤

For a symmetric operator on a finite-dimensional space, the point-spectral subspaces selected by Ω and by its complement together span the space.

theorem LinearMap.IsSymmetric.isCompl_pointSpectralSubspace_Iio_zero_Ioi_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) (hker : ker A = ⊥) : IsCompl (A.pointSpectralSubspace (Set.Iio 0)) (A.pointSpectralSubspace (Set.Ioi 0))

For an injective symmetric operator on a finite-dimensional space, the point-spectral subspaces of the negative and of the positive eigenvalues are complementary.

theorem LinearMap.IsSymmetric.orthogonal_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) (Ω : Set ℝ) : (A.pointSpectralSubspace Ω)ᗮ = A.pointSpectralSubspace Ωᶜ

For a symmetric operator on a finite-dimensional space, the orthogonal complement of the point-spectral subspace selected by Ω is the point-spectral subspace selected by Ωᶜ.

theorem LinearMap.IsSymmetric.orthogonal_pointSpectralSubspace_Iio_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) (hA' : ker A = ⊥) : (A.pointSpectralSubspace (Set.Iio 0))ᗮ = A.pointSpectralSubspace (Set.Ioi 0)

For an injective symmetric operator on a finite-dimensional space, the orthogonal complement of the negative spectral subspace is the positive spectral subspace.

theorem LinearMap.IsSymmetric.orthogonal_pointSpectralSubspace_Ioi_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) (hA' : ker A = ⊥) : (A.pointSpectralSubspace (Set.Ioi 0))ᗮ = A.pointSpectralSubspace (Set.Iio 0)

For an injective symmetric operator on a finite-dimensional space, the orthogonal complement of the positive spectral subspace is the negative spectral subspace.

theorem LinearMap.IsSymmetric.pointSpectralSubspace_eq_eigenvectorSpan {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (Ω : Set ℝ) : A.pointSpectralSubspace Ω = hA.eigenvectorSpan hn {i : Fin n | hA.eigenvalues hn i ∈ Ω}

For a symmetric operator on a finite-dimensional space, the point-spectral subspace selected by Ω is spanned by the vectors of an ordered eigenbasis whose eigenvalues lie in Ω.

theorem LinearMap.IsSymmetric.finrank_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (Ω : Set ℝ) : Module.finrank 𝕜 ↥(A.pointSpectralSubspace Ω) = {i : Fin n | hA.eigenvalues hn i ∈ Ω}.ncard

For a symmetric operator on a finite-dimensional space, the dimension of the point-spectral subspace selected by Ω is the number of eigenvalues in Ω, counted with multiplicity.

theorem LinearMap.IsSymmetric.coe_starProjection_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) (Ω : Set ℝ) : ↑(A.pointSpectralSubspace Ω).starProjection = hA.cfc (Ω.indicator 1)

The point-spectral projector. For a symmetric operator A on a finite-dimensional space, the orthogonal projection onto the point-spectral subspace selected by Ω is the functional calculus 𝟙_Ω(A) of the indicator function of Ω.

theorem LinearMap.IsSymmetric.re_inner_apply_self_lt_zero_of_mem_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) {Ω : Set ℝ} (hΩ : Ω ⊆ Set.Iio 0) {v : E} (hv : v ∈ A.pointSpectralSubspace Ω) (hv0 : v ≠ 0) : RCLike.re (inner 𝕜 (A v) v) < 0

The quadratic form of a symmetric operator is negative definite on a point-spectral subspace selected by negative reals, in particular on its negative spectral subspace.

theorem LinearMap.IsSymmetric.re_inner_apply_self_pos_of_mem_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) {Ω : Set ℝ} (hΩ : Ω ⊆ Set.Ioi 0) {v : E} (hv : v ∈ A.pointSpectralSubspace Ω) (hv0 : v ≠ 0) : 0 < RCLike.re (inner 𝕜 (A v) v)

The quadratic form of a symmetric operator is positive definite on a point-spectral subspace selected by positive reals, in particular on its positive spectral subspace.

theorem LinearMap.IsSymmetric.eq_starProjection_pointSpectralSubspace_Iio_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) (hA' : ker A = ⊥) {p : Module.End 𝕜 E} (hp : IsIdempotentElem p) (hcomm : Commute A p) (hneg : ∀ (x : E), p x ≠ 0 → RCLike.re (inner 𝕜 (A (p x)) (p x)) < 0) (hpos : ∀ (x : E), p x = 0 → x ≠ 0 → 0 < RCLike.re (inner 𝕜 (A x) x)) : p = ↑(A.pointSpectralSubspace (Set.Iio 0)).starProjection

Characterization of the negative spectral projection of an injective symmetric operator. An idempotent p commuting with A, such that the quadratic form of A is negative definite on the range of p and positive definite on its kernel, is the orthogonal projection onto the negative spectral subspace of A.

Quadratic-form bounds

theorem Module.End.pointSpectrumIn_Iic_of_re_inner_apply_self_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {a : ℝ} (h : ∀ x ∈ U, RCLike.re (inner 𝕜 (A x) x) ≤ a * ‖x‖ ^ 2) : A.PointSpectrumIn U (Set.Iic a)

An upper quadratic-form bound re ⟪A x, x⟫ ≤ a ‖x‖² on U confines the restricted point spectrum of A on U to (-∞, a].

theorem Module.End.pointSpectrumIn_Ici_of_le_re_inner_apply_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {a : ℝ} (h : ∀ x ∈ U, a * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)) : A.PointSpectrumIn U (Set.Ici a)

A lower quadratic-form bound a ‖x‖² ≤ re ⟪A x, x⟫ on U confines the restricted point spectrum of A on U to [a, ∞).

theorem LinearMap.IsSymmetric.re_inner_apply_self_le_of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} {U : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥U] {a : ℝ} (hA : IsSymmetric A) (hU : ∀ x ∈ U, A x ∈ U) (h : A.PointSpectrumIn U (Set.Iic a)) {x : E} (hx : x ∈ U) : RCLike.re (inner 𝕜 (A x) x) ≤ a * ‖x‖ ^ 2

Upper form bound from point spectrum. If U is a finite-dimensional subspace invariant under a symmetric operator A, and the restricted point spectrum of A on U lies in (-∞, a], then re ⟪A x, x⟫ ≤ a ‖x‖² for every x ∈ U.

theorem LinearMap.IsSymmetric.le_re_inner_apply_self_of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} {U : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥U] {a : ℝ} (hA : IsSymmetric A) (hU : ∀ x ∈ U, A x ∈ U) (h : A.PointSpectrumIn U (Set.Ici a)) {x : E} (hx : x ∈ U) : a * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)

Lower form bound from point spectrum. If U is a finite-dimensional subspace invariant under a symmetric operator A, and the restricted point spectrum of A on U lies in [a, ∞), then a ‖x‖² ≤ re ⟪A x, x⟫ for every x ∈ U.

theorem LinearMap.IsSymmetric.pointSpectrumIn_Iic_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} {U : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥U] {a : ℝ} (hA : IsSymmetric A) (hU : ∀ x ∈ U, A x ∈ U) : A.PointSpectrumIn U (Set.Iic a) ↔ ∀ x ∈ U, RCLike.re (inner 𝕜 (A x) x) ≤ a * ‖x‖ ^ 2

On a finite-dimensional subspace U invariant under a symmetric operator A, the restricted point spectrum lies in (-∞, a] exactly when re ⟪A x, x⟫ ≤ a ‖x‖² on U.

theorem LinearMap.IsSymmetric.pointSpectrumIn_Ici_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} {U : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥U] {a : ℝ} (hA : IsSymmetric A) (hU : ∀ x ∈ U, A x ∈ U) : A.PointSpectrumIn U (Set.Ici a) ↔ ∀ x ∈ U, a * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)

On a finite-dimensional subspace U invariant under a symmetric operator A, the restricted point spectrum lies in [a, ∞) exactly when a ‖x‖² ≤ re ⟪A x, x⟫ on U.

theorem LinearMap.IsSymmetric.re_inner_apply_self_nonneg_of_mem_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : Module.End 𝕜 E} [FiniteDimensional 𝕜 E] (hA : IsSymmetric A) {Ω : Set ℝ} (hΩ : Ω ⊆ Set.Ici 0) {v : E} (hv : v ∈ A.pointSpectralSubspace Ω) : 0 ≤ RCLike.re (inner 𝕜 (A v) v)

The quadratic form of a symmetric operator is positive semidefinite on a point-spectral subspace selected by nonnegative reals, in particular on its nonnegative spectral subspace.

Norm bounds

theorem LinearMap.IsSymmetric.norm_apply_sub_smul_le_of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : Module.End 𝕜 E} {U : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥U] {c r : ℝ} (hT : IsSymmetric T) (hU : ∀ x ∈ U, T x ∈ U) (h : T.PointSpectrumIn U (Metric.closedBall c r)) {x : E} (hxU : x ∈ U) : ‖T x - ↑c • x‖ ≤ r * ‖x‖

Norm bound from point spectrum. If U is a finite-dimensional subspace invariant under a symmetric operator T, and every eigenvalue of T on U lies within r of c, then ‖T x - c x‖ ≤ r ‖x‖ for every x ∈ U.

theorem LinearMap.IsSymmetric.mul_norm_le_norm_apply_sub_smul_of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : Module.End 𝕜 E} {U : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥U] {c r : ℝ} (hT : IsSymmetric T) (hU : ∀ x ∈ U, T x ∈ U) (h : T.PointSpectrumIn U (Metric.ball c r)ᶜ) {x : E} (hxU : x ∈ U) : r * ‖x‖ ≤ ‖T x - ↑c • x‖

Lower norm bound from point spectrum. If U is a finite-dimensional subspace invariant under a symmetric operator T, and every eigenvalue of T on U is at distance at least r from c, then r ‖x‖ ≤ ‖T x - c x‖ for every x ∈ U.

theorem ContinuousLinearMap.abs_le_norm_of_mem_restrictedPointSpectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {T : E →L[𝕜] E} {U : Submodule 𝕜 E} {μ : ℝ} (hμ : μ ∈ Module.End.restrictedPointSpectrum (↑T) U) : |μ| ≤ ‖T‖

Every real eigenvalue of a bounded operator T, carried by any subspace, has absolute value at most ‖T‖.

Spectral separation

def Module.End.PointSpectraSeparated {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (A : End 𝕜 E) (U : Submodule 𝕜 E) (B : End 𝕜 F) (V : Submodule 𝕜 F) (δ : ℝ) : Prop

A.PointSpectraSeparated U B V δ says that the restricted point spectra of A on U and of B on V are at distance at least δ: δ ≤ |μ - ν| for every eigenvalue μ of A carried by U and every eigenvalue ν of B carried by V. No ordering of the two spectra is implied.

theorem Module.End.pointSpectraSeparated_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} : A.PointSpectraSeparated U B V δ ↔ ∀ μ ∈ A.restrictedPointSpectrum U, ∀ ν ∈ B.restrictedPointSpectrum V, δ ≤ |μ - ν|

Restatement of Module.End.PointSpectraSeparated in terms of the restricted point spectra.

theorem Module.End.PointSpectraSeparated.le_abs_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} (h : A.PointSpectraSeparated U B V δ) {μ ν : ℝ} (hμ : μ ∈ A.restrictedPointSpectrum U) (hν : ν ∈ B.restrictedPointSpectrum V) : δ ≤ |μ - ν|

Eigenvalues carried by separated subspaces are at distance at least δ.

theorem Module.End.PointSpectraSeparated.symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} (h : A.PointSpectraSeparated U B V δ) : B.PointSpectraSeparated V A U δ

Separation is symmetric in the two operators.

theorem Module.End.pointSpectraSeparated_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} : A.PointSpectraSeparated U B V δ ↔ B.PointSpectraSeparated V A U δ

Separation is symmetric in the two operators.

theorem Module.End.PointSpectraSeparated.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U U' : Submodule 𝕜 E} {V V' : Submodule 𝕜 F} {δ δ' : ℝ} (h : A.PointSpectraSeparated U B V δ) (hU : U' ≤ U) (hV : V' ≤ V) (hδ : δ' ≤ δ) : A.PointSpectraSeparated U' B V' δ'

Separation passes to smaller subspaces and smaller distances.

theorem Module.End.PointSpectraSeparated.of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} {Ω Ω' : Set ℝ} (hA : A.PointSpectrumIn U Ω) (hB : B.PointSpectrumIn V Ω') (hΩ : ∀ μ ∈ Ω, ∀ ν ∈ Ω', δ ≤ |μ - ν|) : A.PointSpectraSeparated U B V δ

Restricted point spectra lying in sets Ω and Ω' at distance at least δ from each other are separated by δ.

theorem Module.End.PointSpectraSeparated.disjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} (h : A.PointSpectraSeparated U B V δ) (hδ : 0 < δ) : Disjoint (A.restrictedPointSpectrum U) (B.restrictedPointSpectrum V)

Restricted point spectra separated by a positive distance are disjoint.

theorem Module.End.pointSpectraSeparated_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {δ : ℝ} (A : End 𝕜 E) (B : End 𝕜 F) {Ω Ω' : Set ℝ} (hΩ : ∀ μ ∈ Ω, ∀ ν ∈ Ω', δ ≤ |μ - ν|) : A.PointSpectraSeparated (A.pointSpectralSubspace Ω) B (B.pointSpectralSubspace Ω') δ

Point-spectral subspaces selected by sets Ω and Ω' at distance at least δ from each other carry point spectra separated by δ.

def Module.End.PointOrderedGap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (A : End 𝕜 E) (U : Submodule 𝕜 E) (B : End 𝕜 F) (V : Submodule 𝕜 F) (δ : ℝ) : Prop

A.PointOrderedGap U B V δ says that the restricted point spectrum of A on U lies below that of B on V with margin δ: μ + δ ≤ ν for every eigenvalue μ of A carried by U and every eigenvalue ν of B carried by V.

theorem Module.End.pointOrderedGap_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} : A.PointOrderedGap U B V δ ↔ ∀ μ ∈ A.restrictedPointSpectrum U, ∀ ν ∈ B.restrictedPointSpectrum V, μ + δ ≤ ν

Restatement of Module.End.PointOrderedGap in terms of the restricted point spectra.

theorem Module.End.PointOrderedGap.add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} (h : A.PointOrderedGap U B V δ) {μ ν : ℝ} (hμ : μ ∈ A.restrictedPointSpectrum U) (hν : ν ∈ B.restrictedPointSpectrum V) : μ + δ ≤ ν

An eigenvalue of A carried by U lies at least δ below every eigenvalue of B carried by V.

theorem Module.End.PointOrderedGap.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U U' : Submodule 𝕜 E} {V V' : Submodule 𝕜 F} {δ δ' : ℝ} (h : A.PointOrderedGap U B V δ) (hU : U' ≤ U) (hV : V' ≤ V) (hδ : δ' ≤ δ) : A.PointOrderedGap U' B V' δ'

An ordered gap passes to smaller subspaces and smaller margins.

theorem Module.End.PointOrderedGap.pointSpectraSeparated {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {δ : ℝ} (h : A.PointOrderedGap U B V δ) : A.PointSpectraSeparated U B V δ

An ordered gap is a separation. If the restricted point spectrum of A on U lies below that of B on V with margin δ, the two are separated by δ.

theorem Module.End.PointOrderedGap.of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {a δ : ℝ} (hA : A.PointSpectrumIn U (Set.Iic a)) (hB : B.PointSpectrumIn V (Set.Ici (a + δ))) : A.PointOrderedGap U B V δ

Opposite-side containment gives an ordered gap. If the restricted point spectrum of A on U lies in (-∞, a] and that of B on V lies in [a + δ, ∞), then they are ordered with margin δ.

theorem Module.End.pointOrderedGap_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] (A : End 𝕜 E) (a δ : ℝ) : A.PointOrderedGap (A.pointSpectralSubspace (Set.Iic a)) A (A.pointSpectralSubspace (Set.Ici (a + δ))) δ

The point-spectral subspaces of A selected by (-∞, a] and by [a + δ, ∞) carry point spectra ordered with margin δ.

structure Module.End.PointIntervalExteriorGap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (A : End 𝕜 E) (U : Submodule 𝕜 E) (B : End 𝕜 F) (V : Submodule 𝕜 F) (a b δ : ℝ) : Prop

A.PointIntervalExteriorGap U B V a b δ says that the restricted point spectrum of A on U lies in the interval [a, b], while that of B on V lies outside its enlargement (a - δ, b + δ).

• pointSpectrumIn_Icc : A.PointSpectrumIn U (Set.Icc a b)

  The restricted point spectrum of A on U lies in [a, b].

• pointSpectrumIn_compl_Ioo : B.PointSpectrumIn V (Set.Ioo (a - δ) (b + δ))ᶜ

  The restricted point spectrum of B on V avoids (a - δ, b + δ).

theorem Module.End.PointIntervalExteriorGap.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U U' : Submodule 𝕜 E} {V V' : Submodule 𝕜 F} {a b δ δ' : ℝ} (h : A.PointIntervalExteriorGap U B V a b δ) (hU : U' ≤ U) (hV : V' ≤ V) (hδ : δ' ≤ δ) : A.PointIntervalExteriorGap U' B V' a b δ'

An interval/exterior gap passes to smaller subspaces and smaller margins.

theorem Module.End.PointIntervalExteriorGap.pointSpectraSeparated {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {a b δ : ℝ} (h : A.PointIntervalExteriorGap U B V a b δ) : A.PointSpectraSeparated U B V δ

An interval/exterior gap is a separation. If the restricted point spectrum of A on U lies in [a, b] and that of B on V lies outside (a - δ, b + δ), the two are separated by δ.

theorem Module.End.pointIntervalExteriorGap_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] (A : End 𝕜 E) (a b δ : ℝ) : A.PointIntervalExteriorGap (A.pointSpectralSubspace (Set.Icc a b)) A (A.pointSpectralSubspace (Set.Ioo (a - δ) (b + δ))ᶜ) a b δ

The point-spectral subspaces of A selected by [a, b] and by the complement of (a - δ, b + δ) satisfy the interval/exterior gap.

theorem Module.End.finite_restrictedPointSpectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [FiniteDimensional 𝕜 E] (A : End 𝕜 E) (U : Submodule 𝕜 E) : (A.restrictedPointSpectrum U).Finite

In finite dimension, the restricted point spectrum is finite.

theorem Module.End.exists_pos_pointSpectraSeparated_iff_disjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : (∃ δ > 0, A.PointSpectraSeparated U B V δ) ↔ Disjoint (A.restrictedPointSpectrum U) (B.restrictedPointSpectrum V)

In finite dimension, two restricted point spectra are separated by some positive distance exactly when they are disjoint.

structure Module.End.PointInternalGap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : End 𝕜 E) (U : Submodule 𝕜 E) (δ : ℝ) : Prop

An invariant subspace whose restricted point spectrum is separated by at least δ from the restricted point spectrum of its orthogonal complement.

• invariant (x : E) : x ∈ U → A x ∈ U

  The selected subspace is preserved by the operator.

• pointSpectraSeparated : A.PointSpectraSeparated U A Uᗮ δ

  The restricted point spectra on the subspace and its complement are separated.

theorem Module.End.PointInternalGap.mono_gap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {δ δ' : ℝ} (h : A.PointInternalGap U δ) (hδ : δ' ≤ δ) : A.PointInternalGap U δ'

Weakening the separation bound preserves an internal point-spectrum gap.

theorem Module.End.PointInternalGap.of_pointOrderedGap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {δ : ℝ} (hU : ∀ x ∈ U, A x ∈ U) (h : A.PointOrderedGap U A Uᗮ δ) : A.PointInternalGap U δ

An invariant subspace with an ordered gap from its complement has an internal gap.

theorem Module.End.PointInternalGap.of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : End 𝕜 E} {U : Submodule 𝕜 E} {δ : ℝ} {s t : Set ℝ} (hU : ∀ x ∈ U, A x ∈ U) (hs : A.PointSpectrumIn U s) (ht : A.PointSpectrumIn Uᗮ t) (hsep : ∀ a ∈ s, ∀ b ∈ t, δ ≤ |a - b|) : A.PointInternalGap U δ

Spectral containment in separated sets gives an internal point-spectrum gap.

theorem Module.End.pointSpectrumIn_orthogonal_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : End 𝕜 E) (Ω : Set ℝ) : A.PointSpectrumIn (A.pointSpectralSubspace Ω)ᗮ Ωᶜ

The orthogonal complement of the point-spectral subspace selected by Ω carries no eigenvalues belonging to Ω. No symmetry or finite-dimensionality assumption is needed.

theorem Module.End.pointInternalGap_pointSpectralSubspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {δ : ℝ} (A : End 𝕜 E) (Ω : Set ℝ) (hΩ : ∀ μ ∈ Ω ∩ A.restrictedPointSpectrum ⊤, ∀ ν ∈ Ωᶜ ∩ A.restrictedPointSpectrum ⊤, δ ≤ |μ - ν|) : A.PointInternalGap (A.pointSpectralSubspace Ω) δ

A spectral subspace of any endomorphism has an internal point-spectrum gap if the actual eigenvalues selected by Ω are separated from those in Ωᶜ by at least δ. The separation hypothesis only quantifies over eigenvalues of A, not all real numbers.

theorem Module.End.PointOrderedGap.of_re_inner_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : End 𝕜 E} {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {a δ : ℝ} (hA : ∀ x ∈ U, RCLike.re (inner 𝕜 (A x) x) ≤ a * ‖x‖ ^ 2) (hB : ∀ y ∈ V, (a + δ) * ‖y‖ ^ 2 ≤ RCLike.re (inner 𝕜 (B y) y)) : A.PointOrderedGap U B V δ

Form bounds give an ordered gap. If re ⟪A x, x⟫ ≤ a ‖x‖² on U and (a + δ) ‖y‖² ≤ re ⟪B y, y⟫ on V, then the restricted point spectra of A on U and of B on V are ordered with margin δ.

theorem Module.End.PointIntervalExteriorGap.of_re_inner_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {B : End 𝕜 F} {U : Submodule 𝕜 E} {V : Submodule 𝕜 F} {a : ℝ} {T : E →L[𝕜] E} {b : ℝ} (hT : ∀ x ∈ U, RCLike.re (inner 𝕜 (T x) x) ≤ a * ‖x‖ ^ 2) (hB : ∀ y ∈ V, b * ‖y‖ ^ 2 ≤ RCLike.re (inner 𝕜 (B y) y)) : PointIntervalExteriorGap (↑T) U B V (-‖T‖) a (b - a)

Form bounds give an interval/exterior gap. If re ⟪T x, x⟫ ≤ a ‖x‖² on U and b ‖y‖² ≤ re ⟪B y, y⟫ on V, then the restricted point spectrum of T on U lies in [-‖T‖, a] and that of B on V avoids (-‖T‖ - (b - a), b).

theorem LinearMap.IsSymmetric.eigenvalues_ne_eigenvalues_of_disjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] E} {B : F →ₗ[𝕜] F} {n m : ℕ} (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (hm : Module.finrank 𝕜 F = m) (h : Disjoint (Module.End.restrictedPointSpectrum A ⊤) (Module.End.restrictedPointSpectrum B ⊤)) (i : Fin n) (j : Fin m) : hA.eigenvalues hn i ≠ hB.eigenvalues hm j

If the real point spectra of symmetric A and B are disjoint, then no eigenvalue of an ordered eigenbasis of A equals one of an ordered eigenbasis of B.

theorem LinearMap.IsSymmetric.re_inner_ritz_le_of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] E} (hA : A.IsSymmetric) (X : F →ₗ[𝕜] E) {α : ℝ} (h : Module.End.PointSpectrumIn (adjoint X ∘ₗ A ∘ₗ X) ⊤ (Set.Iic α)) (y : F) : RCLike.re (inner 𝕜 ((adjoint X ∘ₗ A ∘ₗ X) y) y) ≤ α * ‖y‖ ^ 2

The trial-space spectral bound on the Ritz compression X† A X, in quadratic-form shape.

theorem LinearMap.IsSymmetric.le_re_inner_of_pointSpectrumIn_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hA : A.IsSymmetric) {U : Submodule 𝕜 E} (hU : U ∈ Module.End.invtSubmodule A) {β : ℝ} (h : Module.End.PointSpectrumIn A Uᗮ (Set.Ici β)) {y : E} (hy : y ∈ Uᗮ) : β * ‖y‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A y) y)

The separated spectral bound on the orthogonal complement of an invariant subspace, in quadratic-form shape.