Theorems · Inductive type · probability

ProbabilityTheory.IsLocalizingSequence

{ι : Type u_1} →
  {Ω : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        [inst_1 : TopologicalSpace ι] →
          [OrderTopology ι] →
            MeasureTheory.Filtration ι mΩ →
              (ℕ → Ω → WithTop ι) →
                autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsLocalizingSequence._auto_1 → Prop

A localizing sequence is a sequence of stopping times that is almost surely increasing and tends almost surely to infinity.

Defined in

Mathlib.Probability.Process.LocalProperty

Cited by

9 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

PreorderTopologicalSpaceOrderTopology