Theorems · Theorem · functional analysis

cfc_setIntegral

∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] [inst_7 : NormedSpace ℝ A]
  [inst_8 : TopologicalSpace X] [OpensMeasurableSpace X] {s : Set X},
  MeasurableSet s →
    ∀ (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)],
      ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a) →
        (∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
          MeasureTheory.HasFiniteIntegral bound (μ.restrict s) →
            autoParam (p a) cfc_setIntegral._auto_1 →
              cfc (fun r => ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfc (f x) a ∂μ

The continuous functional calculus commutes with integration. This version assumes joint continuity of f, see cfc_setIntegral' for a statement with weaker assumptions.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeMeasurableSpaceNormedRingStarRingNormedAlgebraContinuousFunctionalCalculusCompleteSpaceNormedSpaceTopologicalSpaceOpensMeasurableSpaceSecondCountableTopologyEither