Theorems · Theorem · functional analysis

Continuous.cfc_nnreal_of_mem_nhdsSet

∀ {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]
  [CompleteSpace A] [inst_11 : TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A},
  s ∈ nhdsSet (⋃ x, spectrum NNReal (a x)) →
    Continuous a →
      autoParam (∀ (x : X), 0 ≤ a x) Continuous.cfc_nnreal_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) Continuous.cfc_nnreal_of_mem_nhdsSet._auto_3 → Continuous fun x => cfc f (a x)

If f : ℝ≥0 → ℝ≥0 is continuous on s and a : X → A is continuous and a x is nonnegative for all x and s is a common neighborhood of the spectra of a x for all x, then fun x ↦ cfc f (a x) is continuous. This is weaker than Continuous.cfc_nnreal since it requires f to be continuous on a neighborhood of the spectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using Continuous.cfc_nnreal and upperHemicontinuous_spectrum_nnreal to produce the necessary family of compact sets.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStarPartialOrderStarOrderedRingNonnegSpectrumClassT2SpaceIsSemitopologicalRingCompleteSpaceTopologicalSpace