[RemyDegenne]

This pull request adds e-processes, with the API that makes the definition usable and needs none of the later parts of the target. It adds one new file, LMLExplore/EValues/EProcess.lean, and one general lemma to LMLExplore/Probability/Process/StoppedValue.lean.

The definition

ProbabilityTheory.IsEProcess E ℱ S, for E : ℕ → Ω → ℝ≥0∞, ℱ : Filtration ℕ mΩ and S : Set (Measure Ω), is a structure with two fields:

• adapted : Adapted ℱ E;
• isEVar_stoppedValue: for every τ : Ω → ℕ with IsStoppingTime ℱ (fun ω ↦ (τ ω : WithTop ℕ)), the function fun ω ↦ E (τ ω) ω is an e-variable for S (Statlib's IsEVar).

This is [RW, Definition 7.3 (ii)], in the form the roadmap gives. The null is an arbitrary set of measures and the filtration is arbitrary.

Main declarations

• IsEProcess.measurable and IsEProcess.isEVar: each value E n is measurable, and at every fixed time it is an e-variable.
• IsEProcess.lintegral_le_one: for every probability measure P in the null, ∫⁻ ω, E (τ ω) ω ∂P ≤ 1 at every stopping time τ with values in ℕ.
• IsEProcess.of_lintegral_le_one and isEProcess_iff_lintegral_le_one: for a null of probability measures, IsEProcess E ℱ S ↔ Adapted ℱ E ∧ ∀ τ, IsStoppingTime ℱ τ → ∀ P ∈ S, ∫⁻ ω, E (τ ω) ω ∂P ≤ 1, the counterpart of isEVar_iff_lintegral_le_one.
• IsEProcess.measurable_stoppedValue: the value of an e-process at a stopping time with values in ℕ is measurable.
• IsEProcess.anti_set: an e-process for T is an e-process for every subset of T.
• isEProcess_iff_forall_singleton: IsEProcess E ℱ S ↔ Adapted ℱ E ∧ ∀ P ∈ S, IsEProcess E ℱ {P}. The adaptedness part matters only when S is empty.
• IsEProcess.mono_ae and IsEProcess.mono, for a null of finite measures: an adapted process F is an e-process if it is dominated by an e-process, either almost surely at every time (∀ P ∈ S, ∀ n, F n ≤ᵐ[P] E n) or pointwise (F ≤ E).
• isEProcess_one: the constant process 1 is an e-process for every null and every filtration.
• convex_isEProcess: the e-processes for a null form a convex set, Convex ℝ≥0∞ {E | IsEProcess E ℱ S}. This is the counterpart of Statlib's convex_isEVar.
• MeasureTheory.measurable_apply_of_countable (in StoppedValue.lean): for a countable index type ι with measurable singletons, fun ω ↦ u (σ ω) ω is measurable when every u i and σ are measurable.
• MeasureTheory.Adapted.measurable_apply_stoppingTime (in StoppedValue.lean): the value fun ω ↦ u (σ ω) ω of an adapted process at a stopping time with values in ℕ is measurable.
• IsTestSupermartingale.isEProcess: a test supermartingale for a null of probability measures is an e-process. The proof uses the optional stopping already in LMLExplore (IsTestSupermartingale.isEVar_stoppedValueLimsup, stoppedValueLimsup_natCast); it cites [RW, Fact 7.5].

Roadmap coverage (EValues, Layer 3)

Covered:

• Item 1, first bullet: the definition IsEProcess E ℱ S.
• Item 2, the closure properties that need nothing from item 1:
  • an e-process for S exactly when it is one for each {P};
  • adapted processes dominated almost surely by an e-process;
  • convex combinations;
  • every test supermartingale for the members of S is an e-process.

Left for later pull requests:

• Item 1:
  • the essential supremum of a family, which is the subject of the open feat: the essential supremum of a family of ℝ≥0∞-valued functions #400;
  • the Snell envelope;
  • the equivalences of [RRLK, Lemma 6]: validity at bounded stopping times, validity at all stopping times with stoppedValueLimsup or with the liminf convention, and domination by a test supermartingale or a test martingale.
• Item 2:
  • Ville's inequality for e-processes, which comes from the domination of item 1 and the open feat: the exact Ville identity, the extended Ville inequality and Ville's inequality in ℝ≥0∞ #399;
  • mixtures over measurable families;
  • mixtures of members of the null and the effective null;
  • minima of an e-process for S and one for T;
  • time-mixtures and optional continuation;
  • the counterexamples.
• Items 3 to 7.

This pull request shares no content with the open #399 and #400.

Notes for reviewers

• Measurability of fun ω ↦ E (τ ω) ω comes from the new public MeasureTheory.Adapted.measurable_apply_stoppingTime, built on MeasureTheory.measurable_apply_of_countable, both next to measurable_stoppedValueLimsup.
• The domination lemmas assume ∀ P ∈ S, IsFiniteMeasure P, as Statlib's IsEVar.mono does, because Statlib's IsEVar excludes ∫ᵉ (X - 1) = ⊥. IsTestSupermartingale.isEProcess assumes probability measures, because a test supermartingale only bounds expectations by 1.
• The definition and its closure properties are adapted from EValuesResearch/ForLMLExplore/EValues/EProcess.lean (commit d2da7b7) in the paper project RemyDegenne/evalues_research, which is credited in the module docstring. The field name isEVar_stoppedValue comes from there too.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R6

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

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

The PR says its material and the field name isEVar_stoppedValue come from the paper project RemyDegenne/evalues_research, but the new file never credits that formalization; only [RW] is cited.

• LMLExplore/EValues/EProcess.lean:11 — The module docstring does not credit the paper project the definition, field name and proofs come from (RemyDegenne/evalues_research), which the PR description says outright. Fix: Add a sentence to the module docstring, following repo practice, e.g. 'The definition and statements are adapted from the formalization in the paper project RemyDegenne/evalues_research (same author).', with the specific file if known.

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 · 21s · 60.6k in (50.9k cache read, 9.6k cache write) / 1.6k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

The file and its imports are correctly placed, but a generic stopped-value measurability lemma is hidden as private in the e-values file instead of living with the stopped-value API.

• LMLExplore/EValues/EProcess.lean:76 — measurable_apply_of_isStoppingTime is a generic stochastic-process fact (an adapted process evaluated at an ℕ-valued stopping time is measurable) with no e-value content. It is hidden as private here instead of being placed in its canonical home. Fix: Move it, public, to LMLExplore/Probability/Process/StoppedValue.lean next to measurable_stoppedValueLimsup (e.g. as MeasureTheory.Adapted.measurable_apply_stoppingTime), and use it from there in mono_ae and isEProcess_iff_forall_singleton.

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 · 56s · 213.9k in (200.1k cache read, 13.7k cache write) / 3.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[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	IsEProcess matches the roadmap's suggested structure and [RW, Definition 7.3 (ii)] for stopping times with values in ℕ, which the docstring states, and IsTestSupermartingale.isEProcess gives it a real witness. Every closure lemma states the intended result, and its hypotheses (finite or probability measures, and the Adapted conjunct needed when S is empty) are what the claim needs.
✅	reuse	approved	claude/claude-opus-5-5	IsEProcess and its closure lemmas are new: none is in Mathlib or LMLExplore, and they reuse the IsEVar API and existing optional stopping instead of re-deriving them. The two measurability lemmas are general helpers built on measurable_from_prod_countable_left; neither Mathlib's measurable_stoppedValue (it needs a progressive process and a Borel codomain) nor measurable_stoppedValueLimsup (it needs an order and topology) replaces them.
✅	scope	approved	claude/claude-opus-5-5	Adds the IsEProcess definition specified in EValues Layer 3.1 (README.md:531-533) and closure properties listed in Layer 3.2 (README.md:554-561), with a directly used measurability prerequisite in StoppedValue.lean. Single coherent topic; no scope issues.
✅	attribution	approved	claude/claude-opus-5-5	The module docstring credits the informal source ([RW], Definition 7.3 (ii) and Fact 7.5) and the formalization it adapts (RemyDegenne/evalues_research, EProcess.lean at commit d2da7b7); the roadmap is credited only in the PR description. The new StoppedValue lemmas are routine measurability glue that draws on no particular source.
✅	api-design	approved	claude/claude-opus-5-5	The IsEProcess surface is minimal, has no compatibility artifacts, and now includes the probability-null introduction lemma and iff; the repeated stopped-value measurability term is now the public general lemma Adapted.measurable_apply_stoppingTime in StoppedValue.lean. Neither new general lemma duplicates Mathlib, because Mathlib's measurable_stoppedValue requires a pseudo-metrizable Borel codomain and a strongly progressive process.
✅	generality	approved	claude/claude-opus-5-5	Assumptions match those of the Statlib/LMLExplore lemmas they build on (finite measures for domination, as in IsEVar.mono; probability measures for isEVar_stoppedValueLimsup), and the measurability helper is proved at countable-index generality with the ℕ stopping-time form derived from it. No unused or too-strong hypotheses or special-case duplication found.
✅	placement	approved	claude/claude-opus-5-5	EProcess.lean joins the existing EValues/ directory with imports that are used and specific, and the two general measurability lemmas sit in Probability/Process/StoppedValue.lean next to measurable_stoppedValueLimsup, where they need nothing beyond that file's existing imports.
✅	naming	approved	claude/claude-opus-5-5	Names describe conclusions in standard terminology, consistent with the adjacent IsEVar API (anti_set, mono, mono_ae, convex_isEVar) and with Mathlib's stoppedValue, and dot-notation lemmas on Adapted sit in MeasureTheory.Adapted. No notation is introduced and the _iff names are genuine equivalences.
✅	documentation	approved	claude/claude-opus-5-5	The new module docstring and every public declaration's docstring accurately describe the definitions and statements, with mathematical references and no roadmap or process narrative. The two additions to StoppedValue.lean are documented accurately.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, robust term-mode or single-step automation with no change/show or undocumented defeq; the one simpa (IsTestSupermartingale.isEProcess) rests on the @[simp] lemma stoppedValueLimsup_natCast stating exactly the needed rewrite, and measurability reasoning is factored into the reusable Adapted.measurable_apply_stoppingTime.

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

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