The spectral projection of S*S over ℂ

Why this file is needed: it supplies the complex spectral projection, exists_spectral_projection_complex. The real case (RealProjection) and the uniform RCLike projection (Representation) both reduce to it.

The complex-Hilbert-space operator algebra H →L[ℂ] H is a C⋆-algebra, so Mathlib's continuous functional calculus applies to P = S*S. The projection E = E_{[c²,∞)}(P) is built as the strong-operator limit of cfc gₙ P, where gₙ is a continuous approximation decreasing to the indicator 𝟙_{[c²,∞)}. This file also proves cfc_comm_of_comm: anything commuting with P commutes with E — the ingredient that makes the projection conjugation/scalar invariant (used by RealProjection and Representation).

The approximating family stepDown

stepDown t n is the continuous function equal to 1 on [t, ∞), ramping linearly down to 0 on [t - 1/(n+1), t], and 0 below. As n → ∞ it decreases pointwise to 𝟙_{[t,∞)}. This part of the file develops its elementary properties (continuity, 0 ≤ · ≤ 1, antitone in n, value 1 above the threshold).

noncomputable def SpectralRepresentation.stepDown (t : ℝ) (n : ℕ) (s : ℝ) : ℝ

Continuous approximation, from above, of the indicator 𝟙_{[t,∞)}: stepDown t n is 1 for s ≥ t, ramps down to 0 over [t - 1/(n+1), t], and is 0 below t - 1/(n+1).

Equations

• SpectralRepresentation.stepDown t n s = max 0 (min 1 (1 + (↑n + 1) * (s - t)))

theorem SpectralRepresentation.stepDown_continuous (t : ℝ) (n : ℕ) : Continuous (stepDown t n)

theorem SpectralRepresentation.stepDown_nonneg (t : ℝ) (n : ℕ) (s : ℝ) : 0 ≤ stepDown t n s

theorem SpectralRepresentation.stepDown_le_one (t : ℝ) (n : ℕ) (s : ℝ) : stepDown t n s ≤ 1

theorem SpectralRepresentation.stepDown_eq_one (t : ℝ) (n : ℕ) {s : ℝ} (hs : t ≤ s) : stepDown t n s = 1

Above the threshold the approximation is exactly 1.

theorem SpectralRepresentation.stepDown_antitone (t s : ℝ) : Antitone fun (n : ℕ) => stepDown t n s

The family is antitone in n: a larger n gives a steeper ramp, hence a smaller value below the threshold (and 1 above).

theorem SpectralRepresentation.stepDown_ramp_bound (t : ℝ) (n : ℕ) (s : ℝ) : |(s - t) * stepDown t n s - max (s - t) 0| ≤ (↑n + 1)⁻¹

Uniform ramp estimate. (s - t) · stepDown t n is within 1/(n+1) of (s - t)⁺ = max (s - t) 0, uniformly in s. This drives the norm convergence cfc ((s-t)·stepDownₙ) P → cfc (s-t)⁺ P (no Dini theorem needed: the bound is explicit).

theorem SpectralRepresentation.cfcHom_comm_of_comm {H₁ : Type u_1} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {P : H₁ →L[ℂ] H₁} (hP : IsSelfAdjoint P) (J : H₁ →L[ℝ] H₁) (hJP : ∀ (x : H₁), J (P x) = P (J x)) (f : C(↑(spectrum ℝ P), ℝ)) (x : H₁) : J (((cfcHom hP) f) x) = ((cfcHom hP) f) (J x)

Commutation engine. A continuous ℝ-linear map J of H₁ that commutes with a self-adjoint P commutes with cfcHom hP f for every continuous symbol f. Proved by the Stone–Weierstrass induction on f (constants, id, sums, products, and a closure step), exactly as Mathlib's Commute.cfcHom — but here J is an external map (it may even be conjugate-linear over ℂ, only ℝ-linearity is used), which is why we cannot use the algebra-internal version.

theorem SpectralRepresentation.cfc_comm_of_comm {H₁ : Type u_1} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {P : H₁ →L[ℂ] H₁} (hP : IsSelfAdjoint P) (J : H₁ →L[ℝ] H₁) (hJP : ∀ (x : H₁), J (P x) = P (J x)) {g : ℝ → ℝ} (hg : Continuous g) (x : H₁) : J ((cfc g P) x) = (cfc g P) (J x)

A continuous ℝ-linear map J commuting with a self-adjoint P commutes with cfc g P for every continuous g.

theorem SpectralRepresentation.exists_spectral_projection_complex {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 ∧ ∀ (J : H₁ →L[ℝ] H₁), (∀ (x : H₁), J ((ContinuousLinearMap.adjoint S ∘SL S) x) = (ContinuousLinearMap.adjoint S ∘SL S) (J x)) → ∀ (x : H₁), J (E x) = E (J x)

Spectral projection of S*S (over ℂ).