[RemyDegenne]

This PR proves the almost sure convergence of ℝ≥0∞-valued supermartingales and optional stopping at arbitrary stopping times with values in WithTop ℕ. These are the EValues roadmap's Layer 2.2 target, Convergence and optional stopping in ℝ≥0∞ [RW, Fact 7.5; ShSVV11]. It builds on IsENNSupermartingale and IsTestSupermartingale (EValues/TestSupermartingale.lean, merged in #385). It keeps their conventions: ℝ≥0∞ values, set integrals, any filtration indexed by ℕ, any null S.

Roadmap: EValues

LMLExplore/Probability/Process/StoppedValue.lean (129 lines, namespace MeasureTheory) defines stoppedValueLimsup u τ ω: u n ω where τ ω = n, and limsup (u · ω) where τ ω = ⊤. This is the convention the roadmap fixes for the value of a process at a possibly infinite stopping time [RRLK; RLKR23, (1.2)]. The definition follows the shape in Suggested.lean, with a general value type β. Its API:

• stoppedValueLimsup_of_eq_coe and stoppedValueLimsup_of_eq_top give its values; stoppedValueLimsup_congr says the value at ω depends only on τ ω. The body is not exposed.
• stoppedValueLimsup_natCast (@[simp]) reads the process at an ℕ-valued random time fun ω ↦ (τ ω : WithTop ℕ). stoppedValueLimsup_const follows from it, and stoppedValueLimsup_top (@[simp]) handles the constant time ⊤.
• stoppedValueLimsup_eq_stoppedValue says it agrees with Mathlib's stoppedValue where τ is finite.
• tendsto_stoppedValueLimsup_min: for a convergent process, the values at min τ N converge to the value at τ.
• measurable_stoppedValueLimsup.

LMLExplore/Probability/Martingale/OptionalStopping.lean (303 lines, namespace ProbabilityTheory) goes in the home the roadmap suggests for this material. For IsENNSupermartingale M ℱ S, P ∈ S finite and ∫⁻ M 0 ∂P ≠ ∞:

• Convergence: ae_tendsto_limsup (almost sure convergence to the limsup) and ae_limsup_lt_top (the limit is almost surely finite). They come from Mathlib's Submartingale.exists_ae_tendsto_of_bdd applied to -(M n).toReal, through the existing bridge IsENNSupermartingale.supermartingale_toReal.
• setLIntegral_limsup_le and lintegral_limsup_le: for ℱ n-measurable s, ∫⁻ in s, limsup M ≤ ∫⁻ in s, M n, so in particular ∫⁻ M ∞ ≤ ∫⁻ M 0.
• setLIntegral_stoppedValueLimsup_le_of_le_const, the bounded case: for stopping times σ ≤ τ ≤ N and s measurable for hσ.measurableSpace, ∫⁻ in s, M_τ ≤ ∫⁻ in s, M_σ. It holds for every ℝ≥0∞-valued supermartingale under every member of the null, with no finiteness or integrability. The proof works in ℝ≥0∞: the times max σ (min τ k) interpolate from σ to τ and move only on the ℱ k-measurable event σ ≤ k < τ. Mathlib's Submartingale.expected_stoppedValue_mono is the real, integrable version.
• setLIntegral_stoppedValueLimsup_le, the general case: the same inequality for arbitrary stopping times σ ≤ τ in WithTop ℕ. On {σ = ⊤} the two values agree. On {σ < ⊤} we apply the bounded case to min σ N ≤ min τ N on s ∩ {σ ≤ N} (Mathlib's measurableSet_inter_le_const_iff) and let N → ∞ with Fatou's lemma and the almost sure convergence.
• lintegral_stoppedValueLimsup_le: ∫⁻ M_τ ≤ ∫⁻ M 0.

For IsTestSupermartingale, with no finiteness hypothesis beyond IsFiniteMeasure P, the file adds ae_tendsto_limsup, ae_limsup_lt_top, setLIntegral_stoppedValueLimsup_le and lintegral_stoppedValueLimsup_le (the signature in Suggested.lean, stated for any S). It also adds lintegral_stoppedValueLimsup_le_one and isEVar_stoppedValueLimsup: for a null of probability measures, the value of a test supermartingale at every stopping time in WithTop ℕ is an e-variable (Statlib's IsEVar).

EValues/TestSupermartingale.lean gains IsTestSupermartingale.lintegral_zero_ne_top (finite initial expectation under every member of the null). It replaces the inline term ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne at its three uses there and four uses in the new file.

Consumers: Layer 3.1 of the same roadmap (IsEProcess.isEVar_stoppedValueLimsup in Suggested.lean, and [RRLK, Lemma 6]'s equivalence with validity at all stopping times under the stoppedValueLimsup convention) passes through test supermartingales that dominate e-processes and uses isEVar_stoppedValueLimsup and setLIntegral_stoppedValueLimsup_le. Layer 3.2's Ville inequalities at stopping times in WithTop ℕ use them too. This PR does not depend on the stopped processes of the open #391: the bounded case is proved directly and does not overlap with it.

Reuse: I searched the pinned Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for a value at infinite stopping times (stoppedValueLimsup, limsup with stoppedValue), for convergence of ℝ≥0∞-valued or nonnegative supermartingales, and for optional stopping in ℝ≥0∞ or at unbounded stopping times. I found none. Mathlib's convergence (Submartingale.exists_ae_tendsto_of_bdd) and optional stopping (Submartingale.expected_stoppedValue_mono) are real-valued, and the latter only covers bounded times. The file has two private helpers, order facts about the interpolating times max a (min b k) in WithTop ℕ. The step ↑k < b → ↑(k + 1) ≤ b they use is Mathlib's ENat.natCast_add_one_le_iff. No proof is longer than 50 lines. No public declaration is removed or renamed, and no Mathlib material is vendored.

Milestone: EValues Layer 2.2. With this PR both bullets of Layer 2.2 are covered (convergence with ∫⁻ M ∞ ≤ ∫⁻ M 0, and optional stopping at σ ≤ τ in WithTop ℕ with stoppedValueLimsup). Next comes Layer 2.3, the exact Ville identity and Ville's inequality for ℝ≥0∞-valued test supermartingales.

Local checks (not CI): tauceti-local-checks verify --policy ordinary exited 0.

• scope: scoped: against dca76852a43d553a35fb2afa9d31ae4b37501dde
• Whole-library lake build --iofail succeeded (8601 jobs).
• local-axioms: checked 3 changed module(s), 95 declaration(s); 0 violation(s)
• The module-system, header-style and local-lint checks passed (14 environment linters).

🤖 Prepared with Claude Code

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	stoppedValueLimsup matches the roadmap definition (Suggested.lean:180, untopA vs untop h is the same value off ⊤), and the convergence, bounded and unbounded optional stopping, and e-variable statements are the correct ℝ≥0∞ results, using the real one-step condition of IsENNSupermartingale (TestSupermartingale.lean:106). Finiteness of P and of ∫⁻ M 0 is assumed only where convergence needs it.
✅	reuse	approved	claude/claude-opus-5-5	No existing Mathlib or LMLExplore declaration provides stoppedValueLimsup, a.s. convergence of ℝ≥0∞-valued supermartingales, or lintegral optional stopping at WithTop ℕ stopping times; the proofs reuse Submartingale.exists_ae_tendsto_of_bdd via the existing supermartingale_toReal bridge, plus Mathlib's min_const, measurableSet_le', measurableSet_inter_le_const_iff, measurable_from_prod_countable_left and ENat.natCast_add_one_le_iff. The cast-form stopping-time lemmas in Stopping.lean have no Mathlib counterpart at (n : WithTop ℕ), since Mathlib's Stopping.lean states only isStoppingTime_const, min_const and measurableSet_le' at the coercion, and they are used several times; IsENNSupermartingale.stoppedProcess (TestSupermartingale.lean:595) gives only single-time stopping and cannot replace the σ ≤ τ, s ∈ ℱ_σ bounded case.
✅	scope	approved	claude/claude-opus-5-5	The PR implements EValues Layer 2.2 (README.md:496-503) directly: almost sure convergence with ∫⁻ M ∞ ≤ ∫⁻ M 0, and optional stopping for σ ≤ τ in WithTop ℕ via stoppedValueLimsup (Suggested.lean:180, 204). The lintegral_zero_ne_top helper and the stopping-time lemmas at the cast are prerequisites the new proofs use directly, so the PR is one topic.
✅	attribution	approved	claude/claude-opus-5-5	The new files credit their informal sources ([RW, Fact 7.5], [ShSVV11], [RRLK], [RLKR23, (1.2)]) and the Mathlib results they build on (Submartingale.exists_ae_tendsto_of_bdd, Submartingale.expected_stoppedValue_mono), and the code never mentions the roadmap. The bounded optional-stopping proof uses its own max σ (min τ k) interpolation rather than adapting Mathlib's proof, so no further formal credit is needed.
✅	api-design	approved	claude/claude-opus-5-5	The stoppedValueLimsup API characterizes the definition completely with its body hidden and sound simp annotations; the private helpers are specific to the interpolation argument and the IsTestSupermartingale surface mirrors the IsENNSupermartingale one.
✅	generality	approved	claude/claude-opus-5-5	Convergence and optional stopping are proved once for IsENNSupermartingale, with the bounded case needing no assumptions, and the test-supermartingale results are one-line specialisations that are more general than the roadmap's {P} signature. stoppedValueLimsup is stated for a general conditionally complete lattice, and the finiteness hypotheses are exactly those the Mathlib convergence step needs.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration is in its natural home: the general stopping-time lemmas are now in Process/Stopping.lean, stoppedValueLimsup is in Process/, and optional stopping is in the roadmap's suggested Martingale/ home. No import is unused or too broad.
✅	naming	approved	claude/claude-opus-5-5	Names follow the roadmap's Suggested.lean (stoppedValueLimsup, lintegral_stoppedValueLimsup_le, isEVar_stoppedValueLimsup) and Mathlib precedent (stoppedValue_const, isStoppingTime_const, min_const), and each describes its conclusion without overstating it. No notation is introduced and namespaces are appropriate for dot notation.
✅	documentation	approved	claude/claude-opus-5-5	Both new modules have accurate module docstrings, every public declaration's docstring states its result and hypotheses without overclaiming or roadmap/process narrative, and the Main statements lists match the declarations added. The Stopping.lean module docstring was updated to cover the new cast lemmas.
✅	proof-quality	approved	claude/claude-opus-5-5	The bridges between WithTop.some and Nat.cast are explicit rewrites with the rfl lemma Nat.cast_withTop (not @[simp]) or the new *_natCast helpers, with no change/show or undocumented defeq. The bounded and general optional-stopping proofs are split into named, commented steps (hstep, hF_le, hF_tendsto, a Fatou calc) and the order facts are factored into private helpers.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 2e2995b. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.46.}

[RemyDegenne]

🟡 naming — request_changes claude/claude-opus-5-5

Names describe conclusions in standard terminology and no notation is introduced, but stoppedValueLimsup_of_eq_coe is named after a coercion (WithTop.some) its statement does not use: it is stated at Nat.cast, which the rest of the file consistently calls natCast.

• LMLExplore/Probability/Process/StoppedValue.lean:71 — stoppedValueLimsup_of_eq_coe has hypothesis τ ω = (n : WithTop ℕ), which is Nat.cast, not the coercion WithTop.some. The file explicitly separates the two and names its other cast lemmas _natCast, so _coe misdescribes the hypothesis. Fix: Rename to stoppedValueLimsup_of_eq_natCast and update all uses: lines 29, 93, 120, 123 and 126 here, plus hg_succ and hg in OptionalStopping.lean.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 26s · 83.4k in (66.9k cache read, 16.5k cache write) / 2.5k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[lmlexplore-automation]

⚠️ This PR no longer merges into main. Rebase it onto current main (or merge main into it) and push — nothing downstream can make progress until then, since a green build and an approving review on this head still cannot merge.

Do check what the conflict actually is before resolving it mechanically. If main has since landed its own version of something this PR adds, part of it may be superseded, and the right answer is to drop that part — or close the PR — rather than to reconcile the text. That is an authoring decision.