English
If τ and η are stopping times bounded below, i ≤ τ and i ≤ η for all outcomes, and s is measurable, then the piecewise set s.piecewise τ η is again a stopping time for the same filtration.
Русский
Если τ и η — времена остановки, ограничены снизу, и для всех исходов i ≤ τ и i ≤ η, и если s измеримо, то s.piecewise τ η является временем остановки той же фильтрации.
LaTeX
$$$\text{IsStoppingTime } 𝒢\ (s.\text{piecewise } τ\ η) $ при допущениях: $hτ_{st} : IsStoppingTime 𝒢 τ$, $hη_{st} : IsStoppingTime 𝒢 η$, $\forall ω, i ≤ τ ω$, $\forall ω, i ≤ η ω$, и $hs : \text{MeasurableSet}[𝒢 i] s$.$$
Lean4
theorem isStoppingTime_piecewise_const (hij : i ≤ j) (hs : MeasurableSet[𝒢 i] s) :
IsStoppingTime 𝒢 (s.piecewise (fun _ => i) fun _ => j) :=
(isStoppingTime_const 𝒢 i).piecewise_of_le (isStoppingTime_const 𝒢 j) (fun _ => le_rfl) (fun _ => hij) hs
