diff --git a/LMLExplore/EValues/TestSupermartingale.lean b/LMLExplore/EValues/TestSupermartingale.lean
index be665cdc..efffa547 100644
--- a/LMLExplore/EValues/TestSupermartingale.lean
+++ b/LMLExplore/EValues/TestSupermartingale.lean
@@ -202,6 +202,11 @@ theorem congr (hM : IsTestSupermartingale M ℱ S) (hM' : Adapted ℱ M')
   ⟨hM.toIsENNSupermartingale.congr hM' h, fun P hP ↦
     (lintegral_congr_ae (h P hP 0)).symm.trans_le (hM.lintegral_zero_le P hP)⟩
 
+/-- A test supermartingale has finite initial expectation under every member of the null. -/
+theorem lintegral_zero_ne_top (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) :
+    ∫⁻ ω, M 0 ω ∂P ≠ ∞ :=
+  ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne
+
 /-- Every value of a test supermartingale has expectation at most `1`. -/
 theorem lintegral_le_one (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) (n : ℕ) :
     ∫⁻ ω, M n ω ∂P ≤ 1 :=
@@ -217,14 +222,14 @@ theorem isEVar (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hM : IsTestSupermarti
 theorem ae_lt_top (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) :
     ∀ᵐ ω ∂P, ∀ n, M n ω < ∞ :=
   hM.toIsENNSupermartingale.ae_lt_top hP
-    ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne
+    (hM.lintegral_zero_ne_top hP)
 
 /-- The real values of a test supermartingale form a real supermartingale under every finite
 member of the null. -/
 theorem supermartingale_toReal (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S)
     [IsFiniteMeasure P] : Supermartingale (fun n ω ↦ (M n ω).toReal) ℱ P :=
   hM.toIsENNSupermartingale.supermartingale_toReal hP
-    ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne
+    (hM.lintegral_zero_ne_top hP)
 
 end IsTestSupermartingale
 
@@ -459,7 +464,7 @@ theorem IsTestSupermartingale.ae_eq_mul_prod_div (hM : IsTestSupermartingale M 
     (hP : P ∈ S) :
     ∀ᵐ ω ∂P, ∀ n, M n ω = M 0 ω * ∏ k ∈ range n, M (k + 1) ω / M k ω :=
   hM.toIsENNSupermartingale.ae_eq_mul_prod_div hP
-    ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne
+    (hM.lintegral_zero_ne_top hP)
 
 /-! ### Pulling a known factor out of a supermartingale step -/
 
diff --git a/LMLExplore/Probability/Martingale/OptionalStopping.lean b/LMLExplore/Probability/Martingale/OptionalStopping.lean
new file mode 100644
index 00000000..91fe436a
--- /dev/null
+++ b/LMLExplore/Probability/Martingale/OptionalStopping.lean
@@ -0,0 +1,321 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import LMLExplore.EValues.TestSupermartingale
+public import LMLExplore.Probability.Process.Stopping
+public import LMLExplore.Probability.Process.StoppedValue
+public import Mathlib.Probability.Martingale.Convergence
+
+/-!
+# Convergence and optional stopping of `ℝ≥0∞`-valued supermartingales
+
+An `ℝ≥0∞`-valued supermartingale (`ProbabilityTheory.IsENNSupermartingale`) with finite initial
+expectation under a finite measure converges almost surely, to a limit that is almost surely
+finite and whose set integrals are bounded by those of the process. Optional stopping then holds
+at every pair of stopping times `σ ≤ τ` with values in `WithTop ℕ`, unbounded and possibly infinite:
+the value of the process at a random time is `MeasureTheory.stoppedValueLimsup`, its `limsup` where
+the time is infinite, and
+`∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P` for every set `s`
+measurable for the σ-algebra at `σ` [RW, Fact 7.5; ShSVV11]. For a test supermartingale for a null
+of probability measures, the value at every stopping time is therefore an e-variable; this is the
+validity of test supermartingales at stopping times on which e-processes and anytime-valid tests
+rest.
+
+For stopping times bounded by a constant, optional stopping needs neither the finiteness of the
+initial expectation nor the convergence of the process, and holds for every `ℝ≥0∞`-valued
+supermartingale. Mathlib's `MeasureTheory.Submartingale.expected_stoppedValue_mono` is the real
+version for bounded stopping times, under integrability. Convergence is derived from Mathlib's
+`MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd` through the real values of the process.
+
+## Main statements
+
+* `ProbabilityTheory.IsENNSupermartingale.ae_tendsto_limsup`,
+  `ProbabilityTheory.IsENNSupermartingale.ae_limsup_lt_top`: almost sure convergence, to an almost
+  surely finite limit.
+* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_limsup_le`: the set integrals of the limit
+  over `ℱ n`-measurable sets are at most those of `M n`.
+* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_stoppedValueLimsup_le_of_le_const`: optional
+  stopping for bounded stopping times, for every `ℝ≥0∞`-valued supermartingale.
+* `ProbabilityTheory.IsENNSupermartingale.setLIntegral_stoppedValueLimsup_le`: optional stopping for
+  arbitrary stopping times with values in `WithTop ℕ`.
+* `ProbabilityTheory.IsTestSupermartingale.lintegral_limsup_le_one`: the almost sure limit of a
+  test supermartingale has expectation at most `1`.
+* `ProbabilityTheory.IsTestSupermartingale.lintegral_stoppedValueLimsup_le_one`,
+  `ProbabilityTheory.IsTestSupermartingale.isEVar_stoppedValueLimsup`: a test supermartingale has
+  expectation at most `1` at every stopping time, where its value is an e-variable.
+
+## References
+
+* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in
+  Statistics 1 (2025), arXiv:2410.23614.
+* [ShSVV11] G. Shafer, A. Shen, N. Vereshchagin and V. Vovk, *Test martingales, Bayes factors and
+  p-values*, Statist. Sci. 26 (2011), arXiv:0912.4269.
+-/
+
+public section
+
+open MeasureTheory Filter Set Topology
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {ℱ : Filtration ℕ mΩ} {S : Set (Measure Ω)}
+  {P : Measure Ω} {M : ℕ → Ω → ℝ≥0∞} {σ τ : Ω → WithTop ℕ} {s : Set Ω}
+
+/-- The interpolating times `max a (min b k)` move from `k` to `k + 1` where `a ≤ k < b`. -/
+private lemma max_min_succ_of_le_of_lt {a b : WithTop ℕ} {k : ℕ} (ha : a ≤ k)
+    (hb : (k : WithTop ℕ) < b) :
+    max a (min b ↑(k + 1)) = ↑(k + 1) ∧ max a (min b k) = k := by
+  have hb' : ((k + 1 : ℕ) : WithTop ℕ) ≤ b := ENat.natCast_add_one_le_iff.2 hb
+  rw [min_eq_right hb', min_eq_right hb.le, max_eq_right (ha.trans (by simp)), max_eq_right ha]
+  exact ⟨rfl, rfl⟩
+
+/-- The interpolating times `max a (min b k)` do not move from `k` to `k + 1` outside
+`a ≤ k < b`. -/
+private lemma max_min_succ_eq {a b : WithTop ℕ} {k : ℕ} (h : ¬(a ≤ k ∧ (k : WithTop ℕ) < b)) :
+    max a (min b ↑(k + 1)) = max a (min b k) := by
+  rcases not_and_or.1 h with h | h
+  · rw [not_le] at h
+    have h' : ((k + 1 : ℕ) : WithTop ℕ) ≤ a := ENat.natCast_add_one_le_iff.2 h
+    rw [max_eq_left ((min_le_right _ _).trans h'), max_eq_left ((min_le_right _ _).trans h.le)]
+  · rw [not_lt] at h
+    rw [min_eq_left (h.trans (by simp)), min_eq_left h]
+
+namespace IsENNSupermartingale
+
+/-- An `ℝ≥0∞`-valued supermartingale with finite initial expectation under a finite measure
+converges almost surely to a finite limit. -/
+private theorem ae_exists_tendsto (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) :
+    ∀ᵐ ω ∂P, ∃ c < ∞, Tendsto (fun n ↦ M n ω) atTop (𝓝 c) := by
+  have hsub : Submartingale (fun n ω ↦ -(M n ω).toReal) ℱ P :=
+    (hM.supermartingale_toReal hP h0).neg
+  have hbdd : ⨆ n, eLpNorm (fun ω ↦ -(M n ω).toReal) 1 P < ∞ := by
+    refine (iSup_le fun n ↦ ?_).trans_lt h0.lt_top
+    rw [eLpNorm_one_eq_lintegral_eNorm (hsub.integrable n).aestronglyMeasurable]
+    refine (lintegral_mono fun ω ↦ ?_).trans (hM.lintegral_le hP n.zero_le)
+    rw [eNorm_neg, Real.eNorm_of_nonneg ENNReal.toReal_nonneg]
+    exact ENNReal.ofReal_toReal_le
+  filter_upwards [hsub.exists_ae_tendsto_of_bdd hbdd, hM.ae_lt_top hP h0] with ω ⟨c, hc⟩ hω
+  refine ⟨ENNReal.ofReal (-c), ENNReal.ofReal_lt_top, ?_⟩
+  refine ((ENNReal.continuous_ofReal.tendsto _).comp (by simpa using hc.neg)).congr fun n ↦ ?_
+  exact ENNReal.ofReal_toReal (hω n).ne
+
+/-- An `ℝ≥0∞`-valued supermartingale with finite initial expectation under a finite measure
+converges almost surely, so that its `limsup` is its limit [RW, Fact 7.5]. -/
+theorem ae_tendsto_limsup (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P]
+    (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) :
+    ∀ᵐ ω ∂P, Tendsto (fun n ↦ M n ω) atTop (𝓝 (limsup (fun n ↦ M n ω) atTop)) := by
+  filter_upwards [hM.ae_exists_tendsto hP h0] with ω ⟨c, _, hc⟩
+  rwa [hc.limsup_eq]
+
+/-- The almost sure limit of an `ℝ≥0∞`-valued supermartingale with finite initial expectation
+under a finite measure is almost surely finite. -/
+theorem ae_limsup_lt_top (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P]
+    (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) : ∀ᵐ ω ∂P, limsup (fun n ↦ M n ω) atTop < ∞ := by
+  filter_upwards [hM.ae_exists_tendsto hP h0] with ω ⟨c, hc_lt, hc⟩
+  rwa [hc.limsup_eq]
+
+/-- **Optional stopping for bounded stopping times.** For stopping times `σ ≤ τ ≤ N` and a set `s`
+measurable for the σ-algebra at `σ`, the set integral over `s` of an `ℝ≥0∞`-valued
+supermartingale at `τ` is at most its set integral at `σ`. No integrability is needed. -/
+theorem setLIntegral_stoppedValueLimsup_le_of_le_const (hM : IsENNSupermartingale M ℱ S)
+    (hP : P ∈ S) (hσ : IsStoppingTime ℱ σ) (hτ : IsStoppingTime ℱ τ) (hστ : σ ≤ τ) {N : ℕ}
+    (hτN : ∀ ω, τ ω ≤ N) (hs : MeasurableSet[hσ.measurableSpace] s) :
+    ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P := by
+  -- The times `max σ (min τ k)` run from `σ` at `k = 0` to `τ` at `k = N`, and move from `k` to
+  -- `k + 1` exactly on the `ℱ k`-measurable event `σ ≤ k < τ`.
+  set g : ℕ → Ω → ℝ≥0∞ := fun k ↦ stoppedValueLimsup M fun ω ↦ max (σ ω) (min (τ ω) k)
+  have hs' : MeasurableSet s := hσ.measurableSpace_le s hs
+  have hstep (k : ℕ) : ∫⁻ ω in s, g (k + 1) ω ∂P ≤ ∫⁻ ω in s, g k ω ∂P := by
+    set A := {ω | σ ω ≤ k} ∩ {ω | (k : WithTop ℕ) < τ ω}
+    have hAk : MeasurableSet[ℱ k] A :=
+      (hσ.measurableSet_le_natCast k).inter (hτ.measurableSet_natCast_lt k)
+    have hA : MeasurableSet A := ℱ.le k _ hAk
+    have hsA : MeasurableSet[ℱ k] (s ∩ A) := by
+      have hsk := ((hσ.measurableSet s).1 hs).2 k
+      rw [← Nat.cast_withTop] at hsk
+      rw [← inter_assoc]
+      exact hsk.inter (hτ.measurableSet_natCast_lt k)
+    have hg_succ : EqOn (g (k + 1)) (M (k + 1)) (s ∩ A) := fun ω hω ↦
+      stoppedValueLimsup_of_eq_natCast (max_min_succ_of_le_of_lt hω.2.1 hω.2.2).1
+    have hg : EqOn (g k) (M k) (s ∩ A) := fun ω hω ↦
+      stoppedValueLimsup_of_eq_natCast (max_min_succ_of_le_of_lt hω.2.1 hω.2.2).2
+    have hg_diff : EqOn (g (k + 1)) (g k) (s \ A) := fun ω hω ↦ by
+      exact stoppedValueLimsup_congr (max_min_succ_eq hω.2)
+    rw [← lintegral_inter_add_sdiff _ s hA, ← lintegral_inter_add_sdiff (g k) s hA,
+      setLIntegral_congr_fun (hs'.inter hA) hg_succ, setLIntegral_congr_fun (hs'.inter hA) hg,
+      setLIntegral_congr_fun (hs'.diff hA) hg_diff]
+    exact add_le_add_left (hM.setLIntegral_succ_le P hP k _ hsA) _
+  have hg0 : g 0 = stoppedValueLimsup M σ := by simp [g]
+  have hgN : g N = stoppedValueLimsup M τ := by
+    simp only [g, min_eq_left (hτN _), max_eq_right (hστ _)]
+  rw [← hg0, ← hgN]
+  exact antitone_nat_of_succ_le (f := fun k ↦ ∫⁻ ω in s, g k ω ∂P) hstep N.zero_le
+
+/-- **Optional stopping.** For an `ℝ≥0∞`-valued supermartingale with finite initial expectation
+under a finite measure, stopping times `σ ≤ τ` with values in `WithTop ℕ` and a set `s`
+measurable for the σ-algebra at `σ`, the set integral over `s` of the process at `τ` is at most
+its set integral at `σ`, the value at an infinite time being the almost sure limit
+[RW, Fact 7.5]. -/
+theorem setLIntegral_stoppedValueLimsup_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (hσ : IsStoppingTime ℱ σ)
+    (hτ : IsStoppingTime ℱ τ) (hστ : σ ≤ τ) (hs : MeasurableSet[hσ.measurableSpace] s) :
+    ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P := by
+  have hs' : MeasurableSet s := hσ.measurableSpace_le s hs
+  have htop : MeasurableSet {ω | σ ω = ⊤} := hσ.measurableSet_eq_top
+  rw [← lintegral_inter_add_sdiff _ s htop,
+    ← lintegral_inter_add_sdiff (stoppedValueLimsup M σ) s htop]
+  -- Where `σ` is infinite, so is `τ`, and the two values agree.
+  refine add_le_add (setLIntegral_congr_fun (hs'.inter htop) fun ω hω ↦ ?_).le ?_
+  · rw [stoppedValueLimsup_of_eq_top (top_le_iff.1 (hω.2 ▸ hστ ω)),
+      stoppedValueLimsup_of_eq_top hω.2]
+  -- Where `σ` is finite, apply the bounded case to `min σ N ≤ min τ N` on `s ∩ {σ ≤ N}`, and let
+  -- `N` tend to infinity with Fatou's lemma.
+  set F : ℕ → Ω → ℝ≥0∞ := fun N ↦
+    (s ∩ {ω | σ ω ≤ N}).indicator (stoppedValueLimsup M fun ω ↦ min (τ ω) N)
+  have hsN (N : ℕ) : MeasurableSet (s ∩ {ω | σ ω ≤ N}) :=
+    hs'.inter (ℱ.le N _ (hσ.measurableSet_le_natCast N))
+  have hsub (N : ℕ) : s ∩ {ω | σ ω ≤ N} ⊆ s \ {ω | σ ω = ⊤} := fun _ hω ↦
+    ⟨hω.1, ne_top_of_le_ne_top (WithTop.natCast_ne_top N) hω.2⟩
+  have hF_meas (N : ℕ) : Measurable (F N) :=
+    (measurable_stoppedValueLimsup hM.measurable
+      (hτ.min_natCast N).measurable').indicator (hsN N)
+  have hF_le (N : ℕ) :
+      ∫⁻ ω, F N ω ∂P ≤ ∫⁻ ω in s \ {ω | σ ω = ⊤}, stoppedValueLimsup M σ ω ∂P := by
+    rw [lintegral_indicator (hsN N)]
+    calc _ ≤ ∫⁻ ω in s ∩ {ω | σ ω ≤ N}, stoppedValueLimsup M (fun ω ↦ min (σ ω) N) ω ∂P := by
+          have h := hM.setLIntegral_stoppedValueLimsup_le_of_le_const hP (hσ.min_const N)
+            (hτ.min_const N) (fun ω ↦ min_le_min_right _ (hστ ω))
+            (fun ω ↦ (min_le_right _ _).trans_eq (Nat.cast_withTop N).symm)
+            ((hσ.measurableSet_inter_le_const_iff s N).1 (hs.inter (hσ.measurableSet_le' N)))
+          rwa [← Nat.cast_withTop] at h
+      _ = ∫⁻ ω in s ∩ {ω | σ ω ≤ N}, stoppedValueLimsup M σ ω ∂P :=
+          setLIntegral_congr_fun (hsN N) fun ω hω ↦
+            stoppedValueLimsup_congr (min_eq_left hω.2)
+      _ ≤ _ := lintegral_mono_set (hsub N)
+  have hF_tendsto : ∀ᵐ ω ∂P, Tendsto (fun N ↦ F N ω) atTop
+      (𝓝 ((s \ {ω | σ ω = ⊤}).indicator (stoppedValueLimsup M τ) ω)) := by
+    filter_upwards [hM.ae_tendsto_limsup hP h0] with ω hω
+    by_cases hωs : ω ∈ s \ {ω | σ ω = ⊤}
+    · obtain ⟨a, ha⟩ := WithTop.ne_top_iff_exists.1 hωs.2
+      rw [indicator_of_mem hωs]
+      refine (tendsto_stoppedValueLimsup_min hω).congr' ?_
+      filter_upwards [eventually_ge_atTop a] with N hN
+      have hσN : σ ω ≤ N := by rw [← ha, Nat.cast_withTop, WithTop.coe_le_coe]; exact hN
+      exact (indicator_of_mem (⟨hωs.1, hσN⟩ : ω ∈ s ∩ {ω | σ ω ≤ N}) _).symm
+    · rw [indicator_of_notMem hωs]
+      exact tendsto_const_nhds.congr fun N ↦
+        (indicator_of_notMem (fun h ↦ hωs (hsub N h)) _).symm
+  calc ∫⁻ ω in s \ {ω | σ ω = ⊤}, stoppedValueLimsup M τ ω ∂P
+      = ∫⁻ ω, liminf (fun N ↦ F N ω) atTop ∂P := by
+        rw [← lintegral_indicator (hs'.diff htop)]
+        exact lintegral_congr_ae (hF_tendsto.mono fun ω hω ↦ hω.liminf_eq.symm)
+    _ ≤ liminf (fun N ↦ ∫⁻ ω, F N ω ∂P) atTop := lintegral_liminf_le hF_meas
+    _ ≤ _ := liminf_le_of_frequently_le' (Frequently.of_forall hF_le)
+
+/-- Optional stopping at a single stopping time: the expectation of an `ℝ≥0∞`-valued
+supermartingale with finite initial expectation under a finite measure, at a stopping time with
+values in `WithTop ℕ`, is at most its initial expectation. -/
+theorem lintegral_stoppedValueLimsup_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) (hτ : IsStoppingTime ℱ τ) :
+    ∫⁻ ω, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω, M 0 ω ∂P := by
+  have h := hM.setLIntegral_stoppedValueLimsup_le hP h0 (σ := fun _ ↦ ((0 : ℕ) : WithTop ℕ))
+    (isStoppingTime_natCast 0) hτ (fun _ ↦ by simp) MeasurableSet.univ
+  rwa [stoppedValueLimsup_const, Measure.restrict_univ] at h
+
+/-- The set integrals of the almost sure limit of an `ℝ≥0∞`-valued supermartingale with finite
+initial expectation under a finite measure, over an `ℱ n`-measurable set, are at most those of
+`M n`. -/
+theorem setLIntegral_limsup_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P]
+    (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) {n : ℕ} (hs : MeasurableSet[ℱ n] s) :
+    ∫⁻ ω in s, limsup (fun k ↦ M k ω) atTop ∂P ≤ ∫⁻ ω in s, M n ω ∂P := by
+  have hσ : IsStoppingTime ℱ fun _ ↦ (n : WithTop ℕ) := isStoppingTime_natCast n
+  have h := hM.setLIntegral_stoppedValueLimsup_le hP h0 (τ := fun _ ↦ ⊤) hσ (fun _ ↦ by simp)
+    (fun _ ↦ le_top) (hσ.le_measurableSpace_of_const_le (fun _ ↦ (Nat.cast_withTop n).ge) s hs)
+  rwa [stoppedValueLimsup_const, stoppedValueLimsup_top] at h
+
+/-- The expectation of the almost sure limit of an `ℝ≥0∞`-valued supermartingale with finite
+initial expectation under a finite measure is at most its initial expectation. -/
+theorem lintegral_limsup_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P]
+    (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) :
+    ∫⁻ ω, limsup (fun n ↦ M n ω) atTop ∂P ≤ ∫⁻ ω, M 0 ω ∂P := by
+  simpa using hM.setLIntegral_limsup_le hP h0 (n := 0) MeasurableSet.univ
+
+end IsENNSupermartingale
+
+namespace IsTestSupermartingale
+
+/-- A test supermartingale converges almost surely under every finite member of the null, so that
+its `limsup` is its limit [RW, Fact 7.5]. -/
+theorem ae_tendsto_limsup (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] :
+    ∀ᵐ ω ∂P, Tendsto (fun n ↦ M n ω) atTop (𝓝 (limsup (fun n ↦ M n ω) atTop)) :=
+  hM.toIsENNSupermartingale.ae_tendsto_limsup hP
+    (hM.lintegral_zero_ne_top hP)
+
+/-- The almost sure limit of a test supermartingale is almost surely finite under every finite
+member of the null. -/
+theorem ae_limsup_lt_top (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] :
+    ∀ᵐ ω ∂P, limsup (fun n ↦ M n ω) atTop < ∞ :=
+  hM.toIsENNSupermartingale.ae_limsup_lt_top hP
+    (hM.lintegral_zero_ne_top hP)
+
+/-- The set integrals of the almost sure limit of a test supermartingale, over an `ℱ n`-measurable
+set, are at most those of `M n`, under every finite member of the null. -/
+theorem setLIntegral_limsup_le (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P]
+    {n : ℕ} (hs : MeasurableSet[ℱ n] s) :
+    ∫⁻ ω in s, limsup (fun k ↦ M k ω) atTop ∂P ≤ ∫⁻ ω in s, M n ω ∂P :=
+  hM.toIsENNSupermartingale.setLIntegral_limsup_le hP (hM.lintegral_zero_ne_top hP) hs
+
+/-- The expectation of the almost sure limit of a test supermartingale is at most its initial
+expectation, under every finite member of the null. -/
+theorem lintegral_limsup_le (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) [IsFiniteMeasure P] :
+    ∫⁻ ω, limsup (fun n ↦ M n ω) atTop ∂P ≤ ∫⁻ ω, M 0 ω ∂P :=
+  hM.toIsENNSupermartingale.lintegral_limsup_le hP (hM.lintegral_zero_ne_top hP)
+
+/-- The expectation of the almost sure limit of a test supermartingale is at most `1`, under every
+finite member of the null. -/
+theorem lintegral_limsup_le_one (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] : ∫⁻ ω, limsup (fun n ↦ M n ω) atTop ∂P ≤ 1 :=
+  (hM.lintegral_limsup_le hP).trans (hM.lintegral_zero_le P hP)
+
+/-- **Optional stopping for test supermartingales.** For stopping times `σ ≤ τ` with values in
+`WithTop ℕ`, a set `s` measurable for the σ-algebra at `σ` and a finite member `P` of the null,
+the set integral over `s` of a test supermartingale at `τ` is at most its set integral at `σ`
+[RW, Fact 7.5]. -/
+theorem setLIntegral_stoppedValueLimsup_le (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] (hσ : IsStoppingTime ℱ σ) (hτ : IsStoppingTime ℱ τ) (hστ : σ ≤ τ)
+    (hs : MeasurableSet[hσ.measurableSpace] s) :
+    ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P :=
+  hM.toIsENNSupermartingale.setLIntegral_stoppedValueLimsup_le hP
+    (hM.lintegral_zero_ne_top hP) hσ hτ hστ hs
+
+/-- The expectation of a test supermartingale at a stopping time with values in `WithTop ℕ` is at
+most its initial expectation, under every finite member of the null. -/
+theorem lintegral_stoppedValueLimsup_le (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] (hτ : IsStoppingTime ℱ τ) :
+    ∫⁻ ω, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω, M 0 ω ∂P :=
+  hM.toIsENNSupermartingale.lintegral_stoppedValueLimsup_le hP
+    (hM.lintegral_zero_ne_top hP) hτ
+
+/-- The expectation of a test supermartingale at a stopping time with values in `WithTop ℕ` is at
+most `1`, under every finite member of the null. -/
+theorem lintegral_stoppedValueLimsup_le_one (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] (hτ : IsStoppingTime ℱ τ) : ∫⁻ ω, stoppedValueLimsup M τ ω ∂P ≤ 1 :=
+  (hM.lintegral_stoppedValueLimsup_le hP hτ).trans (hM.lintegral_zero_le P hP)
+
+/-- The value of a test supermartingale for a null of probability measures at a stopping time
+with values in `WithTop ℕ` is an e-variable. -/
+theorem isEVar_stoppedValueLimsup (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hM : IsTestSupermartingale M ℱ S) (hτ : IsStoppingTime ℱ τ) :
+    IsEVar (stoppedValueLimsup M τ) S :=
+  IsEVar.of_lintegral_le_one hS (measurable_stoppedValueLimsup hM.measurable hτ.measurable')
+    fun P hP ↦ have := hS P hP; hM.lintegral_stoppedValueLimsup_le_one hP hτ
+
+end IsTestSupermartingale
+
+end ProbabilityTheory
diff --git a/LMLExplore/Probability/Process/StoppedValue.lean b/LMLExplore/Probability/Process/StoppedValue.lean
new file mode 100644
index 00000000..7b312371
--- /dev/null
+++ b/LMLExplore/Probability/Process/StoppedValue.lean
@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import Mathlib.MeasureTheory.Constructions.BorelSpace.Order
+public import Mathlib.Probability.Process.Stopping
+
+/-!
+# The value of a process at a possibly infinite time
+
+A random time of a filtration indexed by `ℕ` takes values in `WithTop ℕ`. Mathlib's
+`MeasureTheory.stoppedValue u τ` reads the process at `τ ω` where it is finite and takes an
+arbitrary value where `τ ω = ⊤`. Anytime-valid inference needs a canonical value at infinity: the
+value of a process at a possibly infinite stopping time is `u (τ ω) ω` where `τ ω` is finite and
+`limsup (u · ω)` where it is infinite [RRLK; RLKR23, (1.2)]. For nonnegative supermartingales with
+finite initial expectation, which converge almost surely, this is the almost sure limit, and
+optional stopping holds at every stopping time with this convention.
+
+## Main definitions
+
+* `MeasureTheory.stoppedValueLimsup u τ`: the value of `u` at the random time `τ`, with
+  `limsup (u · ω)` where `τ ω = ⊤`.
+
+## Main statements
+
+* `MeasureTheory.stoppedValueLimsup_of_eq_natCast`, `MeasureTheory.stoppedValueLimsup_of_eq_top`:
+  its values at finite and infinite times.
+* `MeasureTheory.stoppedValueLimsup_natCast`: at an `ℕ`-valued random time it reads the process at
+  that time.
+* `MeasureTheory.stoppedValueLimsup_eq_stoppedValue`: where `τ` is finite it agrees with Mathlib's
+  `stoppedValue`.
+* `MeasureTheory.tendsto_stoppedValueLimsup_min`: for a convergent process, the values at the
+  truncated times `min τ N` converge to the value at `τ`.
+* `MeasureTheory.measurable_stoppedValueLimsup`: it is measurable for measurable `u n` and `τ`.
+
+## References
+
+* [RRLK] A. Ramdas, J. Ruf, M. Larsson and W. M. Koolen, *Admissible anytime-valid sequential
+  inference must rely on nonnegative martingales*, arXiv:2009.03167.
+* [RLKR23] J. Ruf, M. Larsson, W. M. Koolen and A. Ramdas, *A composite generalization of Ville's
+  martingale theorem using e-processes*, Electron. J. Probab. 28 (2023), arXiv:2203.04485.
+-/
+
+public section
+
+open Filter Topology
+
+namespace MeasureTheory
+
+variable {Ω β : Type*} {τ : Ω → WithTop ℕ} {ω : Ω}
+
+section ConditionallyCompleteLattice
+
+variable [ConditionallyCompleteLattice β] {u : ℕ → Ω → β}
+
+/-- The value of the process `u` at the random time `τ : Ω → WithTop ℕ`: `u n ω` where
+`τ ω = n`, and `limsup (u · ω)` where `τ ω = ⊤` [RRLK; RLKR23, (1.2)]. Unlike Mathlib's
+`stoppedValue`, its value at infinity is meaningful: for an almost surely convergent process it is
+the limit. -/
+noncomputable def stoppedValueLimsup (u : ℕ → Ω → β) (τ : Ω → WithTop ℕ) (ω : Ω) : β :=
+  if τ ω = ⊤ then limsup (fun n ↦ u n ω) atTop else u (τ ω).untopA ω
+
+/-- Where the random time is finite, `stoppedValueLimsup` reads the process at that time. -/
+theorem stoppedValueLimsup_of_eq_natCast {n : ℕ} (h : τ ω = n) :
+    stoppedValueLimsup u τ ω = u n ω := by
+  simp only [stoppedValueLimsup, h, WithTop.natCast_ne_top, ↓reduceIte]
+  -- `Nat.cast` into `WithTop ℕ` is `WithTop.some`, which `untop` inverts.
+  rw [WithTop.untopA_eq_untop (WithTop.natCast_ne_top n),
+    (WithTop.untop_eq_iff _).2 (Nat.cast_withTop n)]
+
+/-- Where the random time is infinite, `stoppedValueLimsup` is the `limsup` of the process. -/
+theorem stoppedValueLimsup_of_eq_top (h : τ ω = ⊤) :
+    stoppedValueLimsup u τ ω = limsup (fun n ↦ u n ω) atTop := by
+  simp [stoppedValueLimsup, h]
+
+/-- The value of a process at a random time at `ω` depends only on the time at `ω`. -/
+theorem stoppedValueLimsup_congr {τ' : Ω → WithTop ℕ} (h : τ ω = τ' ω) :
+    stoppedValueLimsup u τ ω = stoppedValueLimsup u τ' ω := by
+  simp only [stoppedValueLimsup, h]
+
+/-- At a finite random time, the coercion of an `ℕ`-valued one, `stoppedValueLimsup` reads the
+process at that time. -/
+@[simp]
+theorem stoppedValueLimsup_natCast (u : ℕ → Ω → β) (τ : Ω → ℕ) :
+    stoppedValueLimsup u (fun ω ↦ (τ ω : WithTop ℕ)) = fun ω ↦ u (τ ω) ω :=
+  funext fun _ ↦ stoppedValueLimsup_of_eq_natCast rfl
+
+/-- At a constant finite time, `stoppedValueLimsup` is the process at that time. -/
+theorem stoppedValueLimsup_const (u : ℕ → Ω → β) (n : ℕ) :
+    stoppedValueLimsup u (fun _ ↦ (n : WithTop ℕ)) = u n :=
+  stoppedValueLimsup_natCast u fun _ ↦ n
+
+/-- At the constant time `⊤`, `stoppedValueLimsup` is the `limsup` of the process. -/
+@[simp]
+theorem stoppedValueLimsup_top (u : ℕ → Ω → β) :
+    stoppedValueLimsup u (fun _ ↦ ⊤) = fun ω ↦ limsup (fun n ↦ u n ω) atTop :=
+  funext fun _ ↦ stoppedValueLimsup_of_eq_top rfl
+
+/-- Where the random time is finite, `stoppedValueLimsup` agrees with Mathlib's `stoppedValue`. -/
+theorem stoppedValueLimsup_eq_stoppedValue (h : τ ω ≠ ⊤) :
+    stoppedValueLimsup u τ ω = stoppedValue u τ ω := by
+  simp [stoppedValueLimsup, stoppedValue, h]
+
+/-- For a process that converges at `ω` (to its `limsup`), the values at the truncated times
+`min τ N` converge to the value at `τ`. -/
+theorem tendsto_stoppedValueLimsup_min [TopologicalSpace β]
+    (h : Tendsto (fun n ↦ u n ω) atTop (𝓝 (limsup (fun n ↦ u n ω) atTop))) :
+    Tendsto (fun N : ℕ ↦ stoppedValueLimsup u (fun ω ↦ min (τ ω) N) ω) atTop
+      (𝓝 (stoppedValueLimsup u τ ω)) := by
+  induction hτω : τ ω using WithTop.recTopCoe with
+  | top =>
+    rw [stoppedValueLimsup_of_eq_top hτω]
+    exact h.congr fun N ↦ (stoppedValueLimsup_of_eq_natCast (by simp [hτω])).symm
+  | coe b =>
+    rw [← Nat.cast_withTop] at hτω
+    rw [stoppedValueLimsup_of_eq_natCast hτω]
+    refine tendsto_const_nhds.congr' ?_
+    filter_upwards [eventually_ge_atTop b] with N hN
+    refine (stoppedValueLimsup_of_eq_natCast ?_).symm
+    rw [hτω, min_eq_left (by exact_mod_cast hN)]
+
+end ConditionallyCompleteLattice
+
+/-- The value of a process of measurable functions at a measurable random time is measurable. -/
+theorem measurable_stoppedValueLimsup [ConditionallyCompleteLinearOrder β] [TopologicalSpace β]
+    [OrderTopology β] [SecondCountableTopology β] [MeasurableSpace β] [BorelSpace β]
+    {mΩ : MeasurableSpace Ω} {u : ℕ → Ω → β} (hu : ∀ n, Measurable (u n)) (hτ : Measurable τ) :
+    Measurable (stoppedValueLimsup u τ) := by
+  have h : Measurable fun p : Ω × WithTop ℕ ↦ stoppedValueLimsup u (fun _ ↦ p.2) p.1 := by
+    refine measurable_from_prod_countable_left fun k ↦ ?_
+    cases k with
+    | top => simpa using Measurable.limsup hu
+    | coe n => simpa using hu n
+  exact h.comp (measurable_id.prodMk hτ)
+
+end MeasureTheory
diff --git a/LMLExplore/Probability/Process/Stopping.lean b/LMLExplore/Probability/Process/Stopping.lean
index 09cc9e05..21d153c7 100644
--- a/LMLExplore/Probability/Process/Stopping.lean
+++ b/LMLExplore/Probability/Process/Stopping.lean
@@ -9,13 +9,14 @@ public import Mathlib.MeasureTheory.MeasurableSpace.Instances
 public import Mathlib.Probability.Process.Stopping
 
 /-!
-# Stopping times valued in `ℕ∞` and stopped adapted processes
+# Stopping times valued in `WithTop ℕ` and stopped adapted processes
 
 A stopping time of a filtration indexed by `ℕ` takes values in `WithTop ℕ`, which Mathlib equips
 with its Borel σ-algebra, and `IsStoppingTime.measurable'` is measurability for that σ-algebra.
 The same type seen as `ℕ∞` carries the discrete σ-algebra `⊤`; the two instances are not
 syntactically equal. This file states measurability of such a stopping time for the discrete
-σ-algebra of `ℕ∞`.
+σ-algebra of `ℕ∞`. It also restates Mathlib's stopping-time API for `WithTop ℕ`-valued times at
+the cast `(n : WithTop ℕ)` of a natural number.
 
 A process that is adapted, in the sense of measurability, to a filtration indexed by a discrete
 order stays adapted when it is stopped at a stopping time; Mathlib states this for strongly adapted
@@ -25,6 +26,10 @@ processes.
 
 * `MeasureTheory.IsStoppingTime.measurable_enat`: a stopping time `τ : Ω → ℕ∞` of a filtration
   indexed by `ℕ` is measurable for the discrete σ-algebra of `ℕ∞`.
+* `MeasureTheory.IsStoppingTime.measurableSet_le_natCast`,
+  `MeasureTheory.IsStoppingTime.measurableSet_natCast_lt`, `MeasureTheory.isStoppingTime_natCast`,
+  `MeasureTheory.IsStoppingTime.min_natCast`: Mathlib's stopping-time API for `WithTop ℕ`-valued
+  times, stated at the cast `(n : WithTop ℕ)` rather than the coercion `WithTop.some n`.
 * `MeasureTheory.Adapted.stoppedProcess_of_discrete`: a stopped adapted process is adapted.
 -/
 
@@ -62,4 +67,42 @@ theorem Adapted.stoppedProcess_of_discrete {ι γ : Type*} [Nonempty ι] [Linear
     Adapted f (stoppedProcess u τ) :=
   (hu.stronglyAdapted.stoppedProcess_of_discrete hτ).adapted
 
+/-! ### Stopping times in `WithTop ℕ` at the cast of a natural number
+
+Mathlib's stopping-time API is stated at the coercion `WithTop.some n`, while statements about
+`WithTop ℕ`-valued times use the cast `(n : WithTop ℕ)`; the following lemmas convert between them
+by `Nat.cast_withTop`. -/
+
+section NatCast
+
+variable {ℱ : Filtration ℕ mΩ} {τ : Ω → WithTop ℕ}
+
+/-- For a stopping time with values in `WithTop ℕ`, `{ω | τ ω ≤ n}` is `ℱ n`-measurable, at the
+cast `(n : WithTop ℕ)`. -/
+theorem IsStoppingTime.measurableSet_le_natCast (hτ : IsStoppingTime ℱ τ) (n : ℕ) :
+    MeasurableSet[ℱ n] {ω | τ ω ≤ n} := by
+  rw [Nat.cast_withTop]
+  exact hτ n
+
+/-- For a stopping time with values in `WithTop ℕ`, `{ω | n < τ ω}` is `ℱ n`-measurable, at the
+cast `(n : WithTop ℕ)`. -/
+theorem IsStoppingTime.measurableSet_natCast_lt (hτ : IsStoppingTime ℱ τ) (n : ℕ) :
+    MeasurableSet[ℱ n] {ω | (n : WithTop ℕ) < τ ω} := by
+  rw [Nat.cast_withTop]
+  exact hτ.measurableSet_gt n
+
+/-- The constant time `(n : WithTop ℕ)` is a stopping time. -/
+theorem isStoppingTime_natCast (n : ℕ) : IsStoppingTime ℱ fun _ ↦ (n : WithTop ℕ) := by
+  rw [Nat.cast_withTop]
+  exact isStoppingTime_const ℱ n
+
+/-- The minimum of a stopping time with values in `WithTop ℕ` and the cast `(n : WithTop ℕ)` is a
+stopping time. -/
+theorem IsStoppingTime.min_natCast (hτ : IsStoppingTime ℱ τ) (n : ℕ) :
+    IsStoppingTime ℱ fun ω ↦ min (τ ω) n := by
+  rw [Nat.cast_withTop]
+  exact hτ.min_const n
+
+end NatCast
+
 end MeasureTheory