Documentation

Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner

Inner products of strongly measurable functions are strongly measurable. #

Strongly measurable functions #

theorem MeasureTheory.StronglyMeasurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
theorem MeasureTheory.AEStronglyMeasurable.re {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {f : α𝕜} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => RCLike.re (f x)) μ
theorem MeasureTheory.AEStronglyMeasurable.im {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {f : α𝕜} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun (x : α) => RCLike.im (f x)) μ
theorem MeasureTheory.AEStronglyMeasurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : αE}, MeasureTheory.AEStronglyMeasurable f μMeasureTheory.AEStronglyMeasurable g μMeasureTheory.AEStronglyMeasurable (fun (x : α) => inner (f x) (g x)) μ