Measurability of scalar products #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[measurability]
theorem
measurable.inner
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{m : measurable_space α}
[measurable_space E]
[opens_measurable_space E]
[topological_space.second_countable_topology E]
{f g : α → E}
(hf : measurable f)
(hg : measurable g) :
measurable (λ (t : α), has_inner.inner (f t) (g t))
@[measurability]
theorem
ae_measurable.inner
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{m : measurable_space α}
[measurable_space E]
[opens_measurable_space E]
[topological_space.second_countable_topology E]
{μ : measure_theory.measure α}
{f g : α → E}
(hf : ae_measurable f μ)
(hg : ae_measurable g μ) :
ae_measurable (λ (x : α), has_inner.inner (f x) (g x)) μ