Theorems · Theorem · probability

MeasureTheory.integrable_stoppedProcess_of_mem_finset

∀ {Ω : 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],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.Integrable (u n) μ) →
      ∀ (n : ι) {s : Finset ι},
        (∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s) →
          MeasureTheory.Integrable (MeasureTheory.stoppedProcess u τ n) μ

Defined in

Mathlib.Probability.Process.Stopping

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonemptyLinearOrderTopologicalSpaceOrderTopologyFirstCountableTopologyNormedAddCommGroup