English
Let f be a filtration on Ω. If τ and π are stopping times with respect to f, then the event {ω ∈ Ω : τ(ω) ≤ π(ω)} is measurable with respect to the stopping-time σ-algebra generated by τ.
Русский
Пусть f — фильтрация на Ω. Пусть τ и π являются временами останова относительно f. Тогда событие {ω ∈ Ω : τ(ω) ≤ π(ω)} измеримо относительно σ-алгебры, порождённой временем останова τ.
LaTeX
$$$\{\omega \in \Omega : \tau(\omega) \le \pi(\omega)\} \in \mathcal{F}_{\tau}$$$
Lean4
theorem measurableSet_le_stopping_time [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι]
[MeasurableSpace ι] [BorelSpace ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
MeasurableSet[hτ.measurableSpace] {ω | τ ω ≤ π ω} :=
by
rw [hτ.measurableSet]
intro j
have : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j} :=
by
ext1 ω
simp only [Set.mem_inter_iff, Set.mem_setOf_eq, min_le_iff, le_min_iff, le_refl, and_congr_left_iff]
intro h
simp only [h, or_self_iff, and_true]
rw [Iff.comm, or_iff_left_iff_imp]
exact h.trans
rw [this]
refine MeasurableSet.inter ?_ (hτ.measurableSet_le j)
apply @measurableSet_le _ _ _ _ _ (Filtration.seq f j) _ _ _ _ _ ?_ ?_
· exact (hτ.min_const j).measurable_of_le fun _ => min_le_right _ _
· exact (hπ.min_const j).measurable_of_le fun _ => min_le_right _ _
