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_le and range_cfcₙHom_le: for RCLike scalar rings, the range of the continuous functional calculus homomorphism is contained in the elemental subalgebra generated by the given element. When the continuous functional calculus homomorphism is a closed embedding, this containment is in fact an equality, as found in range_cfcHom and range_cfcₙHom
• range_cfc_nnreal_subset and range_cfcₙ_nnreal_subset: 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. Again, when the continuous functional calculus homomorphism is a closed embedding, this containment is an equality, see range_cfc_nnreal_subset and range_cfcₙ_nnreal_subset.
• cfc_mem and cfcₙ_mem: the continuous functional calculus of an element is contained in any closed star subalgebra containing the 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] [ClosedEmbeddingContinuousFunctionalCalculus 𝕜 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] [ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p] [IsTopologicalRing A] [ContinuousStar A] {a : A} (ha : p a) : (Set.range fun (x : 𝕜 → 𝕜) => cfc x a) = ↑(StarAlgebra.elemental 𝕜 a)

theorem range_cfcHom_le (𝕜 : 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_subset (𝕜 : 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_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_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 cfc_mem {𝕜 : 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] {𝕜' : Type u_3} {S : Type u_4} [Monoid 𝕜'] [MulAction 𝕜' A] [SetLike S A] [SubringClass S A] [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' A] [SMulMemClass S 𝕜' A] [StarMemClass S A] {s : S} [hs : IsClosed ↑s] (f : 𝕜 → 𝕜) {a : A} (has : a ∈ s) : cfc f a ∈ s

theorem range_cfc_nnreal_eq_image_cfc_real {A : Type u_1} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : 0 ≤ a := by cfc_tac) : (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_subset {A : Type u_1} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] [ContinuousStar A] [StarModule ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : 0 ≤ a := by cfc_tac) : (Set.range fun (x : NNReal → NNReal) => cfc x a) ⊆ {x : A | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}

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

theorem cfc_nnreal_mem {A : Type u_1} [Ring A] [StarRing A] [Algebra ℝ A] [TopologicalSpace A] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] [ContinuousStar A] [StarModule ℝ A] {𝕜 : Type u_2} [RCLike 𝕜] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {S : Type u_3} [MulAction 𝕜 A] [SetLike S A] [SubringClass S A] [IsScalarTower ℝ 𝕜 A] [SMulMemClass S 𝕜 A] [StarMemClass S A] {s : S} [hs : IsClosed ↑s] (f : NNReal → NNReal) {a : A} (has : a ∈ s) : cfc f a ∈ s

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] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] [NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p] {a : A} (ha : p a) : (cfcₙHom ha).range = 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] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] [NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p] {a : A} (ha : p a) : (Set.range fun (x : 𝕜 → 𝕜) => cfcₙ x a) = ↑(NonUnitalStarAlgebra.elemental 𝕜 a)

theorem range_cfcₙHom_le (𝕜 : 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] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] {a : A} (ha : p a) : (cfcₙHom ha).range ≤ NonUnitalStarAlgebra.elemental 𝕜 a

theorem range_cfcₙ_subset (𝕜 : 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] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] {a : A} (ha : p a) : (Set.range fun (x : 𝕜 → 𝕜) => cfcₙ x a) ⊆ ↑(NonUnitalStarAlgebra.elemental 𝕜 a)

theorem cfcₙHom_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] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] {a : A} (ha : p a) (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) : (cfcₙHom ha) f ∈ NonUnitalStarAlgebra.elemental 𝕜 a

@[simp]

theorem cfcₙ_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] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) : cfcₙ f a ∈ NonUnitalStarAlgebra.elemental 𝕜 a

theorem cfcₙ_mem {𝕜 : 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] [ContinuousConstSMul 𝕜 A] [StarModule 𝕜 A] [IsTopologicalRing A] [ContinuousStar A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] {𝕜' : Type u_3} {S : Type u_4} [Monoid 𝕜'] [MulAction 𝕜' A] [SetLike S A] [NonUnitalSubringClass S A] [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' A] [SMulMemClass S 𝕜' A] [StarMemClass S A] {s : S} [hs : IsClosed ↑s] (f : 𝕜 → 𝕜) {a : A} (has : a ∈ s) : cfcₙ f a ∈ s

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] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : 0 ≤ a := by cfc_tac) : (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_subset {A : Type u_1} [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [TopologicalSpace A] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] [StarModule ℝ A] [ContinuousStar A] [ContinuousConstSMul ℝ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : 0 ≤ a := by cfc_tac) : (Set.range fun (x : NNReal → NNReal) => cfcₙ x a) ⊆ {x : A | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}

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

theorem cfcₙ_nnreal_mem {A : Type u_1} [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [TopologicalSpace A] [IsTopologicalRing A] [T2Space A] [PartialOrder A] [NonnegSpectrumClass ℝ A] [StarOrderedRing A] [StarModule ℝ A] [ContinuousStar A] [ContinuousConstSMul ℝ A] {𝕜 : Type u_2} [RCLike 𝕜] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {S : Type u_3} [MulAction 𝕜 A] [SetLike S A] [NonUnitalSubringClass S A] [IsScalarTower ℝ 𝕜 A] [SMulMemClass S 𝕜 A] [StarMemClass S A] {s : S} [hs : IsClosed ↑s] (f : NNReal → NNReal) {a : A} (has : a ∈ s) : cfcₙ f a ∈ s

instance Subtype.starOrderedRing {𝕜 : Type u_1} {S : Type u_2} {A : Type u_3} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [ContinuousStar A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [IsTopologicalRing A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [RCLike 𝕜] [Module 𝕜 A] [IsScalarTower ℝ 𝕜 A] [ContinuousConstSMul ℝ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [StarModule ℝ A] [SetLike S A] [NonUnitalSubringClass S A] [SMulMemClass S 𝕜 A] [StarMemClass S A] (s : S) [hs : IsClosed ↑s] : StarOrderedRing ↥s