-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean
/-- The continuous functional calculus commutes with integration. -/
lemma cfc_integral [TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜)
    (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(spectrum 𝕜 a, 𝕜)]
    (hf₁ : ∀ x, ContinuousOn (f x) (spectrum 𝕜 a))
    (hf₂ : Continuous (fun x ↦ (⟨_, hf₁ x |>.restrict⟩ : C(spectrum 𝕜 a, 𝕜))))
    (hbound : ∀ x, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖)
    (hbound_finite_integral : HasFiniteIntegral bound μ) (ha : p a

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
x : X
⊢ ‖fc x‖ ≤ ‖bound x‖

Tactic:
rw [norm_le _ (norm_nonneg (bound x))]

Result:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
x : X
⊢ ∀ (x_1 : ↑(spectrum 𝕜 a)), ‖(fc x) x_1‖ ≤ ‖bound x‖

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
fc_integrable : Integrable fc μ
⊢ ((spectrum 𝕜 a).restrict fun x => ∫ (x_1 : X), f x_1 x ∂μ) = ⇑(∫ (x : X), fc x ∂μ)

Tactic:
ext

Result:
case h
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
fc_integrable : Integrable fc μ
x✝ : ↑(spectrum 𝕜 a)
⊢ (spectrum 𝕜 a).restrict (fun x => ∫ (x_1 : X), f x_1 x ∂μ) x✝ = (∫ (x : X), fc x ∂μ) x✝

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
⊢ Integrable fc μ

Tactic:
refine ⟨hf₂.aestronglyMeasurable, ?_⟩

Result:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
⊢ HasFiniteIntegral fc μ

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
x : X
⊢ ∀ (x_1 : ↑(spectrum 𝕜 a)), ‖(fc x) x_1‖ ≤ ‖bound x‖

Tactic:
exact fun z ↦ hbound x z.1 z.2

Result:
no goals