Measurability of scalar products #
theorem
Measurable.inner
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
:
∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E]
[inst_2 : SecondCountableTopology E] {f g : α → E},
Measurable f → Measurable g → Measurable fun (t : α) => ⟪f t, g t⟫_𝕜
theorem
Measurable.const_inner
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
:
∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E]
[inst_2 : SecondCountableTopology E] {c : E} {f : α → E}, Measurable f → Measurable fun (t : α) => ⟪c, f t⟫_𝕜
theorem
Measurable.inner_const
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
:
∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E]
[inst_2 : SecondCountableTopology E] {c : E} {f : α → E}, Measurable f → Measurable fun (t : α) => ⟪f t, c⟫_𝕜
theorem
AEMeasurable.inner
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{m : MeasurableSpace α}
[MeasurableSpace E]
[OpensMeasurableSpace E]
[SecondCountableTopology E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{g : α → E}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
AEMeasurable (fun (x : α) => ⟪f x, g x⟫_𝕜) μ
theorem
AEMeasurable.const_inner
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{m : MeasurableSpace α}
[MeasurableSpace E]
[OpensMeasurableSpace E]
[SecondCountableTopology E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{c : E}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => ⟪c, f x⟫_𝕜) μ
theorem
AEMeasurable.inner_const
{α : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{m : MeasurableSpace α}
[MeasurableSpace E]
[OpensMeasurableSpace E]
[SecondCountableTopology E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{c : E}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : α) => ⟪f x, c⟫_𝕜) μ