English
If τ is a stopping time, the process i ↦ min(i, τ(ω)) is progressively measurable with respect to the filtration f.
Русский
Если τ — время останова, тогда процесс i ↦ min(i, τ(ω)) является прогрессивно измеримым относительно фильтрации f.
LaTeX
$$$\text{ProgMeasurable}_{f}(\,\min(i, \tau(\omega))\,)$$$
Lean4
theorem progMeasurable_min_stopping_time [PseudoMetrizableSpace ι] (hτ : IsStoppingTime f τ) :
ProgMeasurable f fun i ω => min i (τ ω) := by
intro i
let m_prod : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (f i)
let m_set : ∀ t : Set (Set.Iic i × Ω), MeasurableSpace t := fun _ =>
@Subtype.instMeasurableSpace (Set.Iic i × Ω) _ m_prod
let s := {p : Set.Iic i × Ω | τ p.2 ≤ i}
have hs : MeasurableSet[m_prod] s := @measurable_snd (Set.Iic i) Ω _ (f i) _ (hτ i)
have h_meas_fst : ∀ t : Set (Set.Iic i × Ω), Measurable[m_set t] fun x : t => ((x : Set.Iic i × Ω).fst : ι) :=
fun t => (@measurable_subtype_coe (Set.Iic i × Ω) m_prod _).fst.subtype_val
apply Measurable.stronglyMeasurable
refine measurable_of_restrict_of_restrict_compl hs ?_ ?_
· refine @Measurable.min _ _ _ _ _ (m_set s) _ _ _ _ _ (h_meas_fst s) ?_
refine @measurable_of_Iic ι s _ _ _ (m_set s) _ _ _ _ fun j => ?_
have h_set_eq :
(fun x : s => τ (x : Set.Iic i × Ω).snd) ⁻¹' Set.Iic j =
(fun x : s => (x : Set.Iic i × Ω).snd) ⁻¹' {ω | τ ω ≤ min i j} :=
by
ext1 ω
simp only [Set.mem_preimage, Set.mem_Iic, iff_and_self, le_min_iff, Set.mem_setOf_eq]
exact fun _ => ω.prop
rw [h_set_eq]
suffices h_meas : @Measurable _ _ (m_set s) (f i) fun x : s ↦ (x : Set.Iic i × Ω).snd from
h_meas (f.mono (min_le_left _ _) _ (hτ.measurableSet_le (min i j)))
exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _)
· letI sc := sᶜ
suffices h_min_eq_left :
(fun x : sc => min (↑(x : Set.Iic i × Ω).fst) (τ (x : Set.Iic i × Ω).snd)) = fun x : sc =>
↑(x : Set.Iic i × Ω).fst
by
simp +unfoldPartialApp only [sc, Set.restrict, h_min_eq_left]
exact h_meas_fst _
ext1 ω
rw [min_eq_left]
have hx_fst_le : ↑(ω : Set.Iic i × Ω).fst ≤ i := (ω : Set.Iic i × Ω).fst.prop
refine hx_fst_le.trans (le_of_lt ?_)
convert ω.prop
simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_setOf_eq]
