The continuous functional calculus on product types #
This file contains results about the continuous functional calculus on (indexed) product types.
Main theorems #
cfc_map_piandcfcₙ_map_pi: givena : ∀ i, A i, thencfc f a = fun i => cfc f (a i)(and likewise for the non-unital version)cfc_map_prodandcfcₙ_map_prod: givena : Aandb : B, thencfc f (a, b) = (cfc f a, cfc f b)(and likewise for the non-unital version)
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)
:
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)
:
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)
:
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)
: