mathlib documentation

measure_theory.function.special_functions.inner

Measurability of scalar products #

@[measurability]
theorem measurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [is_R_or_C 𝕜] [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 𝕜] [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)) μ