Range of the continuous functional calculus

This file contains results about the range of the continuous functional calculus, and consequences thereof.

Main results

• range_cfcHom and range_cfcₙHom: for RCLike scalar rings, the range of the continuous functional calculus homomorphism is the elemental subalgebra generated by the given element.
• range_cfc_nnreal and range_cfcₙ_nnreal: over the scalar semiring ℝ≥0, the range of the continuous functional calculus consists of the nonnegative elements in the elemental ℝ-algebra generated by the given element.

theorem range_cfcHom (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [StarModule 𝕜 A] [ContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [ContinuousStar A] {a : A} (ha : p a) : (cfcHom ha).range = StarAlgebra.elemental 𝕜 a

theorem range_cfc (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [StarModule 𝕜 A] [ContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [ContinuousStar A] {a : A} (ha : p a) : (Set.range fun (x : 𝕜 → 𝕜) => cfc x a) = ↑(StarAlgebra.elemental 𝕜 a)

theorem cfcHom_apply_mem_elemental {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [StarModule 𝕜 A] [ContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [ContinuousStar A] {a : A} (ha : p a) (f : C(↑(spectrum 𝕜 a), 𝕜)) : (cfcHom ha) f ∈ StarAlgebra.elemental 𝕜 a

@[simp]

theorem cfc_apply_mem_elemental {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [StarModule 𝕜 A] [ContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [ContinuousStar A] (f : 𝕜 → 𝕜) (a : A) : cfc f a ∈ StarAlgebra.elemental 𝕜 a

theorem range_cfc_nnreal_eq_image_cfc_real {A : Type u_1} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] (a : A) (ha : 0 ≤ a) : (Set.range fun (x : NNReal → NNReal) => cfc x a) = (fun (x : ℝ → ℝ) => cfc x a) '' {f : ℝ → ℝ | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}

theorem range_cfc_nnreal {A : Type u_1} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] [ContinuousStar A] [StarModule ℝ A] (a : A) (ha : 0 ≤ a) : (Set.range fun (x : NNReal → NNReal) => cfc x a) = {x : A | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}

theorem range_cfcₙHom (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] {a : A} (ha : p a) : NonUnitalStarAlgHom.range (cfcₙHom ha) = NonUnitalStarAlgebra.elemental 𝕜 a

theorem range_cfcₙ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] {a : A} (ha : p a) : (Set.range fun (x : 𝕜 → 𝕜) => cfcₙ x a) = ↑(NonUnitalStarAlgebra.elemental 𝕜 a)

theorem cfcₙHom_apply_mem_elemental {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] {a : A} (ha : p a) (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) : (cfcₙHom ha) f ∈ NonUnitalStarAlgebra.elemental 𝕜 a

@[simp]

theorem cfcₙ_apply_mem_elemental {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] (f : 𝕜 → 𝕜) (a : A) : cfcₙ f a ∈ NonUnitalStarAlgebra.elemental 𝕜 a

theorem range_cfcₙ_nnreal_eq_image_cfcₙ_real {A : Type u_1} [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] (a : A) (ha : 0 ≤ a) : (Set.range fun (x : NNReal → NNReal) => cfcₙ x a) = (fun (x : ℝ → ℝ) => cfcₙ x a) '' {f : ℝ → ℝ | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x}

theorem range_cfcₙ_nnreal {A : Type u_1} [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] [StarModule ℝ A] [ContinuousStar A] [ContinuousConstSMul ℝ A] (a : A) (ha : 0 ≤ a) : (Set.range fun (x : NNReal → NNReal) => cfcₙ x a) = {x : A | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}