English
Under tau ≤ pi and bounded above by N, the stopped-value difference can be written with indicator sets splitting by τ and π in a finite range.
Русский
При τ ≤ π и ограниченности сверху на N, разность stoppedValue может быть записана через конечные индикаторные множества и разности u(i+1)−u(i).
LaTeX
$$$\text{stoppedValue } u\ π - \text{stoppedValue } u\ τ = \omega \mapsto \sum_{i=0}^{N} \mathbf{1}_{\{ω\mid τ(ω) ≤ i ∧ i < π(ω)\}}(ω)\ (u(i+1,ω) - u(i,ω))$$$
Lean4
theorem condExp_min_stopping_time_ae_eq_restrict_le_const (hτ : IsStoppingTime ℱ τ) (i : ι)
[SigmaFinite (μ.trim (hτ.min_const i).measurableSpace_le)] :
μ[f|(hτ.min_const i).measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ i}] μ[f|hτ.measurableSpace] :=
by
have : SigmaFinite (μ.trim hτ.measurableSpace_le) :=
haveI h_le : (hτ.min_const i).measurableSpace ≤ hτ.measurableSpace :=
by
rw [IsStoppingTime.measurableSpace_min_const]
exact inf_le_left
sigmaFiniteTrim_mono _ h_le
refine
(condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (hτ.min_const i).measurableSpace_le
(hτ.measurableSet_le' i) fun t => ?_).symm
rw [Set.inter_comm _ t, hτ.measurableSet_inter_le_const_iff]
