Theorems · Theorem · functional analysis

cfcL_integral

∀ {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] [inst_6 : CompleteSpace A] [inst_7 : NormedSpace ℝ A] (a : A)
  (f : X → C(↑(spectrum 𝕜 a), 𝕜)),
  MeasureTheory.Integrable f μ →
    ∀ (ha : autoParam (p a) cfcL_integral._auto_1), ∫ (x : X), (cfcL ha) (f x) ∂μ = (cfcL ha) (∫ (x : X), f x ∂μ)

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeMeasurableSpaceNormedRingStarRingNormedAlgebraContinuousFunctionalCalculusCompleteSpaceNormedSpace