Reducing subspaces for bounded operators

General RCLike infrastructure for invariant and reducing subspaces of bounded operators on inner-product spaces. This module is independent of the Davis--Kahan theory.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: authored directly in ForMathlib at Davis--Kahan commit df036cd; it has had no prior home.
• Extraction class: authored in place, for Tau Ceti — ForMathlib was retired on 2026-07-29 and ForTauCeti is the single staging library, whose destination is Tau Ceti and not Mathlib (ForTauCeti/README.md).
• Original authors / copyright: Jon Crall, GPT 5.6 High; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — the ForTauCeti import firewall admits only Mathlib, TauCeti and ForTauCeti (enforced by scripts/check_dependency_layers.py).

def ContinuousLinearMap.Reduces {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) : Prop

A subspace reduces a bounded operator when it and its orthogonal complement are invariant.

Equations

• A.Reduces U = ((∀ x ∈ U, A x ∈ U) ∧ ∀ x ∈ Uᗮ, A x ∈ Uᗮ)

theorem ContinuousLinearMap.IsSymmetric.reduces_of_invariant {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →L[𝕜] E} (hA : (↑A).IsSymmetric) {U : Submodule 𝕜 E} (hU : ∀ x ∈ U, A x ∈ U) : A.Reduces U

An invariant subspace of a symmetric operator is reducing.

theorem ContinuousLinearMap.starProjection_comp_comm_of_reduces {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hU : A.Reduces U) : U.starProjection ∘SL A = A ∘SL U.starProjection

The orthogonal projection onto a reducing subspace commutes with the operator.

theorem ContinuousLinearMap.starProjection_apply_comm_of_reduces {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hU : A.Reduces U) (x : E) : U.starProjection (A x) = A (U.starProjection x)

Pointwise form of starProjection_comp_comm_of_reduces.

theorem LinearMap.norm_starProjection_apply_le_of_mem_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {Z : Submodule 𝕜 E} [Z.HasOrthogonalProjection] {rho : ℝ} (hrho0 : 0 ≤ rho) (hrho : ∀ x ∈ Z, ‖T x - Z.starProjection (T x)‖ ≤ rho * ‖x‖) {w : E} (hw : w ∈ Zᗮ) : ‖Z.starProjection (T w)‖ ≤ rho * ‖w‖

A symmetric map that nearly reduces Z moves Zᗮ only slightly into Z.

If ‖T x - Z.starProjection (T x)‖ ≤ ρ ‖x‖ for every x ∈ Z -- the quantitative form of "T reduces Z" -- then for w ⊥ Z the part of T w lying in Z is at most ρ ‖w‖. Symmetry is what lets the estimate be read on either side of the inner product.

At ρ = 0 this is the qualitative statement: a symmetric map reducing Z maps Zᗮ into Zᗮ, which is ContinuousLinearMap.IsSymmetric.reduces_of_invariant above in bounded form.

theorem Submodule.isComplete_coe_of_hasOrthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : IsComplete ↑U

A subspace admitting an orthogonal projection is complete when the ambient space is complete.

theorem TauCeti.CompleteSubspace.instCompleteSpaceCoeOfHasOrthogonalProjection {𝕜 : Type u_3} [RCLike 𝕜] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] (U : Submodule 𝕜 G) [U.HasOrthogonalProjection] : CompleteSpace ↥U

A subspace admitting an orthogonal projection inside a complete ambient space is itself complete, as an instance.

scoped rather than global, because the search CompleteSpace ↥U is one that fires on every subspace coercion and the cost of that is not worth paying in modules that do not need it. Activate it with

open scoped TauCeti.CompleteSubspace

Use this one. It exists because the same three-line local instance was written out forty-three times across DavisKahan and ForTauCeti, each under a different name. That is not only duplication: the instance name is part of the elaborated type of every theorem whose statement compresses to a subspace, so two modules holding private copies state provably identical theorems that the comparator, and any exact signature comparison, reports as different. A new copy would put that back.