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_integral: given a function f : X → 𝕜 → 𝕜, we have that cfc (fun r => ∫ x, f x r ∂μ) a = ∫ x, cfc (f x) a ∂μ under appropriate conditions
• cfcₙ_integral: given a function f : X → 𝕜 → 𝕜, we have that cfcₙ (fun r => ∫ x, f x r ∂μ) a = ∫ x, cfcₙ (f x) a ∂μ under appropriate conditions

TODO

• Lift this to the case where the CFC is over ℝ≥0
• Use this to prove operator monotonicity and concavity/convexity of rpow and log

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] [NormedAlgebra ℝ A] [CompleteSpace A] [ContinuousFunctionalCalculus 𝕜 p] (a : A) (f : X → C(↑(spectrum 𝕜 a), 𝕜)) (hf₁ : MeasureTheory.Integrable f μ) (ha : p a := by cfc_tac) : ∫ (x : X), (cfcL ha) (f x) ∂μ = (cfcL ha) (∫ (x : X), 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] [NormedAlgebra ℝ A] [CompleteSpace A] [ContinuousFunctionalCalculus 𝕜 p] (a : A) (f : X → C(↑(spectrum 𝕜 a), 𝕜)) (hf₁ : MeasureTheory.Integrable f μ) (ha : p a := by cfc_tac) : ∫ (x : X), (cfcHom ha) (f x) ∂μ = (cfcHom ha) (∫ (x : X), f x ∂μ)

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] [NormedAlgebra ℝ A] [CompleteSpace A] [ContinuousFunctionalCalculus 𝕜 p] [TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)] (hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)) (hf₂ : Continuous fun (x : X) => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }) (hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖) (hbound_finite_integral : MeasureTheory.HasFiniteIntegral bound μ) (ha : p a := by cfc_tac) : cfc (fun (r : 𝕜) => ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

The continuous functional calculus commutes with integration.

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] [NormedAlgebra ℝ A] [CompleteSpace A] [ContinuousFunctionalCalculus 𝕜 p] [TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)] (hf : Continuous (Function.uncurry fun (x : X) => (spectrum 𝕜 a).restrict (f x))) (hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖) (hbound_finite_integral : MeasureTheory.HasFiniteIntegral bound μ) (ha : p a := by cfc_tac) : cfc (fun (r : 𝕜) => ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

The continuous functional calculus commutes with integration.

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] [CompleteSpace A] [NormedSpace 𝕜 A] [NormedSpace ℝ A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 p] (a : A) (f : X → ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) (hf₁ : MeasureTheory.Integrable f μ) (ha : p a := by cfc_tac) : ∫ (x : X), (cfcₙL ha) (f x) ∂μ = (cfcₙL ha) (∫ (x : X), f x ∂μ)

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] [CompleteSpace A] [NormedSpace 𝕜 A] [NormedSpace ℝ A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 p] (a : A) (f : X → ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) (hf₁ : MeasureTheory.Integrable f μ) (ha : p a := by cfc_tac) : ∫ (x : X), (cfcₙHom ha) (f x) ∂μ = (cfcₙHom ha) (∫ (x : X), f x ∂μ)

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] [CompleteSpace A] [NormedSpace 𝕜 A] [NormedSpace ℝ A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 p] [TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X (ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜)] (hf₁ : ∀ (x : X), ContinuousOn (f x) (quasispectrum 𝕜 a)) (hf₂ : ∀ (x : X), f x 0 = 0) (hf₃ : Continuous fun (x : X) => { toFun := (quasispectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯, map_zero' := ⋯ }) (hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖) (hbound_finite_integral : MeasureTheory.HasFiniteIntegral bound μ) (ha : p a := by cfc_tac) : cfcₙ (fun (r : 𝕜) => ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ

The non-unital continuous functional calculus commutes with integration.

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] [CompleteSpace A] [NormedSpace 𝕜 A] [NormedSpace ℝ A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 p] [TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X (ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜)] (hf : Continuous (Function.uncurry fun (x : X) => (quasispectrum 𝕜 a).restrict (f x))) (hf₂ : ∀ (x : X), f x 0 = 0) (hbound : ∀ (x : X), ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖) (hbound_finite_integral : MeasureTheory.HasFiniteIntegral bound μ) (ha : p a := by cfc_tac) : cfcₙ (fun (r : 𝕜) => ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ

The non-unital continuous functional calculus commutes with integration.