English
For any n, the stopped process can be written as the indicator of {τ ≥ n} at n plus the sum over i < n of indicators for τ = i at i.
Русский
Для любого n останленный процесс может быть записан через индикацию {τ≥n} при n и сумму индикаторов τ=i при i<n.
LaTeX
$$$\text{stoppedProcess } u\ τ\ n = 1_{\{a\mid n ≤ τ a\}}(a) \cdot u(n) + \sum_{i< n} 1_{\{a\mid τ a = i\}}(a) \cdot u(i)$$$
Lean4
theorem condExp_min_stopping_time_ae_eq_restrict_le [MeasurableSpace ι] [SecondCountableTopology ι] [BorelSpace ι]
(hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) [SigmaFinite (μ.trim (hτ.min hσ).measurableSpace_le)] :
μ[f|(hτ.min hσ).measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[f|hτ.measurableSpace] :=
by
have : SigmaFinite (μ.trim hτ.measurableSpace_le) :=
haveI h_le : (hτ.min hσ).measurableSpace ≤ hτ.measurableSpace :=
by
rw [IsStoppingTime.measurableSpace_min]
· exact inf_le_left
· simp_all only
sigmaFiniteTrim_mono _ h_le
refine
(condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (hτ.min hσ).measurableSpace_le
(hτ.measurableSet_le_stopping_time hσ) fun t => ?_).symm
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_le_iff]; simp_all only
