MeasureTheory.AEStronglyMeasurable.inner

theorem MeasureTheory.AEStronglyMeasurable.inner : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}, MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => ⟪f x, g x⟫_𝕜) μ

The theorem `MeasureTheory.AEStronglyMeasurable.inner` states that for any types `α`, `𝕜`, and `E`, any `RCLike` instance for `𝕜`, any `NormedAddCommGroup` instance for `E`, any `InnerProductSpace` instance for `𝕜` and `E`, any measurable space `x` as well as any measure `μ` on this measurable space, and any two functions `f` and `g` from `α` to `E`, if `f` and `g` are almost everywhere strongly measurable with respect to `μ`, then the function that maps each element of `α` to the inner product of `f(x)` and `g(x)` is also almost everywhere strongly measurable with respect to `μ`. Here, "almost everywhere strongly measurable" means that the function is the same "almost everywhere" as the limit of a sequence of simple functions.

More concisely: If `f` and `g` are almost everywhere strongly measurable functions from a measurable space `(α, Σ, μ)` to an inner product space `(E, ∣·∣)` over a normed field `𝕜`, then the function `x ↦ ∣f(x)∣² * ⟨f(x), g(x)⟩` is almost everywhere equal to a limit of simple functions.