theorem
uniformIntegrable_stopped_second_term
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ}
{N : Ω → ℕ}
(hf : MeasureTheory.Submartingale f 𝒢 μ)
(hUI : MeasureTheory.UniformIntegrable f 1 μ)
(hN : MeasureTheory.IsStoppingTime 𝒢 fun (ω : Ω) => ↑(N ω))
:
Helper lemma: if f is a uniformly integrable submartingale adapted to 𝒢 and N is a
stopping time, then the sequence n ↦ f_N · 1_{N ≤ n} (the contribution to the stopped process
from indices that have already been stopped) is uniformly integrable in L¹.
theorem
optional_stopping_alt_ui_preserved
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
{f : ℕ → Ω → ℝ}
{N : Ω → ℕ}
(hf : MeasureTheory.Submartingale f 𝒢 μ)
(hUI : MeasureTheory.UniformIntegrable f 1 μ)
(hN : MeasureTheory.IsStoppingTime 𝒢 fun (ω : Ω) => ↑(N ω))
:
MeasureTheory.UniformIntegrable (fun (n : ℕ) (ω : Ω) => f (min (N ω) n) ω) 1 μ
General optional stopping preservation of uniform integrability: if f is a uniformly
integrable submartingale adapted to 𝒢 and N is a stopping time, then the stopped process
n ↦ f_{min(N, n)} is also uniformly integrable. This is the key ingredient for the general
optional stopping theorem (Lecture 29).