L2M space

theorem MeasureTheory.Filtration.predictable_le_prod {T : Type u_1} {Ω : Type u_2} [LinearOrder T] [TopologicalSpace T] [OrderBot T] [OrderTopology T] [MeasurableSpace T] [BorelSpace T] {mΩ : MeasurableSpace Ω} (𝓕 : Filtration T mΩ) : 𝓕.predictable ≤ Prod.instMeasurableSpace

noncomputable def ProbabilityTheory.L2Predictable {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder T] [TopologicalSpace T] [OrderBot T] [OrderTopology T] [MeasurableSpace T] [BorelSpace T] [NormedAddCommGroup E] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration T mΩ} (μ : MeasureTheory.Measure T) (P : MeasureTheory.Measure Ω) : AddSubgroup (T × Ω →ₘ[(μ.prod P).trim ⋯] E)

L2 space of predictable processes with respect to a product measure.

Equations

• ProbabilityTheory.L2Predictable μ P = MeasureTheory.Lp E 2 ((μ.prod P).trim ⋯)