Inner products of strongly measurable functions are strongly measurable. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Strongly measurable functions #
@[protected]
theorem
measure_theory.strongly_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 α}
{f g : α → E}
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.strongly_measurable g) :
measure_theory.strongly_measurable (λ (t : α), has_inner.inner (f t) (g t))
@[protected]
theorem
measure_theory.ae_strongly_measurable.re
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{f : α → 𝕜}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), ⇑is_R_or_C.re (f x)) μ
@[protected]
theorem
measure_theory.ae_strongly_measurable.im
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{f : α → 𝕜}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (x : α), ⇑is_R_or_C.im (f x)) μ
@[protected]
theorem
measure_theory.ae_strongly_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 α}
{μ : measure_theory.measure α}
{f g : α → E}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ) :
measure_theory.ae_strongly_measurable (λ (x : α), has_inner.inner (f x) (g x)) μ