Theorem: SchwartzMap.integralCLM'_apply (ForML/SchwartzLp.lean)

State before:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' 𝕜) f = ∫ (x : E), f x
Tactic:
rw [MeasureTheory.integral_eq _ f.integrable]
State after:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' 𝕜) f = L1.integral (Integrable.toL1 (fun x => f x) (_ : Integrable fun x => f x))

State before:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' 𝕜) f = L1.integral (Integrable.toL1 (fun x => f x) (_ : Integrable fun x => f x))
Tactic:
rw [integralCLM', L1.integral_def]
State after:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (ContinuousLinearMap.comp (L1.integralCLM' 𝕜) (toL1_CLM' 𝕜)) f =
    L1.integralCLM (Integrable.toL1 (fun x => f x) (_ : Integrable fun x => f x))

State before:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (ContinuousLinearMap.comp (L1.integralCLM' 𝕜) (toL1_CLM' 𝕜)) f =
    L1.integralCLM (Integrable.toL1 (fun x => f x) (_ : Integrable fun x => f x))
Tactic:
rfl
State after:
no goals