Theorems · Theorem · functional analysis

continuousOn_cfc_setProd

∀ {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] {s : Set 𝕜},
  IsCompact s →
    ContinuousOn (fun fa => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2)
      ({f | ContinuousOn ((UniformOnFun.toFun {s}) f) s} ×ˢ {a | p a ∧ spectrum 𝕜 a ⊆ s})

Let s : Set 𝕜 be a compact set and consider pairs (f, a) : (𝕜 → 𝕜) × A where f is continuous on s and spectrum 𝕜 a ⊆ s and a satisfies the predicate p a for the continuous functional calculus. Then cfc is jointly continuous in both variables (i.e., continuous in its uncurried form) on this set of pairs when the function space is equipped with the topology of uniform convergence on s.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

1 results in Mathlib

Foundations

Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStar