Theorems · Theorem · functional analysis

integrable_cfc

∀ {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 : TopologicalSpace X] [OpensMeasurableSpace X]
  (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)],
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ spectrum 𝕜 a) →
    (∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
      MeasureTheory.HasFiniteIntegral bound μ →
        autoParam (p a) integrable_cfc._auto_1 → MeasureTheory.Integrable (fun x => cfc (f x) a) μ

An integrability criterion for the continuous functional calculus. This version assumes joint continuity of f, see integrable_cfc' for a statement with weaker assumptions.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeMeasurableSpaceNormedRingStarRingNormedAlgebraContinuousFunctionalCalculusCompleteSpaceTopologicalSpaceOpensMeasurableSpaceSecondCountableTopologyEither