English
The stopping-time sigma-algebra generated by the minimum of two stopping times equals the infimum of their sigma-algebras.
Русский
Сигма-алгебра останова, порожденная минимумом двух времен останова, равна их инфиминному пересечению сигма-алгебр.
LaTeX
$$$(h_τ.min h_π).\text{measurableSpace} = h_τ.measurableSpace \sqcap h_π.measurableSpace$$$
Lean4
theorem measurableSpace_min (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) :
(hτ.min hπ).measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace :=
by
refine le_antisymm ?_ ?_
·
exact
le_inf (measurableSpace_mono _ hτ fun _ => min_le_left _ _) (measurableSpace_mono _ hπ fun _ => min_le_right _ _)
· intro s
change
MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[hπ.measurableSpace] s →
MeasurableSet[(hτ.min hπ).measurableSpace] s
simp_rw [IsStoppingTime.measurableSet]
have : ∀ i, {ω | min (τ ω) (π ω) ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i} := by intro i; ext1 ω; simp
simp_rw [this, Set.inter_union_distrib_left]
exact fun h i => (h.left i).union (h.right i)
