Theorems · Theorem · probability

MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime

∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [WellFoundedLT ι] [Countable ι] [inst_3 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
  [inst_6 : MeasurableSpace β] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ →
    ∀ {N : ι},
      (∀ (x : Ω), τ x ≤ ↑N) →
        ∀ {s : Set β},
          MeasurableSet s →
            MeasureTheory.Adapted f u →
              MeasureTheory.IsStoppingTime f fun x => ↑(MeasureTheory.hittingBtwn u s (τ x).untopA N x)

The hitting time of a discrete process with the starting time indexed by a stopping time is a stopping time.

Defined in

Mathlib.Probability.Process.HittingTime

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderWellFoundedLTCountableTopologicalSpaceOrderTopologyFirstCountableTopologyMeasurableSpace