# Measurability of scalar products #

theorem Measurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [] [] :
∀ {x : } [inst : ] [inst_1 : ] [inst_2 : ] {f g : αE}, Measurable fun (t : α) => f t, g t⟫_𝕜
theorem Measurable.const_inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [] [] :
∀ {x : } [inst : ] [inst_1 : ] [inst_2 : ] {c : E} {f : αE}, Measurable fun (t : α) => c, f t⟫_𝕜
theorem Measurable.inner_const {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [] [] :
∀ {x : } [inst : ] [inst_1 : ] [inst_2 : ] {c : E} {f : αE}, Measurable fun (t : α) => f t, c⟫_𝕜
theorem AEMeasurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [] [] {m : } [] {μ : } {f : αE} {g : αE} (hf : ) (hg : ) :
AEMeasurable (fun (x : α) => f x, g x⟫_𝕜) μ
theorem AEMeasurable.const_inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [] [] {m : } [] {μ : } {f : αE} {c : E} (hf : ) :
AEMeasurable (fun (x : α) => c, f x⟫_𝕜) μ
theorem AEMeasurable.inner_const {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [] [] {m : } [] {μ : } {f : αE} {c : E} (hf : ) :
AEMeasurable (fun (x : α) => f x, c⟫_𝕜) μ