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]
:
∀ {x : MeasurableSpace α} {f g : α → E},
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun (t : α) => ⟪f t, g t⟫_𝕜
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 : α) => ⟪f x, g x⟫_𝕜) μ