Theorems · Theorem · probability

MeasureTheory.IsStronglyPredictable.measurable_add_one

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → E}, MeasureTheory.IsStronglyPredictable 𝓕 u → ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))

If u is a discrete predictable process, then u (n + 1) is 𝓕 n-measurable.

Defined in

Mathlib.Probability.Process.Predictable

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpace