theorem submartingale_integral_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} {X : ℕ → Ω → ℝ} (hsub : MeasureTheory.Submartingale X ℱ μ) {i j : ℕ} (hij : i ≤ j) : ∫ (ω : Ω), X i ω ∂μ ≤ ∫ (ω : Ω), X j ω ∂μ

Monotonicity of expectations along a submartingale: if X is a submartingale and i ≤ j, then ∫ X_i dμ ≤ ∫ X_j dμ.

theorem submartingale_integral_norm_le {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} {X : ℕ → Ω → ℝ} {C : ℝ} (hsub : MeasureTheory.Submartingale X ℱ μ) (hbdd : ∀ (n : ℕ), ∫ (ω : Ω), (X n ω)⁺ ∂μ ≤ C) (n : ℕ) : ∫ (ω : Ω), ‖X n ω‖ ∂μ ≤ 2 * C - ∫ (ω : Ω), X 0 ω ∂μ

L¹-bound for a submartingale X from a uniform bound on the positive parts: if ∫ (X n)⁺ dμ ≤ C for every n, then ∫ ‖X n‖ dμ ≤ 2C - ∫ X 0 dμ. This uses the identity ‖x‖ = 2 x⁺ - x together with monotonicity of ∫ X n dμ.

theorem submartingale_ae_convergence {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} {X : ℕ → Ω → ℝ} {C : ℝ} (hsub : MeasureTheory.Submartingale X ℱ μ) (hbdd : ∀ (n : ℕ), ∫ (ω : Ω), (X n ω)⁺ ∂μ ≤ C) : ∃ (X_inf : Ω → ℝ), MeasureTheory.Integrable X_inf μ ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => X n ω) Filter.atTop (nhds (X_inf ω))

Submartingale almost-sure convergence theorem. If X is a submartingale on a probability space with ∫ (X n)⁺ dμ uniformly bounded by some C, then there exists an integrable limit X_∞ such that X n → X_∞ almost surely.