English
If τ and π are stopping times, the set {ω : τ(ω) = π(ω)} is measurable with respect to the stopping-time σ-algebra generated by τ (under suitable regularity assumptions).
Русский
Если τ и π — времена останова, множество {ω : τ(ω) = π(ω)} измеримо относительно остановочнои σ-алгебры, порождённой τ (при некоторых регулярностях).
LaTeX
$$$\{\omega : \tau(\omega) = \pi(\omega)\} \in \mathcal{F}_{\tau}$$$
Lean4
theorem measurableSet_eq_stopping_time [AddGroup ι] [TopologicalSpace ι] [MeasurableSpace ι] [BorelSpace ι]
[OrderTopology ι] [MeasurableSingletonClass ι] [SecondCountableTopology ι] [MeasurableSub₂ ι]
(hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) : MeasurableSet[hτ.measurableSpace] {ω | τ ω = π ω} :=
by
rw [hτ.measurableSet]
intro j
have : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j} :=
by
ext1 ω
simp only [Set.mem_inter_iff, Set.mem_setOf_eq]
refine ⟨fun h => ⟨⟨?_, h.2⟩, ?_⟩, fun h => ⟨?_, h.1.2⟩⟩
· rw [h.1]
· rw [← h.1]; exact h.2
· obtain ⟨h', hσ_le⟩ := h
obtain ⟨h_eq, hτ_le⟩ := h'
rwa [min_eq_left hτ_le, min_eq_left hσ_le] at h_eq
rw [this]
refine MeasurableSet.inter (MeasurableSet.inter ?_ (hτ.measurableSet_le j)) (hπ.measurableSet_le j)
apply measurableSet_eq_fun
· exact (hτ.min_const j).measurable_of_le fun _ => min_le_right _ _
· exact (hπ.min_const j).measurable_of_le fun _ => min_le_right _ _
