Theorems · Definition · probability

MeasureTheory.IsStronglyProgressive

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

Strongly progressive process. A sequence of functions u is said to be strongly progressive with respect to a filtration f if at each point in time i, u restricted to Set.Iic i × Ω is strongly measurable with respect to the product MeasurableSpace structure where the σ-algebra used for Ω is f i. The usual definition uses the interval [0,i], which we replace by Set.Iic i. We recover the usual definition for index types ℝ≥0 or ℕ.

Defined in

Mathlib.Probability.Process.Adapted

Cited by

54 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderTopologicalSpaceMeasurableSpace