theorem optional_stopping_uniformly_integrable {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} {M : ℕ → Ω → ℝ} {τ : Ω → ℕ} (hmart : MeasureTheory.Submartingale M ℱ μ) (hui : MeasureTheory.UniformIntegrable M 1 μ) (hτ : MeasureTheory.IsStoppingTime ℱ fun (ω : Ω) => ↑(τ ω)) : MeasureTheory.UniformIntegrable (fun (n : ℕ) (ω : Ω) => M (min (τ ω) n) ω) 1 μ

General optional stopping theorem (uniform integrability preservation) (Lecture 29): let M be a uniformly integrable submartingale with respect to a filtration ℱ and let τ be a stopping time. Then the stopped process n ↦ M_{min(τ, n)} is uniformly integrable. Thin wrapper around optional_stopping_alt_ui_preserved.