Integrals and the continuous functional calculus #
This file gives results about integrals of the form ∫ x, cfc (f x) a. Most notably, we show
that the integral commutes with the continuous functional calculus under appropriate conditions.
Main declarations #
cfc_setIntegral(resp.cfc_integral): given a functionf : X → 𝕜 → 𝕜, we have thatcfc (fun r => ∫ x in s, f x r ∂μ) a = ∫ x in s, cfc (f x) a ∂μunder appropriate conditions (resp. withs = univ)cfcₙ_setIntegral,cfcₙ_integral: the same for the non-unital continuous functional calculusintegrableOn_cfc,integrableOn_cfcₙ,integrable_cfc,integrable_cfcₙ: functions of the formfun x => cfc (f x) aare integrable.
Implementation Notes #
The lemmas mentioned above are stated under much stricter hypotheses than necessary
(typically, simultaneous continuity of f in the parameter and the spectrum element).
They all come with primed version which only assume what's needed, and may be used together
with the API developed in Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap.
TODO #
- Lift this to the case where the CFC is over
ℝ≥0 - Use this to prove operator monotonicity and concavity/convexity of
rpowandlog
theorem
cfcL_integral
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
(a : A)
(f : X → C(↑(spectrum 𝕜 a), 𝕜))
(hf₁ : MeasureTheory.Integrable f μ)
(ha : p a := by cfc_tac)
:
theorem
cfcL_integrable
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
(a : A)
(f : X → C(↑(spectrum 𝕜 a), 𝕜))
(hf₁ : MeasureTheory.Integrable f μ)
(ha : p a := by cfc_tac)
:
MeasureTheory.Integrable (fun (x : X) => (cfcL ha) (f x)) μ
theorem
cfcHom_integral
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
(a : A)
(f : X → C(↑(spectrum 𝕜 a), 𝕜))
(hf₁ : MeasureTheory.Integrable f μ)
(ha : p a := by cfc_tac)
:
theorem
integrable_cfc'
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
(f : X → 𝕜 → 𝕜)
(a : A)
(hf : MeasureTheory.Integrable (fun (x : X) => ContinuousMap.mkD ((spectrum 𝕜 a).restrict (f x)) 0) μ)
(ha : p a := by cfc_tac)
:
MeasureTheory.Integrable (fun (x : X) => cfc (f x) a) μ
An integrability criterion for the continuous functional calculus.
For a version with stronger assumptions which in practice are often easier to verify, see
integrable_cfc.
theorem
integrableOn_cfc'
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
{s : Set X}
(f : X → 𝕜 → 𝕜)
(a : A)
(hf : MeasureTheory.IntegrableOn (fun (x : X) => ContinuousMap.mkD ((spectrum 𝕜 a).restrict (f x)) 0) s μ)
(ha : p a := by cfc_tac)
:
MeasureTheory.IntegrableOn (fun (x : X) => cfc (f x) a) s μ
An integrability criterion for the continuous functional calculus.
For a version with stronger assumptions which in practice are often easier to verify, see
integrableOn_cfc.
theorem
integrable_cfc
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[TopologicalSpace X]
[OpensMeasurableSpace X]
(f : X → 𝕜 → 𝕜)
(bound : X → ℝ)
(a : A)
[SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)]
(hf : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ spectrum 𝕜 a))
(bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x)
(bound_int : MeasureTheory.HasFiniteIntegral bound μ)
(ha : p a := by cfc_tac)
:
MeasureTheory.Integrable (fun (x : 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.
theorem
integrableOn_cfc
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[TopologicalSpace X]
[OpensMeasurableSpace X]
{s : Set X}
(hs : MeasurableSet s)
(f : X → 𝕜 → 𝕜)
(bound : X → ℝ)
(a : A)
[SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)]
(hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a))
(bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x)
(bound_int : MeasureTheory.HasFiniteIntegral bound (μ.restrict s))
(ha : p a := by cfc_tac)
:
MeasureTheory.IntegrableOn (fun (x : X) => cfc (f x) a) s μ
An integrability criterion for the continuous functional calculus.
This version assumes joint continuity of f, see integrableOn_cfc' for a statement
with weaker assumptions.
theorem
cfc_integral'
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
(f : X → 𝕜 → 𝕜)
(a : A)
(hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a))
(hf₂ : MeasureTheory.Integrable (fun (x : X) => ContinuousMap.mkD ((spectrum 𝕜 a).restrict (f x)) 0) μ)
(ha : p a := by cfc_tac)
:
The continuous functional calculus commutes with integration.
For a version with stronger assumptions which in practice are often easier to verify, see
cfc_integral.
theorem
cfc_setIntegral'
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
{s : Set X}
[NormedSpace ℝ A]
(f : X → 𝕜 → 𝕜)
(a : A)
(hf₁ : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a))
(hf₂ : MeasureTheory.IntegrableOn (fun (x : X) => ContinuousMap.mkD ((spectrum 𝕜 a).restrict (f x)) 0) s μ)
(ha : p a := by cfc_tac)
:
The continuous functional calculus commutes with integration.
For a version with stronger assumptions which in practice are often easier to verify, see
cfc_setIntegral.
theorem
cfc_integral
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
[TopologicalSpace X]
[OpensMeasurableSpace X]
(f : X → 𝕜 → 𝕜)
(bound : X → ℝ)
(a : A)
[SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)]
(hf : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ spectrum 𝕜 a))
(bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x)
(bound_int : MeasureTheory.HasFiniteIntegral bound μ)
(ha : p a := by cfc_tac)
:
The continuous functional calculus commutes with integration.
This version assumes joint continuity of f, see cfc_integral' for a statement
with weaker assumptions.
theorem
cfc_setIntegral
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NormedRing A]
[StarRing A]
[NormedAlgebra 𝕜 A]
[ContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
[TopologicalSpace X]
[OpensMeasurableSpace X]
{s : Set X}
(hs : MeasurableSet s)
(f : X → 𝕜 → 𝕜)
(bound : X → ℝ)
(a : A)
[SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)]
(hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a))
(bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x)
(bound_int : MeasureTheory.HasFiniteIntegral bound (μ.restrict s))
(ha : p a := by cfc_tac)
:
The continuous functional calculus commutes with integration.
This version assumes joint continuity of f, see cfc_setIntegral' for a statement
with weaker assumptions.
theorem
cfcₙL_integral
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
(a : A)
(f : X → ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜)
(hf₁ : MeasureTheory.Integrable f μ)
(ha : p a := by cfc_tac)
:
theorem
cfcₙHom_integral
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
(a : A)
(f : X → ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜)
(hf₁ : MeasureTheory.Integrable f μ)
(ha : p a := by cfc_tac)
:
theorem
cfcₙL_integrable
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
(a : A)
(f : X → ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜)
(hf₁ : MeasureTheory.Integrable f μ)
(ha : p a := by cfc_tac)
:
MeasureTheory.Integrable (fun (x : X) => (cfcₙL ha) (f x)) μ
theorem
integrable_cfcₙ'
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
(f : X → 𝕜 → 𝕜)
(a : A)
(hf : MeasureTheory.Integrable (fun (x : X) => ContinuousMapZero.mkD ((quasispectrum 𝕜 a).restrict (f x)) 0) μ)
(ha : p a := by cfc_tac)
:
MeasureTheory.Integrable (fun (x : X) => cfcₙ (f x) a) μ
An integrability criterion for the continuous functional calculus.
For a version with stronger assumptions which in practice are often easier to verify, see
integrable_cfcₙ.
theorem
integrableOn_cfcₙ'
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
{s : Set X}
(f : X → 𝕜 → 𝕜)
(a : A)
(hf : MeasureTheory.IntegrableOn (fun (x : X) => ContinuousMapZero.mkD ((quasispectrum 𝕜 a).restrict (f x)) 0) s μ)
(ha : p a := by cfc_tac)
:
MeasureTheory.IntegrableOn (fun (x : X) => cfcₙ (f x) a) s μ
An integrability criterion for the continuous functional calculus.
For a version with stronger assumptions which in practice are often easier to verify, see
integrableOn_cfcₙ.
theorem
integrable_cfcₙ
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[TopologicalSpace X]
[OpensMeasurableSpace X]
(f : X → 𝕜 → 𝕜)
(bound : X → ℝ)
(a : A)
[SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)]
(hf : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ quasispectrum 𝕜 a))
(f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0)
(bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x)
(bound_int : MeasureTheory.HasFiniteIntegral bound μ)
(ha : p a := by cfc_tac)
:
MeasureTheory.Integrable (fun (x : 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.
theorem
integrableOn_cfcₙ
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[TopologicalSpace X]
[OpensMeasurableSpace X]
{s : Set X}
(hs : MeasurableSet s)
(f : X → 𝕜 → 𝕜)
(bound : X → ℝ)
(a : A)
[SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)]
(hf : ContinuousOn (Function.uncurry f) (s ×ˢ quasispectrum 𝕜 a))
(f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0)
(bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x)
(bound_int : MeasureTheory.HasFiniteIntegral bound (μ.restrict s))
(ha : p a := by cfc_tac)
:
MeasureTheory.IntegrableOn (fun (x : X) => cfcₙ (f x) a) s μ
An integrability criterion for the continuous functional calculus.
This version assumes joint continuity of f, see integrableOn_cfcₙ' for a statement
with weaker assumptions.
theorem
cfcₙ_integral'
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
(f : X → 𝕜 → 𝕜)
(a : A)
(hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a))
(hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0)
(hf₃ : MeasureTheory.Integrable (fun (x : X) => ContinuousMapZero.mkD ((quasispectrum 𝕜 a).restrict (f x)) 0) μ)
(ha : p a := by cfc_tac)
:
The continuous functional calculus commutes with integration.
For a version with stronger assumptions which in practice are often easier to verify, see
cfcₙ_integral.
theorem
cfcₙ_setIntegral'
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
{s : Set X}
[NormedSpace ℝ A]
(f : X → 𝕜 → 𝕜)
(a : A)
(hf₁ : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a))
(hf₂ : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0)
(hf₃ : MeasureTheory.IntegrableOn (fun (x : X) => ContinuousMapZero.mkD ((quasispectrum 𝕜 a).restrict (f x)) 0) s μ)
(ha : p a := by cfc_tac)
:
The continuous functional calculus commutes with integration.
For a version with stronger assumptions which in practice are often easier to verify, see
cfcₙ_setIntegral.
theorem
cfcₙ_integral
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
[TopologicalSpace X]
[OpensMeasurableSpace X]
(f : X → 𝕜 → 𝕜)
(bound : X → ℝ)
(a : A)
[SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)]
(hf : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ quasispectrum 𝕜 a))
(f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0)
(bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x)
(bound_int : MeasureTheory.HasFiniteIntegral bound μ)
(ha : p a := by cfc_tac)
:
The continuous functional calculus commutes with integration.
This version assumes joint continuity of f, see cfcₙ_integral' for a statement
with weaker assumptions.
theorem
cfcₙ_setIntegral
{X : Type u_1}
{𝕜 : Type u_2}
{A : Type u_3}
{p : A → Prop}
[RCLike 𝕜]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[NonUnitalContinuousFunctionalCalculus 𝕜 A p]
[CompleteSpace A]
[NormedSpace ℝ A]
[TopologicalSpace X]
[OpensMeasurableSpace X]
{s : Set X}
(hs : MeasurableSet s)
(f : X → 𝕜 → 𝕜)
(bound : X → ℝ)
(a : A)
[SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)]
(hf : ContinuousOn (Function.uncurry f) (s ×ˢ quasispectrum 𝕜 a))
(f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0)
(bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x)
(bound_int : MeasureTheory.HasFiniteIntegral bound (μ.restrict s))
(ha : p a := by cfc_tac)
:
The continuous functional calculus commutes with integration.
This version assumes joint continuity of f, see cfcₙ_setIntegral' for a statement
with weaker assumptions.