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} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
∀ {x : MeasurableSpace α} {f g : αE}, MeasureTheory.StronglyMeasurable fMeasureTheory.StronglyMeasurable gMeasureTheory.StronglyMeasurable fun (t : α) => f t, g t⟫_𝕜
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)) μ
theorem MeasureTheory.AEStronglyMeasurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : αE}, MeasureTheory.AEStronglyMeasurable f μMeasureTheory.AEStronglyMeasurable g μMeasureTheory.AEStronglyMeasurable (fun (x : α) => f x, g x⟫_𝕜) μ