Symmetry and spectral bounds for reduced extensions

ContinuousLinearMap.reducedExtension is defined in Projection.Block, together with its block actions, quadratic-form splitting and global bounds from local quadratic-form bounds. This module proves symmetry of the extension for invariant symmetric blocks, without a completeness assumption, and obtains the global form bounds from finite-dimensional restricted point-spectrum containment. For an invariant block, every real eigenvalue of the extension is either the scalar κ or an eigenvalue of the original operator carried by the block, so the extension can move the spectrum off the block wherever it is convenient.

Provenance

The spectral consequences are adapted from the maintained AIQ-Kitware DKPS formalization (Kitware, Inc.; Apache-2.0), ForTauCeti/Analysis/InnerProductSpace/ReducedExtension.lean. The common block splitting and bounds reuse Projection.Block rather than duplicating them.

theorem ContinuousLinearMap.isSymmetric_reducedExtension {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) {W : Submodule 𝕜 E} [W.HasOrthogonalProjection] (hT : (↑T).IsSymmetric) (hW : ∀ x ∈ W, T x ∈ W) (κ : ℝ) : (↑(T.reducedExtension W κ)).IsSymmetric

The reduced extension of a symmetric operator along an invariant subspace is symmetric, without any completeness hypothesis on the ambient inner product space.

theorem ContinuousLinearMap.re_inner_reducedExtension_self_le_of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) {W : Submodule 𝕜 E} [W.HasOrthogonalProjection] [FiniteDimensional 𝕜 ↥W] (hT : (↑T).IsSymmetric) (hW : ∀ x ∈ W, T x ∈ W) {c κ : ℝ} (hκ : κ ≤ c) (hspec : Module.End.PointSpectrumIn (↑T) W (Set.Iic c)) (x : E) : RCLike.re (inner 𝕜 ((T.reducedExtension W κ) x) x) ≤ c * ‖x‖ ^ 2

Restricted point-spectrum containment in (-∞, c] gives an upper bound for a reduced extension with scalar κ ≤ c.

theorem ContinuousLinearMap.le_re_inner_reducedExtension_self_of_pointSpectrumIn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) {W : Submodule 𝕜 E} [W.HasOrthogonalProjection] [FiniteDimensional 𝕜 ↥W] (hT : (↑T).IsSymmetric) (hW : ∀ x ∈ W, T x ∈ W) {c κ : ℝ} (hκ : c ≤ κ) (hspec : Module.End.PointSpectrumIn (↑T) W (Set.Ici c)) (x : E) : c * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 ((T.reducedExtension W κ) x) x)

Restricted point-spectrum containment in [c, ∞) gives a lower bound for a reduced extension with scalar κ ≥ c.

theorem ContinuousLinearMap.restrictedPointSpectrum_reducedExtension_subset {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) {W : Submodule 𝕜 E} [W.HasOrthogonalProjection] (hW : ∀ x ∈ W, A x ∈ W) (κ : ℝ) : Module.End.restrictedPointSpectrum ↑(A.reducedExtension W κ) ⊤ ⊆ insert κ (Module.End.restrictedPointSpectrum (↑A) W)

Along an invariant subspace W, every real eigenvalue of the reduced extension A P_W + κ P_{Wᗮ} is either κ or an eigenvalue of A with an eigenvector in W.