English
If f is a filtration and τ is a stopping time, then the stoppedValue u τ is measurable with respect to the stopping-time σ-algebra.
Русский
Если f — фильтрация, а τ — время останова, то stoppedValue u τ измеримо относительно σ-алгебры времени останова.
LaTeX
$$$\text{Measurable}_{\mathcal{F}_{\tau}}(\text{stoppedValue}(u, \tau))$$$
Lean4
theorem measurable_stoppedValue [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β]
(hf_prog : ProgMeasurable f u) (hτ : IsStoppingTime f τ) : Measurable[hτ.measurableSpace] (stoppedValue u τ) :=
by
have h_str_meas : ∀ i, StronglyMeasurable[f i] (stoppedValue u fun ω => min (τ ω) i) := fun i =>
stronglyMeasurable_stoppedValue_of_le hf_prog (hτ.min_const i) fun _ => min_le_right _ _
intro t ht i
suffices stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ i} = (stoppedValue u fun ω => min (τ ω) i) ⁻¹' t ∩ {ω : Ω | τ ω ≤ i}
by rw [this]; exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)
ext1 ω
simp only [stoppedValue, Set.mem_inter_iff, Set.mem_preimage, Set.mem_setOf_eq, and_congr_left_iff]
intro h
rw [min_eq_left h]
