Spectral projection over ℝ via complexification

Why this file is needed: it supplies the real spectral projection (exists_spectral_projection_real); the uniform RCLike projection in Representation reduces every field to this real case via realification.

The spectral-projection construction (exists_spectral_projection_complex) lives over ℂ, because the continuous functional calculus on H →L[𝕜] H is only available for 𝕜 = ℂ. This file transfers it to a real Hilbert space H₁ by complexifying.

Given S : H₁ →L[ℝ] H₂, complexify to Sℂ : Cℂ H₁ →L[ℂ] Cℂ H₂. The complex projection Eℂ commutes with conjugation — this is the formal content of "a self-adjoint operator has real spectrum": the strengthened exists_spectral_projection_complex returns commutation of Eℂ with every ℝ-linear map commuting with Sℂ*Sℂ, and conjugation is such a map (since Sℂ*Sℂ is a complexification). Hence Eℂ maps the real subspace range ofReal into itself, and restricts to a real operator E inheriting the two operator-norm bounds.

theorem SpectralRepresentation.exists_spectral_projection_real {H₁ : Type u_1} {H₂ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] [CompleteSpace H₂] [Nontrivial 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 ∧ ∀ (K : H₁ →L[ℝ] H₁), (∀ (x : H₁), K ((ContinuousLinearMap.adjoint S ∘SL S) x) = (ContinuousLinearMap.adjoint S ∘SL S) (K x)) → ∀ (x : H₁), K (E x) = E (K x)

Spectral projection of S*S (over ℝ). The real analogue of exists_spectral_projection_complex, obtained by complexifying and restricting the conjugation- invariant complex projection.