English
Assume ι is countable. If τ and π are stopping times, then the set {ω : τ(ω) = π(ω)} is measurable with respect to the stopping-time σ-algebra.
Русский
Пусть ι счётно. Если τ и π — времена останова, тогда множество {ω : τ(ω) = π(ω)} измеримо относительно σ-алгебры времени останова.
LaTeX
$$$\{\omega : \tau(\omega) = \pi(\omega)\} \in \mathcal{F}_{\tau}$ (countable setting)$$
Lean4
theorem measurableSet_eq_stopping_time_of_countable [Countable ι] [TopologicalSpace ι] [MeasurableSpace ι]
[BorelSpace ι] [OrderTopology ι] [MeasurableSingletonClass ι] [SecondCountableTopology ι] (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_of_countable
· exact (hτ.min_const j).measurable_of_le fun _ => min_le_right _ _
· exact (hπ.min_const j).measurable_of_le fun _ => min_le_right _ _
