Theorems · Theorem · probability

MeasureTheory.integrable_stoppedProcess

∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [inst_1 : LinearOrder ι] [inst_2 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m} [inst_5 : NormedAddCommGroup E]
  [LocallyFiniteOrderBot ι],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.Integrable (u n) μ) →
      ∀ (n : ι), MeasureTheory.Integrable (MeasureTheory.stoppedProcess u τ n) μ

Defined in

Mathlib.Probability.Process.Stopping

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonemptyLinearOrderTopologicalSpaceOrderTopologyFirstCountableTopologyNormedAddCommGroupLocallyFiniteOrderBot