measurableSet_ge_of_countable_range

English

Let τ be a stopping time with respect to a filtration f. For every index i in the index set, the event {ω ∈ Ω : i ≤ τ(ω)} is measurable with respect to the σ-algebra F_i.

Русский

Пусть τ является остановочным временем относительно фильтрации f. Для каждого индекса i из множества индексов множество {ω ∈ Ω : i ≤ τ(ω)} измеримо относительно σ‑алгебры F_i.

LaTeX

$$$\forall i, \{\omega \in \Omega \mid i \le \tau(\omega)\} \in \mathcal{F}_i$$$

Lean4

protected theorem measurableSet_ge_of_countable_range {ι} [LinearOrder ι] {τ : Ω → ι} {f : Filtration ι m}
    (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable) (i : ι) : MeasurableSet[f i] {ω | i ≤ τ ω} :=
  by
  have : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ := by ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]
  rw [this]
  exact (hτ.measurableSet_lt_of_countable_range h_countable i).compl

Похожие утверждения