Theorems · Theorem · functional analysis

continuousOn_cfc_nnreal_setProd

∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  {s : Set NNReal},
  IsCompact s →
    ContinuousOn (fun fa => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2)
      ({f | ContinuousOn ((UniformOnFun.toFun {s}) f) s} ×ˢ {a | 0 ≤ a ∧ spectrum NNReal a ⊆ s})

Let s : Set ℝ≥0 be a compact set and consider pairs (f, a) : (ℝ≥0 → ℝ≥0) × A where f is continuous on s and spectrum ℝ≥0 a ⊆ s and 0 ≤ a. 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 200 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStarPartialOrderStarOrderedRingNonnegSpectrumClassT2SpaceIsSemitopologicalRing