Documentation

BGW.Skorokhod.AldousCriterionOptional

Optional times and strict upward discretization #

The convention for optional times here is measurability of {σ < t} at time t. Strict upward rounding is necessary: ordinary ceiling rounding fixes grid points and can retain a failure of measurability of {σ ≤ t}.

source
def BGW.Skorokhod.IsOptionalTime {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m) (σ : Ω → ↑(Set.Icc 0 T)) :
Prop

An optional time in the strict sublevel-set convention, without regularity of the filtration.

Reference: Billingsley 1999, Section 16.

Equations
Instances For
    source
    theorem BGW.Skorokhod.IsOptionalTime.measurable {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m} {σ : Ω → ↑(Set.Icc 0 T)} (hσ : IsOptionalTime 𝓕 σ) :
    Measurable σ

    An optional time is measurable for the ambient σ-algebra.

    Reference: Billingsley 1999, Section 16.

    source
    noncomputable def BGW.Skorokhod.aldousRoundTime {T : ℝ} (hT : 0 ≤ T) (j : ℕ) (t : ↑(Set.Icc 0 T)) :
    ↑(Set.Icc 0 T)

    Strict upward dyadic rounding, capped at the horizon.

    Reference: Billingsley 1999, Section 16.

    Equations
    Instances For
      source
      theorem BGW.Skorokhod.le_aldousRoundTime {T : ℝ} (hT : 0 ≤ T) (j : ℕ) (t : ↑(Set.Icc 0 T)) :
      t ≤ aldousRoundTime hT j t

      Strict upward rounding never moves a time backwards.

      Reference: Billingsley 1999, Section 16.

      source
      theorem BGW.Skorokhod.IsOptionalTime.isStopTime_aldousRoundTime {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m} {σ : Ω → ↑(Set.Icc 0 T)} (hσ : IsOptionalTime 𝓕 σ) (hT : 0 ≤ T) (j : ℕ) :
      IsStopTime 𝓕 fun (ω : Ω) => aldousRoundTime hT j (σ ω)

      Rounding an optional time strictly upwards gives a stopping time.

      Reference: Billingsley 1999, Section 16.

      source
      theorem BGW.Skorokhod.tendsto_aldousRoundTime {T : ℝ} (hT : 0 ≤ T) (t : ↑(Set.Icc 0 T)) :
      Filter.Tendsto (fun (j : ℕ) => aldousRoundTime hT j t) Filter.atTop (nhds t)

      Strict upward dyadic rounding converges to the original time.

      Reference: Billingsley 1999, Section 16.

      source
      theorem BGW.Skorokhod.tendsto_eval_aldousRoundTime {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) (t : ↑(Set.Icc 0 T)) :
      Filter.Tendsto (fun (j : ℕ) => f (aldousRoundTime hT j t)) Filter.atTop (nhds (f t))

      Evaluation along rounded times converges by right continuity, including at the horizon.

      Reference: Billingsley 1999, Section 16.