Documentation

Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner

Inner products of strongly measurable functions are strongly measurable. #

Strongly measurable functions #

theorem MeasureTheory.AEStronglyMeasurable.re {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [IsROrC 𝕜] {f : α𝕜} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun x => IsROrC.re (f x)) μ
theorem MeasureTheory.AEStronglyMeasurable.im {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [IsROrC 𝕜] {f : α𝕜} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun x => IsROrC.im (f x)) μ