mathlib documentation

measure_theory.function.strongly_measurable.inner

Inner products of strongly measurable functions are strongly measurable. #

Strongly measurable functions #

source
@[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))
source
@[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)) μ
source
@[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)) μ
source
@[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)) μ