Theorems · Definition · probability

MeasureTheory.StronglyAdapted

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

A sequence of functions u is strongly adapted to a filtration f if for all i, u i is f i-strongly measurable.

Defined in

Mathlib.Probability.Process.Adapted

Cited by

81 results in Mathlib

Foundations

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

Assumes

PreorderTopologicalSpace