Theorems · Definition · probability

MeasureTheory.Filtration.predictable

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

Given a filtration 𝓕, the predictable σ-algebra is the σ-algebra on ι × Ω generated by sets of the form (t, ∞) × A for t ∈ ι and A ∈ 𝓕 t and {⊥} × A for A ∈ 𝓕 ⊥.

Defined in

Mathlib.Probability.Process.Predictable

Cited by

10 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

PreorderOrderBot