English
The stopped process of a submartingale with respect to a stopping time is itself a submartingale.
Русский
Остановленный процесс субмартингала относительно останова сам является субмартингалом.
LaTeX
$$$ \\text{stoppedProcess}(f,\\tau) \\; \\text{is a Submartingale under } \\mathcal{G}, \\mu$$$
Lean4
/-- The stopped process of a submartingale with respect to a stopping time is a submartingale. -/
protected theorem stoppedProcess [IsFiniteMeasure μ] (h : Submartingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ) :
Submartingale (stoppedProcess f τ) 𝒢 μ :=
by
rw [submartingale_iff_expected_stoppedValue_mono]
· intro σ π hσ hπ hσ_le_π hπ_bdd
simp_rw [stoppedValue_stoppedProcess]
obtain ⟨n, hπ_le_n⟩ := hπ_bdd
exact
h.expected_stoppedValue_mono (hσ.min hτ) (hπ.min hτ) (fun ω => min_le_min (hσ_le_π ω) le_rfl) fun ω =>
(min_le_left _ _).trans (hπ_le_n ω)
· exact Adapted.stoppedProcess_of_discrete h.adapted hτ
· exact fun i => h.integrable_stoppedValue ((isStoppingTime_const _ i).min hτ) fun ω => min_le_left _ _
