English
If s is measurable in both stopping-time sigmas, then s ∩ {ω : τ(ω) ≤ π(ω)} is measurable in the minimum sigma-algebra.
Русский
Если s измеримо в обеих сигма-алгебрах останова, то s ∩ {τ ≤ π} измеримо в минимальном пространстве.
LaTeX
$$$\text{Measurable}(s) \text{ in } h_τ.measurableSpace \land h_π.measurableSpace \Rightarrow \text{Measurable}(s ∩ \{ω: τω ≤ σω\})$$$
Lean4
theorem measurableSet_inter_le [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace ι]
[BorelSpace ι] (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (s : Set Ω)
(hs : MeasurableSet[hτ.measurableSpace] s) : MeasurableSet[(hτ.min hπ).measurableSpace] (s ∩ {ω | τ ω ≤ π ω}) :=
by
simp_rw [IsStoppingTime.measurableSet] at hs ⊢
intro i
have :
s ∩ {ω | τ ω ≤ π ω} ∩ {ω | min (τ ω) (π ω) ≤ i} =
s ∩ {ω | τ ω ≤ i} ∩ {ω | min (τ ω) (π ω) ≤ i} ∩ {ω | min (τ ω) i ≤ min (min (τ ω) (π ω)) i} :=
by
ext1 ω
simp only [min_le_iff, Set.mem_inter_iff, Set.mem_setOf_eq, le_min_iff, le_refl, true_and, true_or]
by_cases hτi : τ ω ≤ i
· simp only [hτi, true_or, and_true, and_congr_right_iff]
intro
constructor <;> intro h
· exact Or.inl h
· rcases h with h | h
· exact h
· exact hτi.trans h
simp only [hτi, false_or, and_false, false_and, iff_false, not_and, not_le, and_imp]
refine fun _ hτ_le_π => lt_of_lt_of_le ?_ hτ_le_π
rw [← not_le]
exact hτi
rw [this]
refine ((hs i).inter ((hτ.min hπ) i)).inter ?_
apply @measurableSet_le _ _ _ _ _ (Filtration.seq f i) _ _ _ _ _ ?_ ?_
· exact (hτ.min_const i).measurable_of_le fun _ => min_le_right _ _
· exact ((hτ.min hπ).min_const i).measurable_of_le fun _ => min_le_right _ _
