Star projections from the continuous functional calculus

If a real function f takes only the values 0 and 1 on the spectrum of a, then cfc f a is a star projection. When f is continuous on the spectrum and a is self-adjoint this follows from multiplicativity of the functional calculus; otherwise cfc f a is the junk value 0. In particular the spectral projector cfc (Ω.indicator 1) a is a star projection for every set Ω ⊆ ℝ and every a.

When a is self-adjoint and invertible, 0 is not in its spectrum, so the spectral projectors P₊ = cfc ((Ioi 0).indicator 1) a and P₋ = cfc ((Iio 0).indicator 1) a onto the positive and negative parts of the spectrum are complementary, P₊ + P₋ = 1.

Main results

• TauCeti.isStarProjection_cfc — cfc f a is a star projection when f is idempotent-valued on the spectrum of a;
• TauCeti.isStarProjection_cfc_indicator — the spectral projector cfc (Ω.indicator 1) a is a star projection;
• IsUnit.continuousOn_indicator_spectrum — at an invertible element, the indicator of a set whose frontier is contained in {0} is continuous on the spectrum;
• TauCeti.cfc_indicator_Ioi_add_cfc_indicator_Iio — for invertible self-adjoint a, the positive and negative spectral projectors add up to 1.

theorem TauCeti.isStarProjection_cfc {A : Type u_1} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {f : ℝ → ℝ} {a : A} (hf : ∀ t ∈ spectrum ℝ a, IsIdempotentElem (f t)) : IsStarProjection (cfc f a)

If f t is idempotent (that is, 0 or 1) at every point t of the spectrum of a, then cfc f a is a star projection.

theorem TauCeti.isStarProjection_cfc_indicator {A : Type u_1} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (Ω : Set ℝ) : IsStarProjection (cfc (Ω.indicator 1) a)

The spectral projector cfc (Ω.indicator 1) a is a star projection for every Ω ⊆ ℝ. (When a is not self-adjoint, or the indicator is not continuous on its spectrum, it is the junk value 0.)

theorem IsUnit.continuousOn_indicator_spectrum {A : Type u_1} [Ring A] [Algebra ℝ A] {a : A} (ha : IsUnit a) {Ω : Set ℝ} (hΩ : frontier Ω ⊆ {0}) : ContinuousOn (Ω.indicator 1) (spectrum ℝ a)

At an invertible element, the indicator of a set whose frontier is contained in {0}, such as a half-line ending at 0, is continuous on the spectrum, since the spectrum avoids 0.

theorem TauCeti.cfc_indicator_Ioi_add_cfc_indicator_Iio {A : Type u_1} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A} (ha : IsUnit a) (ha' : IsSelfAdjoint a := by cfc_tac) : cfc ((Set.Ioi 0).indicator 1) a + cfc ((Set.Iio 0).indicator 1) a = 1

For an invertible self-adjoint a, the spectral projectors onto the positive and the negative parts of the spectrum add up to 1.