Theorems · Theorem · functional analysis

ContinuousOn.cfc_nnreal

∀ {X : Type u_1} {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]
  [inst_10 : TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X},
  (∀ x ∈ t, IsCompact (s x)) →
    ContinuousOn a t →
      (∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum NNReal (a x) ⊆ s x₀) →
        (∀ x ∈ t, 0 ≤ a x) →
          autoParam (∀ x ∈ t, ContinuousOn f (s x)) ContinuousOn.cfc_nnreal._auto_1 →
            ContinuousOn (fun x => cfc f (a x)) t

Suppose a : X → Set A is continuous on t : Set X and 0 ≤ a x for all x ∈ t. Suppose further that s : X → Set ℝ≥0 is a family of sets with s x compact when x ∈ t such that s x₀ contains the spectrum of a x for all sufficiently close x ∈ t. If f : ℝ≥0 → ℝ≥0 is continuous on s x, for each x ∈ t, then fun x ↦ cfc f (a x) is continuous on t.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStarPartialOrderStarOrderedRingNonnegSpectrumClassT2SpaceIsSemitopologicalRingTopologicalSpace