[RemyDegenne]

This PR adds LMLExplore/EValues/OptionalStopping.lean and LMLExplore/Probability/Process/StoppedValueLimsup.lean. It proves that ℝ≥0∞-valued supermartingales converge, and that optional stopping holds at arbitrary stopping times. Together these complete the EValues target Layer 2, item 2: "Convergence and optional stopping in ℝ≥0∞" [RW, Fact 7.5; ShSVV11, Theorem 1].

Roadmap: EValues

It contains:

• ProbabilityTheory.stoppedValueLimsup M τ. This is the value of a process at a time τ : Ω → WithTop ι: M (τ ω) ω where τ ω is finite, and limsup (M · ω) where τ ω = ⊤. This follows the roadmap's Conventions [RRLK; RLKR23, (1.2)]. It and its API live in LMLExplore/Probability/Process/StoppedValueLimsup.lean, since they use no EValues theory. Its API:

  • _of_eq_top, _of_ne_top, _of_eq_coe and _congr;
  • the simp lemmas _coe and _top, plus _const;
  • stoppedProcess_eq_stoppedValueLimsup, limsup_stoppedProcess (the value is the limsup of the stopped process) and tendsto_stoppedProcess_stoppedValueLimsup;
  • measurable_stoppedValueLimsup.

  The pointwise API is stated for any linearly ordered time, like Mathlib's stoppedValue/stoppedProcess. Its coercions are then WithTop.some, which is what Mathlib's stopping-time lemmas produce.

• Convergence (first bullet of the item). IsENNSupermartingale.ae_tendsto_limsup: under a finite measure, a supermartingale with finite initial expectation converges a.s. to its limsup. This is derived from Mathlib's Submartingale.exists_ae_tendsto_of_bdd, through the existing bridge IsENNSupermartingale.supermartingale_toReal. Further results:

  • setLIntegral_limsup_le: the limit closes the supermartingale on ℱ n-measurable sets;
  • lintegral_limsup_le: ∫⁻ M ∞ ≤ ∫⁻ M 0;
  • ae_limsup_lt_top: the limit is a.s. finite;
  • the test-supermartingale versions, using IsTestSupermartingale.lintegral_zero_ne_top, which is added to TestSupermartingale.lean and replaces the three inline proofs of that fact there.

• Optional stopping (second bullet). IsENNSupermartingale.setLIntegral_stoppedValueLimsup_le is the roadmap statement: for stopping times σ ≤ τ with values in WithTop ℕ, and every s measurable for hσ.measurableSpace, ∫⁻ ω in s, stoppedValueLimsup M τ ω ∂P ≤ ∫⁻ ω in s, stoppedValueLimsup M σ ω ∂P. It assumes nothing beyond ∫⁻ M 0 ∂P ≠ ∞ and a finite P. Other forms:

  • setLIntegral_stoppedProcess_le: the fixed-time comparison of stopped processes, with no integrability at all;
  • lintegral_stoppedValueLimsup_le;
  • for test supermartingales, IsTestSupermartingale.lintegral_stoppedValueLimsup_le_one (the item's "in particular ∫⁻ M τ ≤ 1") and isEVar_stoppedValueLimsup: the value at any stopping time is an e-variable.

How each part is proved:

• Fixed time. Induction on the time, splitting along {σ ≤ n} and {n < τ}; this works directly in ℝ≥0∞, with no subtraction.
• Bounded σ. Fatou's lemma along the stopped process, using the a.s. convergence.
• General σ. The events {σ ≤ k} exhaust {σ < ⊤}, through IsStoppingTime.measurableSet_inter_le_const_iff.

Why this step next: Layer 3 (e-processes) is the next layer on the critical path, and it consumes stoppedValueLimsup and this optional stopping theorem. The two consumers are IsEProcess.isEVar_stoppedValueLimsup (validity at all stopping times with the limsup convention, [RRLK, Lemma 6]) and the Snell-envelope characterisation of Layer 3.1. After this PR, Layer 2.2 has nothing left. The next Layer 2 work is item 3: the exact Ville identity and Ville's inequality in ℝ≥0∞.

Reuse: I searched Mathlib, Tau Ceti, Statlib, LML and LMLExplore/ for ℝ≥0∞-valued supermartingale convergence, optional stopping with set integrals, and a limsup-valued stopped value, and found none. Mathlib's Submartingale.expected_stoppedValue_mono covers only bounded stopping times and integrable real processes, with no sets. This PR reuses:

• Tau Ceti's MeasureTheory.measurable_stoppedValue_of_countable and stoppedValue_of_eq (TauCeti/Probability/Process/StoppedValue.lean, newly imported; it is light);
• Mathlib's martingale convergence and stopping-time σ-algebra API;
• the existing IsENNSupermartingale bridges.

The private one-step lemma setLIntegral_stoppedProcess_succ_le is the special case, for ℱ n-measurable sets, of IsENNSupermartingale.stoppedProcess in the open PR #391, which is not on main. Once #391 lands, it can be replaced by (hM.stoppedProcess hτ).setLIntegral_succ_le. Inside namespace IsENNSupermartingale, stoppedProcess is written MeasureTheory.stoppedProcess; otherwise #391's theorem of that name would shadow it. I checked that the file compiles with a stub of that theorem in scope.

No declarations are removed or renamed.

Local checks (not CI): tauceti-local-checks verify --policy ordinary — scope: scoped: against dca76852a43d553a35fb2afa9d31ae4b37501dde, local-sources: PASS, whole-library lake build --iofail succeeded, local-axioms: checked 3 changed module(s), 98 declaration(s); 0 violation(s), module-system, header-style, and environment lint (local-lint: checked 3 changed module(s), 98 declarations) passed.

🤖 Prepared with Claude Code

[RemyDegenne]

AI review — changes requested

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	The definitions and theorems faithfully state the roadmap's Layer 2.2 results: a.s. convergence to the limsup, the closure inequality, and optional stopping at arbitrary WithTop ℕ stopping times on F_σ-measurable sets, with no hypotheses beyond finite P and finite ∫⁻ M 0. I tried to break each statement and its edge cases ({σ = ⊤}, bounded σ, constant times) and found no faithfulness defect.
✅	reuse	approved	claude/claude-opus-5-5	Nothing in Mathlib or LMLExplore already covers stoppedValueLimsup, isStoppingTime_top, ℝ≥0∞ supermartingale convergence or optional stopping at arbitrary stopping times, and the proofs reuse Mathlib's martingale convergence and stopping-time API. The new lintegral_zero_ne_top replaces three inline copies of the same proof.
✅	scope	approved	claude/claude-opus-5-5	The PR completes EValues Layer 2.2 (README.md:496-503): almost-sure convergence in ℝ≥0∞ and optional stopping at arbitrary WithTop ℕ stopping times using the roadmap's stoppedValueLimsup convention. The only change to existing code is the lintegral_zero_ne_top helper, which the new theorems use, so the PR is one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	Both new files cite the informal sources the work follows (RW Fact 7.5, ShSVV11 Theorem 1, RRLK, RLKR23 (1.2)) with locations matching the roadmap item, and name the Mathlib martingale results they build on. Nothing is vendored or closely followed without credit, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The public surface is minimal and the stoppedValueLimsup body stays hidden behind a complete set of characterising lemmas with sound @[simp] tags. The private helpers are proof-specific or already covered by Mathlib, and the PR leaves no compatibility layer.
✅	generality	approved	claude/claude-opus-5-5	Statements sit at the natural level: the general optional stopping theorem is proved once and the fixed-time, from-zero, limsup and test-supermartingale forms are derived from it, with hypotheses that match the Mathlib convergence theorem's needs and a time index as general as Mathlib's stoppedValue.
🟡	placement	changes requested	claude/claude-opus-5-5	The new material is well placed except for the generic lemma MeasureTheory.isStoppingTime_top, which belongs in the existing LMLExplore/Probability/Process/Stopping.lean, not in StoppedValueLimsup.lean. Both new imports are used.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard Mathlib terminology, match the roadmap's suggested names (stoppedValueLimsup, setLIntegral_stoppedValueLimsup_le, isEVar_stoppedValueLimsup) and follow the existing IsENNSupermartingale/IsTestSupermartingale namespaces; no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Both new modules have accurate module docstrings with mathematical references and no roadmap or process narrative, and every public definition and main theorem has a docstring that matches its statement without overclaiming.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and well structured: the one-step and bounded-σ cases are separate lemmas, the main theorem's comments explain how it splits and exhausts the events, and there is no undocumented defeq reliance or change/show. The repeated finite-initial-expectation fact is now the reusable lemma lintegral_zero_ne_top.

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

_{Reviewing this diff at head b3de0d2. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.49.}

[RemyDegenne]

🟡 api-design — request_changes claude/claude-opus-5-5

The stoppedValueLimsup API is complete, its body is not exposed, and the simp annotations are sound. One general stopping-time lemma is in the wrong file, and one private helper duplicates Mathlib's Order.add_one_le_of_lt.

• LMLExplore/Probability/Process/StoppedValueLimsup.lean:49 — MeasureTheory.isStoppingTime_top is a general stopping-time fact that mentions only Mathlib types, but it was placed in the stoppedValueLimsup file instead of the library's existing stopping-time file. Fix: Move isStoppingTime_top to LMLExplore/Probability/Process/Stopping.lean, next to measurable_enat, and import it from there.
• LMLExplore/EValues/OptionalStopping.lean:96 — The private coe_add_one_le_of_coe_lt is a general WithTop ℕ (= ℕ∞) order fact that Mathlib already provides as Order.add_one_le_of_lt. Fix: Delete the helper and use by exact_mod_cast Order.add_one_le_of_lt (α := ℕ∞) h at its two call sites (lines 116 and 143).

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 · 36s · 141.1k in (128k cache read, 13.1k cache write) / 3.4k 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.

[RemyDegenne]

Superseded by #395

#395 merged as 13fc17b22a3b6db29b36567ff9c2c04893ac139b. It targets the same EValues Layer 2.2 item, Convergence and optional stopping in ℝ≥0∞, and it delivers all of this PR's results. I checked this against the source at main 13fc17b22a3b6db29b36567ff9c2c04893ac139b, which is the merge commit of #395 and the current tip of main. Rebasing this PR would produce a second stoppedValueLimsup definition and a second copy of every theorem, so the repo rules would require deleting it all.

Declaration mapping (this PR → main)

LMLExplore/Probability/Process/StoppedValueLimsup.lean → LMLExplore/Probability/Process/StoppedValue.lean (namespace MeasureTheory; time index ℕ, any value type β, which is the shape in the roadmap's Suggested.lean):

• ProbabilityTheory.stoppedValueLimsup (generic ι, ℝ≥0∞ values) → MeasureTheory.stoppedValueLimsup
• stoppedValueLimsup_of_eq_top → stoppedValueLimsup_of_eq_top
• stoppedValueLimsup_of_ne_top → stoppedValueLimsup_eq_stoppedValue
• stoppedValueLimsup_of_eq_coe → stoppedValueLimsup_of_eq_natCast
• stoppedValueLimsup_congr → stoppedValueLimsup_congr
• stoppedValueLimsup_coe (simp) → stoppedValueLimsup_natCast (simp)
• stoppedValueLimsup_const → stoppedValueLimsup_const
• stoppedValueLimsup_top (simp) → stoppedValueLimsup_top (simp)
• tendsto_stoppedProcess_stoppedValueLimsup, stoppedProcess_eq_stoppedValueLimsup, limsup_stoppedProcess → tendsto_stoppedValueLimsup_min. Main expresses the truncation as stoppedValueLimsup M (min τ N) and not as stoppedProcess M τ N. These two are the same function, because stoppedProcess M τ N = stoppedValue M (min τ N).
• measurable_stoppedValueLimsup → measurable_stoppedValueLimsup (main's version is more general)

LMLExplore/EValues/OptionalStopping.lean → LMLExplore/Probability/Martingale/OptionalStopping.lean:

• IsENNSupermartingale.ae_tendsto_limsup, ae_limsup_lt_top, setLIntegral_limsup_le, lintegral_limsup_le, setLIntegral_stoppedValueLimsup_le, lintegral_stoppedValueLimsup_le → the same names, with the same hypotheses
• private setLIntegral_stoppedValueLimsup_le_of_le_const → public IsENNSupermartingale.setLIntegral_stoppedValueLimsup_le_of_le_const. Main's version is stronger: it needs neither h0 nor IsFiniteMeasure.
• IsTestSupermartingale.ae_tendsto_limsup, ae_limsup_lt_top, setLIntegral_stoppedValueLimsup_le, lintegral_stoppedValueLimsup_le_one, isEVar_stoppedValueLimsup → the same names. Main also adds setLIntegral_limsup_le, lintegral_limsup_le, lintegral_limsup_le_one and lintegral_stoppedValueLimsup_le.
• private coe_add_one_le_of_coe_lt → Mathlib's ENat.natCast_add_one_le_iff (as used by feat: convergence and optional stopping of ℝ≥0∞-valued supermartingales at stopping times in WithTop ℕ #395)

LMLExplore/EValues/TestSupermartingale.lean:

• IsTestSupermartingale.lintegral_zero_ne_top, together with its three in-file uses → already on main, with the same name and the same statement.

What is left, and why I am not keeping it

• IsENNSupermartingale.setLIntegral_stoppedProcess_le (and its private one-step lemma). This was this PR's route to the bounded case. On main, the public setLIntegral_stoppedValueLimsup_le_of_le_const does that job, through the times max σ (min τ k). No LMLRoadmaps target asks for optional stopping stated with stoppedProcess. Kept on its own, it would be a second idiom for the truncated value next to main's stoppedValueLimsup M (min τ N). If a later target needs it, it is a short corollary of main's bounded case.
• MeasureTheory.isStoppingTime_top. Main proves this fact inline once, as fun _ ↦ by simp, in setLIntegral_limsup_le. Factoring it out is a one-line refactor and would be its own PR. It is not enough to justify keeping this one open.

The branch is left in place. No commit was pushed.