[RemyDegenne]

This PR completes the EValues Layer 2.1 milestone, Conditional e-variables, test supermartingales and wealth, with its last bullet: mixtures of a measurable family of test supermartingales over a probability measure, minima of two test supermartingales, stopped processes, and optional continuation [RW, Proposition 7.9]. It extends EValues/TestSupermartingale.lean (merged in #385) and keeps its conventions: ℝ≥0∞ values, set integrals, any filtration indexed by ℕ, any null S : Set (Measure Ω), and the namespace ProbabilityTheory.

Roadmap: EValues

The new declarations:

• Pulling a known factor out of one step. For ℱ n-measurable Y and s:
  • IsENNSupermartingale.setLIntegral_mul_succ_le: ∫⁻ ω in s, Y ω * M (n + 1) ω ∂P ≤ ∫⁻ ω in s, Y ω * M n ω ∂P.
  • It is a one-line use of MeasureTheory.setLIntegral_mul_le_setLIntegral_mul_of_forall_setLIntegral_le, added to MeasureTheory/Measure/WithDensity.lean with its twin …setLIntegral_mul_eq_setLIntegral_mul_of_forall_setLIntegral_eq. They are the set-integral forms of the existing lintegral_mul_{le,eq}_lintegral_mul_of_forall_setLIntegral_{le,eq}, for any sub-σ-algebra m, m-measurable Y and s, and a.e.-measurable densities. The _eq lemma gives the martingale step of IsTestMartingale.stoppedProcess_mul directly.
• Minima:
  • IsENNSupermartingale.inf: IsENNSupermartingale (M ⊓ N), named after Mathlib's Submartingale.sup.
  • IsTestSupermartingale.inf: the minimum of a test supermartingale and any ℝ≥0∞-valued supermartingale is a test supermartingale, so in particular the minimum of two test supermartingales is one.
• Optional continuation [RW, Proposition 7.9]. Take a stopping time τ : Ω → WithTop ℕ and a process B with B n = 1 whenever n ≤ τ. Then stoppedProcess A τ * B is:
  • an ℝ≥0∞-supermartingale (IsENNSupermartingale.stoppedProcess_mul);
  • a test supermartingale when A is one and B is only an ℝ≥0∞-valued supermartingale (IsTestSupermartingale.stoppedProcess_mul);
  • a test martingale when A is one and B is only adapted with martingale steps under every P ∈ S (IsTestMartingale.stoppedProcess_mul). Asking for IsTestMartingale B would force P univ ≤ 1, since B 0 = 1.
  • The proof splits each step at the ℱ n-measurable event {τ ≤ n}, as [RW] does. A single private lemma handles that split for both the supermartingale and the martingale versions.
• Stopped processes:
  • IsENNSupermartingale.stoppedProcess, IsTestSupermartingale.stoppedProcess, IsTestMartingale.stoppedProcess.
  • All three are derived from optional continuation with B = 1.
• Mixtures (Tonelli in ℝ≥0∞, no integrability hypothesis):
  • isENNSupermartingale_lintegral (any s-finite π), isTestSupermartingale_lintegral and isTestMartingale_lintegral (probability π).
  • They apply to a family M : Θ → ℕ → Ω → ℝ≥0∞ with (θ, ω) ↦ M θ n ω measurable for mΘ.prod (ℱ n), under every s-finite member of the null.
  • Tonelli needs that s-finiteness; it can fail for measures that are not s-finite.
• MeasureTheory.Adapted.stoppedProcess_of_discrete, in Probability/Process/Stopping.lean. It is the measurable (Adapted) form of Mathlib's StronglyAdapted.stoppedProcess_of_discrete, for second-countable pseudo-metrizable Borel value spaces. It goes through Adapted.stronglyAdapted.
• MeasureTheory.adapted_lintegral, in Probability/Process/Adapted.lean: the mixture i ↦ ∫⁻ θ, M θ i · ∂π over an s-finite π is adapted, for a filtration indexed by any preorder, when (θ, ω) ↦ M θ i ω is measurable for mΘ.prod (f i). That file now also imports Mathlib.MeasureTheory.Measure.Prod.

Reuse: I searched the pinned Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for stopped, minimum and mixture closure of ℝ≥0∞-valued supermartingales, and for an Adapted (non-strong) stopped-process lemma. None exist. Mathlib's Submartingale.stoppedProcess and Supermartingale API are real-valued and need integrability. Tau Ceti's stoppedProcess_bot covers the time-0 value. I use Mathlib's conditional stoppedProcess_eq_of_le in simp instead, which needs no ⊥ = 0 conversion; an earlier private copy of that fact was dropped. The proofs use Mathlib's lintegral_inter_add_sdiff, setLIntegral_congr_fun, lintegral_lintegral_swap, Measurable.lintegral_prod_left', MeasurableSpace.prod_mono and stoppedProcess_eq_of_le / _of_ge. No proof is longer than 25 lines. No public declaration is removed or renamed.

Milestone: EValues Layer 2.1. With this PR every bullet of Layer 2.1 is covered. Layer 2.2 (convergence and optional stopping in ℝ≥0∞ at stopping times in WithTop ℕ) comes next: it needs the stopped processes added here for its bounded-time step. The closure properties of e-processes in Layer 3.2 (minima, mixtures over measurable families, optional continuation) need the mixtures, minima and optional continuation, through the domination of e-processes by test supermartingales.

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

• scope: scoped: against c6fc99ce9e747a4f7bdc32e73152e58a20048a09
• Whole-library lake build --iofail succeeded (8589 jobs).
• local-axioms: checked 4 changed module(s), 89 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	Optional continuation, stopped processes, minima and mixtures are stated faithfully to [RW, Prop. 7.9] and the existing IsENNSupermartingale/IsTest(Super)martingale definitions; the hypotheses (B = 1 up to and including τ, an s-finite null for Tonelli, joint measurability) are honest and non-vacuous.
✅	reuse	approved	claude/claude-opus-5-5	New ℝ≥0∞ closure results (minima, stopping, optional continuation, mixtures) have no counterpart in Mathlib or LMLExplore and are built on located Mathlib and LMLExplore lemmas (StronglyAdapted.stoppedProcess_of_discrete, lintegral_lintegral_swap, Measurable.lintegral_prod_left', the existing lintegral_mul_*_of_forall_setLIntegral_*); Tau Ceti, LML and Statlib sources were not available to grep.
✅	scope	approved	claude/claude-opus-5-5	The PR implements exactly the final bullet of EValues Layer 2.1 (README.md:492-495): mixtures, minima, stopped processes and optional continuation [RW, Prop. 7.9]. Its helper lemmas in WithDensity, Stopping and Adapted are each used directly by those theorems, so it is a single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The central informal source, [RW, Proposition 7.9] for optional continuation, is cited in the module docstring, the theorem docstrings and the References section, and the Mathlib lemma the measurable stopped-process lemma adapts is named in its docstring. The remaining closure results are routine and need no further credit.
✅	api-design	approved	claude/claude-opus-5-5	The general results (setLIntegral_mul_{le,eq}_…, adapted_lintegral, Adapted.stoppedProcess_of_discrete) are public in their own infrastructure files and do not duplicate Mathlib, and the private helpers are proof-specific or thin wrappers. The PR adds no definitions that would need characteristic API, no simp or grind normal-form lemmas, and no compatibility artifacts.
✅	generality	approved	claude/claude-opus-5-5	The general results come first and the special cases follow from them: stopped processes are optional continuation with B = 1, and the set-integral helper lemmas are reused for both the supermartingale and martingale steps. The hypotheses (s-finiteness for Tonelli, a supermartingale or martingale-step B, joint measurability for adaptedness) are what the proofs need, and the value-space assumptions in Adapted.stoppedProcess_of_discrete follow Mathlib's stronglyAdapted_iff_adapted convention.
✅	placement	approved	claude/claude-opus-5-5	Each new generic lemma is in its generic home (WithDensity, Process/Adapted, Process/Stopping), and only results about the EValues supermartingale predicates are in TestSupermartingale.lean; the existing Martingale/Mixture.lean covers the real-valued Mathlib predicate and is not a better home. Both added imports are used and specific.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard Mathlib terminology, consistent with adjacent declarations (supermartingale_integral, StronglyAdapted.stoppedProcess_of_discrete, lintegral_mul_{le,eq}_…); _le/_eq suffixes match statement strength and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Both prior findings are resolved: the module overview, Main statements entry and mixture docstrings now state the s-finite-null condition, and the unsupported e-process transfer claim is removed. All new public declarations and the updated module docstrings are documented accurately without overclaiming.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and well factored: the shared step split is one private lemma, the stopped-process corollaries specialise optional continuation, and the single explicit-instance term is commented. No brittle rewrite chains or undocumented defeq reliance.

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

_{Reviewing this diff at head 09f5d33. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.43.}