[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : TopologicalSpace.SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ AEMeasurable fun x => Inner.inner (f x) (g x)
[PROOFSTEP]
refine' ⟨fun x => ⟪hf.mk f x, hg.mk g x⟫, hf.measurable_mk.inner hg.measurable_mk, _⟩
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : TopologicalSpace.SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ (fun x => Inner.inner (f x) (g x)) =ᶠ[MeasureTheory.Measure.ae μ] fun x => Inner.inner (mk f hf x) (mk g hg x)
[PROOFSTEP]
refine' hf.ae_eq_mk.mp (hg.ae_eq_mk.mono fun x hxg hxf => _)
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : TopologicalSpace.SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hxg : g x = mk g hg x
hxf : f x = mk f hf x
⊢ (fun x => Inner.inner (f x) (g x)) x = (fun x => Inner.inner (mk f hf x) (mk g hg x)) x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : TopologicalSpace.SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hxg : g x = mk g hg x
hxf : f x = mk f hf x
⊢ Inner.inner (f x) (g x) = Inner.inner (mk f hf x) (mk g hg x)
[PROOFSTEP]
congr
