Interactions of the continuous functional calculus with the real and imaginary part

theorem cfcₙ_re_id {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : cfcₙ (fun (x : ℂ) => ↑x.re) a = ↑(realPart a)

theorem cfcₙ_im_id {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : cfcₙ (fun (x : ℂ) => ↑x.im) a = ↑(imaginaryPart a)

theorem quasispectrum_realPart {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : quasispectrum ℂ ↑(realPart a) = (fun (x : ℂ) => ↑x.re) '' quasispectrum ℂ a

theorem quasispectrum_realPart' {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : quasispectrum ℝ ↑(realPart a) = Complex.re '' quasispectrum ℂ a

theorem quasispectrum_imaginaryPart {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : quasispectrum ℂ ↑(imaginaryPart a) = (fun (x : ℂ) => ↑x.im) '' quasispectrum ℂ a

theorem quasispectrum_imaginaryPart' {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : quasispectrum ℝ ↑(imaginaryPart a) = Complex.im '' quasispectrum ℂ a

theorem cfcₙ_realPart {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMapZero.UniqueHom ℂ A] (f : ℂ → ℂ) (a : A) (hf : ContinuousOn f (quasispectrum ℂ ↑(realPart a)) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : IsStarNormal a := by cfc_tac) : cfcₙ f ↑(realPart a) = cfcₙ (fun (x : ℂ) => f ↑x.re) a

theorem cfcₙ_imaginaryPart {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMapZero.UniqueHom ℂ A] (f : ℂ → ℂ) (a : A) (hf : ContinuousOn f (quasispectrum ℂ ↑(imaginaryPart a)) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : IsStarNormal a := by cfc_tac) : cfcₙ f ↑(imaginaryPart a) = cfcₙ (fun (x : ℂ) => f ↑x.im) a

theorem cfcₙ_comp_re {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMapZero.UniqueHom ℂ A] [T2Space A] (f : ℝ → ℝ) (a : A) (hf : ContinuousOn f (quasispectrum ℝ ↑(realPart a)) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : IsStarNormal a := by cfc_tac) : cfcₙ (fun (x : ℂ) => ↑(f x.re)) a = cfcₙ f ↑(realPart a)

theorem cfcₙ_comp_im {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMapZero.UniqueHom ℂ A] [T2Space A] (f : ℝ → ℝ) (a : A) (hf : ContinuousOn f (quasispectrum ℝ ↑(imaginaryPart a)) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : IsStarNormal a := by cfc_tac) : cfcₙ (fun (x : ℂ) => ↑(f x.im)) a = cfcₙ f ↑(imaginaryPart a)

theorem cfc_re_id {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (hp : IsStarNormal a := by cfc_tac) : cfc (fun (x : ℂ) => ↑x.re) a = ↑(realPart a)

theorem cfc_im_id {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (hp : IsStarNormal a := by cfc_tac) : cfc (fun (x : ℂ) => ↑x.im) a = ↑(imaginaryPart a)

theorem spectrum_realPart {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : spectrum ℂ ↑(realPart a) = (fun (x : ℂ) => ↑x.re) '' spectrum ℂ a

theorem spectrum_realPart' {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : spectrum ℝ ↑(realPart a) = Complex.re '' spectrum ℂ a

theorem spectrum_imaginaryPart {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : spectrum ℂ ↑(imaginaryPart a) = (fun (x : ℂ) => ↑x.im) '' spectrum ℂ a

theorem spectrum_imaginaryPart' {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : IsStarNormal a := by cfc_tac) : spectrum ℝ ↑(imaginaryPart a) = Complex.im '' spectrum ℂ a

theorem cfc_realPart {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMap.UniqueHom ℂ A] (f : ℂ → ℂ) (a : A) (hf : ContinuousOn f (spectrum ℂ ↑(realPart a)) := by cfc_tac) (ha : IsStarNormal a := by cfc_tac) : cfc f ↑(realPart a) = cfc (fun (x : ℂ) => f ↑x.re) a

theorem cfc_imaginaryPart {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMap.UniqueHom ℂ A] (f : ℂ → ℂ) (a : A) (hf : ContinuousOn f (spectrum ℂ ↑(imaginaryPart a)) := by cfc_tac) (ha : IsStarNormal a := by cfc_tac) : cfc f ↑(imaginaryPart a) = cfc (fun (x : ℂ) => f ↑x.im) a

theorem cfc_comp_re {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMap.UniqueHom ℂ A] [T2Space A] (f : ℝ → ℝ) (a : A) (hf : ContinuousOn f (spectrum ℝ ↑(realPart a)) := by cfc_tac) (ha : IsStarNormal a := by cfc_tac) : cfc (fun (x : ℂ) => ↑(f x.re)) a = cfc f ↑(realPart a)

theorem cfc_comp_im {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMap.UniqueHom ℂ A] [T2Space A] (f : ℝ → ℝ) (a : A) (hf : ContinuousOn f (spectrum ℝ ↑(imaginaryPart a))) (ha : IsStarNormal a := by cfc_tac) : cfc (fun (x : ℂ) => ↑(f x.im)) a = cfc f ↑(imaginaryPart a)