English
The associated sigma-algebra of a stopping time τ is defined by s ∈ Ω is measurable if for every i, s ∩ {τ ≤ i} ∈ F_i.
Русский
Связанная сигма‑алгебра остановочного времени τ задаётся так: множество s ⊆ Ω измеримо, если для каждого i выполняется s ∩ {τ ≤ i} ∈ F_i.
LaTeX
$$$\text{MeasurableSpace}_{τ}(s) \iff \forall i,\ s \cap \{\omega: τ(\omega) \le i\} \in \mathcal{F}_i$$$
Lean4
/-- The associated σ-algebra with a stopping time. -/
protected def measurableSpace (hτ : IsStoppingTime f τ) : MeasurableSpace Ω
where
MeasurableSet' s := ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i})
measurableSet_empty i := (Set.empty_inter {ω | τ ω ≤ i}).symm ▸ @MeasurableSet.empty _ (f i)
measurableSet_compl s hs
i := by
rw [(_ : sᶜ ∩ {ω | τ ω ≤ i} = (sᶜ ∪ {ω | τ ω ≤ i}ᶜ) ∩ {ω | τ ω ≤ i})]
· refine MeasurableSet.inter ?_ ?_
· rw [← Set.compl_inter]
exact (hs i).compl
· exact hτ i
· rw [Set.union_inter_distrib_right]
simp only [Set.compl_inter_self, Set.union_empty]
measurableSet_iUnion s hs
i := by
rw [forall_swap] at hs
rw [Set.iUnion_inter]
exact MeasurableSet.iUnion (hs i)
