theorem coe_untopA_eq (a : ℕ∞) (ha : a ≠ ⊤) : ↑(WithTop.untopA a) = a

Helper lemma: for any extended natural a : ℕ∞ that is not ⊤, coercing a.untopA : ℕ back into ℕ∞ recovers a.

noncomputable def stoppedValueExtended {Ω : Type u_1} [MeasurableSpace Ω] (f : ℕ → Ω → ℝ) (τ : Ω → ℕ∞) : Ω → ℝ

The stopped value of a process f : ℕ → Ω → ℝ at a stopping time τ : Ω → ℕ∞ that may take the value ⊤ (infinity). When τ ω = ⊤, the value is the limit lim_{n → ∞} f n ω; otherwise it is f (τ ω) ω. This extends stoppedValue to allow infinite stopping times, as required for the general optional stopping theorem.

theorem general_optional_stopping_bounded {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : ℕ → Ω → ℝ} {L M : Ω → ℕ∞} (hsub : MeasureTheory.Submartingale f ℱ μ) (hL : MeasureTheory.IsStoppingTime ℱ L) (hM : MeasureTheory.IsStoppingTime ℱ M) (hLM : L ≤ M) {N : ℕ} (hbdd : ∀ (ω : Ω), M ω ≤ ↑N) [MeasureTheory.SigmaFinite (μ.trim ⋯)] : ∫ (ω : Ω), MeasureTheory.stoppedValue f L ω ∂μ ≤ ∫ (ω : Ω), MeasureTheory.stoppedValue f M ω ∂μ ∧ MeasureTheory.stoppedValue f L ≤ᵐ[μ] μ[MeasureTheory.stoppedValue f M | hL.measurableSpace]

Bounded general optional stopping theorem. If f is a submartingale, L ≤ M are stopping times with M bounded above by a finite N, then E[f_L] ≤ E[f_M] and f_L ≤ E[f_M | ℱ_L] almost surely. This is the bounded-stopping-time form that underpins the general optional stopping theorem.

theorem general_optional_stopping {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : ℕ → Ω → ℝ} (hsub : MeasureTheory.Submartingale f ℱ μ) (hui : MeasureTheory.UniformIntegrable f 1 μ) (τ : Ω → ℕ∞) (hτ : MeasureTheory.IsStoppingTime ℱ τ) : ∫ (ω : Ω), f 0 ω ∂μ ≤ ∫ (ω : Ω), stoppedValueExtended f τ ω ∂μ ∧ ∫ (ω : Ω), stoppedValueExtended f τ ω ∂μ ≤ ∫ (ω : Ω), Filter.atTop.limUnder fun (n : ℕ) => f n ω ∂μ

General optional stopping theorem (expectation inequality form). Let f be a uniformly integrable submartingale and τ : Ω → ℕ∞ any stopping time (possibly infinite). Then E[f_0] ≤ E[f_τ] ≤ E[f_∞], where f_∞ = lim_{n → ∞} f n and f_τ is given by stoppedValueExtended. This corresponds to the textbook statement "Let X_n be a uniformly integrable submartingale; for any stopping time N ≤ ∞ we have EX_0 ≤ EX_N ≤ EX_∞."