# The continuous functional calculus on product types #

This file contains results about the continuous functional calculus on (indexed) product types.

## Main theorems #

- `cfc_map_pi` and `cfcₙ_map_pi`: given `a : ∀ i, A i`, then `cfc f a = fun i => cfc f (a i)` (and likewise for the non-unital version)
- `cfc_map_prod` and `cfcₙ_map_prod`: given `a : A` and `b : B`, then `cfc f (a, b) = (cfc f a, cfc f b)` (and likewise for the non-unital version)

source
theorem cfcₙ_map_pi {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : ι → Type u_4} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S] [(i : ι) → NonUnitalRing (A i)] [(i : ι) → Module S (A i)] [(i : ι) → Module R (A i)] [∀ (i : ι), IsScalarTower R S (A i)] [∀ (i : ι), SMulCommClass R (A i) (A i)] [∀ (i : ι), IsScalarTower R (A i) (A i)] [(i : ι) → StarRing (A i)] [(i : ι) → TopologicalSpace (A i)] {p : ((i : ι) → A i) → Prop} {q : (i : ι) → A i → Prop} [NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p] [∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)] [∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)] (f : R → R) (a : (i : ι) → A i) (hf : ContinuousOn f (⋃ (i : ι), quasispectrum R (a i)) := by cfc_cont_tac) (ha : p a := by cfc_tac) (ha' : ∀ (i : ι), q i (a i) := by cfc_tac) :
cfcₙ f a = fun (i : ι) => cfcₙ f (a i)
source
theorem cfcₙ_map_prod {A : Type u_1} {B : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommRing S] [Nontrivial R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Algebra R S] [NonUnitalRing A] [NonUnitalRing B] [Module S A] [Module R A] [Module R B] [Module S B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] [StarRing A] [StarRing B] [TopologicalSpace A] [TopologicalSpace B] [IsScalarTower R S A] [IsScalarTower R S B] {pab : A × B → Prop} {pa : A → Prop} {pb : B → Prop} [NonUnitalContinuousFunctionalCalculus R (A × B) pab] [NonUnitalContinuousFunctionalCalculus R A pa] [NonUnitalContinuousFunctionalCalculus R B pb] [ContinuousMapZero.UniqueHom R A] [ContinuousMapZero.UniqueHom R B] (f : R → R) (a : A) (b : B) (hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b) := by cfc_cont_tac) (hab : pab (a, b) := by cfc_tac) (ha : pa a := by cfc_tac) (hb : pb b := by cfc_tac) :
cfcₙ f (a, b) = (cfcₙ f a, cfcₙ f b)
source
theorem cfc_map_pi {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : ι → Type u_4} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S] [(i : ι) → Ring (A i)] [(i : ι) → Algebra S (A i)] [(i : ι) → Algebra R (A i)] [∀ (i : ι), IsScalarTower R S (A i)] [hinst : IsScalarTower R S ((i : ι) → A i)] [(i : ι) → StarRing (A i)] [(i : ι) → TopologicalSpace (A i)] {p : ((i : ι) → A i) → Prop} {q : (i : ι) → A i → Prop} [ContinuousFunctionalCalculus R ((i : ι) → A i) p] [∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)] [∀ (i : ι), ContinuousMap.UniqueHom R (A i)] (f : R → R) (a : (i : ι) → A i) (hf : ContinuousOn f (⋃ (i : ι), spectrum R (a i)) := by cfc_cont_tac) (ha : p a := by cfc_tac) (ha' : ∀ (i : ι), q i (a i) := by cfc_tac) :
cfc f a = fun (i : ι) => cfc f (a i)
source
theorem cfc_map_prod {A : Type u_1} {B : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S] [Ring A] [Ring B] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [StarRing A] [StarRing B] [TopologicalSpace A] [TopologicalSpace B] {pab : A × B → Prop} {pa : A → Prop} {pb : B → Prop} [ContinuousFunctionalCalculus R (A × B) pab] [ContinuousFunctionalCalculus R A pa] [ContinuousFunctionalCalculus R B pb] [ContinuousMap.UniqueHom R A] [ContinuousMap.UniqueHom R B] (f : R → R) (a : A) (b : B) (hf : ContinuousOn f (spectrum R a ∪ spectrum R b) := by cfc_cont_tac) (hab : pab (a, b) := by cfc_tac) (ha : pa a := by cfc_tac) (hb : pb b := by cfc_tac) :
cfc f (a, b) = (cfc f a, cfc f b)