Theorems · Definition · probability

ProbabilityTheory.Locally

{ι : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        [inst : LinearOrder ι] →
          [OrderBot ι] →
            [inst_2 : TopologicalSpace ι] →
              [OrderTopology ι] →
                [Zero E] →
                  ((ι → Ω → E) → Prop) →
                    MeasureTheory.Filtration ι mΩ →
                      (ι → Ω → E) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.Locally._auto_1 → Prop

A stochastic process X is said to satisfy a property p locally with respect to a filtration 𝓕 if there exists a localizing sequence (τ_n) such that for all n, the stopped process fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i) satisfies p.

Defined in

Mathlib.Probability.Process.LocalProperty

Cited by

15 results in Mathlib

Foundations

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

Assumes

LinearOrderOrderBotTopologicalSpaceOrderTopologyZero