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}
(hf : StronglyMeasurable f)
(hg : StronglyMeasurable g)
:
StronglyMeasurable fun (t : α) => inner 𝕜 (f t) (g t)
theorem
MeasureTheory.AEStronglyMeasurable.re
{α : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → 𝕜}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : α) => RCLike.re (f x)) μ
theorem
MeasureTheory.AEStronglyMeasurable.im
{α : Type u_1}
{𝕜 : Type u_2}
[RCLike 𝕜]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → 𝕜}
(hf : AEStronglyMeasurable f μ)
:
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]
{m x✝ : MeasurableSpace α}
{μ : Measure α}
{f g : α → E}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
:
AEStronglyMeasurable (fun (x : α) => inner 𝕜 (f x) (g x)) μ
theorem
MeasureTheory.AEStronglyMeasurable.inner_const
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{f : α → E}
{c : E}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : α) => inner 𝕜 (f x) c) μ
theorem
MeasureTheory.AEStronglyMeasurable.const_inner
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{m m₀ : MeasurableSpace α}
{μ : Measure α}
{g : α → E}
{c : E}
(hg : AEStronglyMeasurable g μ)
:
AEStronglyMeasurable (fun (x : α) => inner 𝕜 c (g x)) μ