Theorems · Theorem · probability

MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete

∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : TopologicalSpace ι] [DiscreteTopology ι]
  [SecondCountableTopology ι] [inst_5 : MeasurableSpace ι] [OpensMeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.IsStronglyProgressive f u

For filtrations indexed by a discrete order, StronglyAdapted and IsStronglyProgressive are equivalent. This lemma provides StronglyAdapted f u → IsStronglyProgressive f u. See IsStronglyProgressive.stronglyAdapted for the reverse direction, which is true more generally.

Defined in

Mathlib.Probability.Process.Adapted

Cited by

5 results in Mathlib

Foundations

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

Assumes

PreorderTopologicalSpaceTopologicalSpaceDiscreteTopologySecondCountableTopologyMeasurableSpaceOpensMeasurableSpaceTopologicalSpace.PseudoMetrizableSpace