The spectral projection of S*S and the lower-bound subspace

Why this file is needed: it is the capstone of the BasicResults.Spectral subpackage — the single spectral-theory input that the s-number uniqueness theorem consumes for arbitrary bounded operators. It assembles the per-field constructions into one uniform statement and derives the geometric fact the factorisation needs.

What it provides

• SpectralRepresentation.exists_spectral_projection — for every RCLike field 𝕜 and a bounded S : H₁ →L[𝕜] H₂, the spectral projection E = E_{[c²,∞)}(S*S) with its two operator-norm bounds:

  • c · ‖E x‖ ≤ ‖S (E x)‖ (on ran E, S is bounded below by c);
  • ‖S ∘ (1 - E)‖ ≤ c (on the complement, S is bounded above by c).

  It is proved uniformly over RCLike by realification: view H₁, H₂ as real Hilbert spaces, apply the real spectral projection (exists_spectral_projection_real, itself built by complexification), and lift the result back to a 𝕜-linear operator — it is 𝕜-linear because it commutes with scalar multiplication. This avoids any case split on 𝕜 = ℝ/ℂ (which Lean cannot do) and any spectral hypothesis on downstream theorems.

• SpectralRepresentation.exists_lowerBound_subspace — (★): for 0 ≤ c < aₙ(S) there is an (n+1)-dimensional subspace M ⊆ H₁ with ‖S x‖ ≥ c ‖x‖ on M. The range of E has dimension ≥ n+1 (else S∘E is rank ≤ n with ‖S - S∘E‖ ≤ c, contradicting aₙ(S) > c), and S is bounded below by c there. This is the geometric heart of SVD.exists_scalar_factorisation.

theorem SpectralRepresentation.exists_spectral_projection {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] (S : H₁ →L[𝕜] H₂) {c : ℝ} (hc0 : 0 ≤ c) : ∃ (E : H₁ →L[𝕜] H₁), (∀ (x : H₁), c * ‖E x‖ ≤ ‖S (E x)‖) ∧ ‖S ∘SL (1 - E)‖ ≤ c

Spectral projection of S*S, uniformly over any RCLike field. Realify H₁, H₂ to real Hilbert spaces, take the real spectral projection, and lift it back to a 𝕜-linear operator: the lift is 𝕜-linear because it commutes with scalar multiplication (the commutation conjunct of exists_spectral_projection_real). The key sublemma adjoint (S.restrictScalars ℝ) = (adjoint S).restrictScalars ℝ is proved inline.

theorem SpectralRepresentation.exists_lowerBound_subspace {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] (S : H₁ →L[𝕜] H₂) (n : ℕ) {c : ℝ} (hc0 : 0 ≤ c) (hca : c < SNumbers.approximationNumber S n) : ∃ (M : Submodule 𝕜 H₁), FiniteDimensional 𝕜 ↥M ∧ Module.finrank 𝕜 ↥M = n + 1 ∧ ∀ x ∈ M, c * ‖x‖ ≤ ‖S x‖

(★) Lower-bound subspace. For 0 ≤ c < aₙ(S) there is an (n+1)-dimensional subspace M ⊆ H₁ on which S is bounded below by c. Take the spectral projection E of S*S at threshold c; its range has dimension ≥ n+1, and S is bounded below by c there.