Theorems · Theorem · probability

MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous

∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : TopologicalSpace ι]
  [TopologicalSpace.MetrizableSpace ι] [SecondCountableTopology ι] [inst_5 : MeasurableSpace ι] [OpensMeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.StronglyAdapted f u → (∀ (ω : Ω), Continuous fun i => u i ω) → MeasureTheory.IsStronglyProgressive f u

A continuous and strongly adapted process is strongly progressive.

Defined in

Mathlib.Probability.Process.Adapted

Cited by

4 results in Mathlib

Foundations

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

Assumes

PreorderTopologicalSpaceTopologicalSpaceTopologicalSpace.MetrizableSpaceSecondCountableTopologyMeasurableSpaceOpensMeasurableSpaceTopologicalSpace.PseudoMetrizableSpace