Theorems · Definition · probability

MeasureTheory.IsStronglyPredictable

{Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      {E : Type u_3} →
        [TopologicalSpace E] → [inst : Preorder ι] → [OrderBot ι] → MeasureTheory.Filtration ι m → (ι → Ω → E) → Prop

A process is said to be predictable if it is measurable with respect to the predictable σ-algebra.

Defined in

Mathlib.Probability.Process.Predictable

Cited by

17 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpacePreorderOrderBot