Documentation

Mathlib.MeasureTheory.Function.SpecialFunctions.Inner

Measurability of scalar products #

theorem Measurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E] [inst_2 : TopologicalSpace.SecondCountableTopology E] {f g : αE}, Measurable fMeasurable gMeasurable fun t => inner (f t) (g t)
theorem Measurable.const_inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E] [inst_2 : TopologicalSpace.SecondCountableTopology E] {c : E} {f : αE}, Measurable fMeasurable fun t => inner c (f t)
theorem Measurable.inner_const {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : OpensMeasurableSpace E] [inst_2 : TopologicalSpace.SecondCountableTopology E] {c : E} {f : αE}, Measurable fMeasurable fun t => inner (f t) c
theorem AEMeasurable.inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E] [TopologicalSpace.SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (hf : AEMeasurable f) (hg : AEMeasurable g) :
AEMeasurable fun x => inner (f x) (g x)
theorem AEMeasurable.const_inner {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E] [TopologicalSpace.SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f : αE} {c : E} (hf : AEMeasurable f) :
AEMeasurable fun x => inner c (f x)
theorem AEMeasurable.inner_const {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E] [TopologicalSpace.SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f : αE} {c : E} (hf : AEMeasurable f) :
AEMeasurable fun x => inner (f x) c