[RemyDegenne]

This PR adds the discrete-time Snell envelope of an ℝ≥0∞-valued process, with the properties that EValues Layer 3, item 1 ("Definition and characterization"), asks of it in its "Snell envelope" bullet. It adds two new files, LMLExplore/Probability/Martingale/SnellEnvelope.lean (298 lines) and LMLExplore/MeasureTheory/Function/ConditionalLExpectation.lean (78 lines), and edits two existing files:

• LMLExplore/Probability/Process/StoppedValue.lean gains the public lemma MeasureTheory.lintegral_stoppedValueLimsup_le_sum (at a random time bounded by N, the integral of an ℝ≥0∞-valued process is at most the sum of its integrals at the times up to N) and the import Mathlib.MeasureTheory.Integral.Lebesgue.Add for lintegral_finsetSum'. It is the finite-expectation step of snellEnvelope_ae_eq_essSupFamily_condExp, and belongs next to the other stoppedValueLimsup lemmas.
• LMLExplore/EValues/CondEVariable.lean: isCondEVar_iff_condLExp_le (statement unchanged) is re-proved with the new condLExp_ae_le_iff_forall_setLIntegral_le, removing the copy of that lemma's argument which its proof contained, and the file imports the new LMLExplore.MeasureTheory.Function.ConditionalLExpectation.

ProbabilityTheory.snellEnvelope E ℱ P n is the essential supremum under P (LMLExplore's MeasureTheory.essSupFamily, merged in #400) over the stopping times τ : Ω → ℕ with n ≤ τ and τ ≤ N for some constant N. The supremum is taken of the conditional expectations P⁻[fun ω ↦ E (τ ω) ω|ℱ n].

Departure from the roadmap's wording. The roadmap asks for the essential supremum of Mathlib's condExp (ℱ n) P of the real values (E τ).toReal, under ⨆ τ, ∫⁻ E τ ∂P < ∞. The definition here instead uses Mathlib's conditional Lebesgue expectation condLExp (P⁻[X|m], available at the pinned Mathlib). It needs no integrability, so the envelope is a supermartingale for every process. snellEnvelope_ae_eq_essSupFamily_condExp proves that it agrees almost surely with the roadmap's real-valued form as soon as each E n is measurable with finite expectation, a hypothesis that the roadmap's implies. The proof goes through Mathlib's toReal_condLExp. The roadmap's probability measure is weakened to Mathlib's [SigmaFiniteFiltration P ℱ].

Main declarations (ProbabilityTheory):

• The index family boundedStoppingTimesFrom ℱ n of stopping times τ with n ≤ τ ≤ N for some constant N, with mem_boundedStoppingTimesFrom_iff (@[simp]), const_mem_boundedStoppingTimesFrom, boundedStoppingTimesFrom_anti and piecewise_mem_boundedStoppingTimesFrom.
• snellEnvelope, snellEnvelope_def (proved by (rfl); the body is not exposed), adapted_snellEnvelope (holds for every process).
• The characterization as a least function: condLExp_ae_le_snellEnvelope, snellEnvelope_ae_le, snellEnvelope_ae_le_iff.
• Domination: ae_le_snellEnvelope, E n ≤ᵐ[P] snellEnvelope E ℱ P n for an adapted E.
• setLIntegral_snellEnvelope: the integral of the envelope over an ℱ n-measurable s is ⨆ of ∫⁻ ω in s, E (τ ω) ω ∂P over the bounded stopping times τ ≥ n. lintegral_snellEnvelope_zero gives ∫⁻ L 0 ∂P = ⨆ τ, ∫⁻ E τ ∂P over the bounded stopping times.
• isENNSupermartingale_snellEnvelope: it is an IsENNSupermartingale for {P} (Layer 2.1), for every process.
• IsENNSupermartingale.snellEnvelope_ae_le: it is below every ℝ≥0∞-valued supermartingale for {P} that dominates E almost surely at every time. The proof uses the existing bounded optional stopping IsENNSupermartingale.setLIntegral_stoppedValueLimsup_le_of_le_const.
• isTestSupermartingale_snellEnvelope: if the expectations at bounded stopping times are at most 1, it is an IsTestSupermartingale for {P}.
• snellEnvelope_ae_eq_essSupFamily_condExp: the comparison with the real condExp form described above, for a process of measurable functions with finite expectations.

General lemmas (MeasureTheory, in LMLExplore/MeasureTheory/Function/ConditionalLExpectation.lean, which mirrors Mathlib's Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean). Neither exists in Mathlib, Tau Ceti, Statlib or LML; I grepped for condLExp together with piecewise, indicator, ≤ᵐ and ae_le.

• condLExp_piecewise: P⁻[s.piecewise X Y|m] =ᵐ[P] s.piecewise P⁻[X|m] P⁻[Y|m] for an m-measurable s, with no measurability or integrability of X and Y. This is the pasting step that makes the family of conditional expectations directed upward.
• condLExp_ae_le_iff_forall_setLIntegral_le: P⁻[X|m] ≤ᵐ[P] Y for an m-measurable Y exactly when ∫⁻ ω in s, X ω ∂P ≤ ∫⁻ ω in s, Y ω ∂P for every m-measurable s.

How the proof works. Pasting two bounded stopping times τ₁, τ₂ ≥ n along the ℱ n-measurable set where the first conditional expectation is the larger gives another such stopping time (Mathlib's IsStoppingTime.piecewise_of_le). Its conditional expectation is the maximum of the two (condLExp_piecewise), so the family is directed upward. setLIntegral_essSupFamily_of_directed then computes the set integrals of the envelope. The supermartingale inequality follows because the stopping times after n + 1 are among those after n. Sources, credited in the module docstring: Föllmer and Schied, Stochastic Finance, 4th ed., Chapter 6 (the essential-supremum description of the Snell envelope), and Ramdas, Ruf, Larsson and Koolen, arXiv:2009.03167v3, Lemma 6 and Appendix A (its use for e-processes).

Consumer milestone: EValues Layer 3, item 1, the bullet "[RRLK, Lemma 6]". Its implication from validity at bounded stopping times to "for each P ∈ S, E is P-almost surely dominated by a test supermartingale for P" is isTestSupermartingale_snellEnvelope together with ae_le_snellEnvelope. What remains after this PR in Layer 3, item 1 is the [RRLK, Lemma 6] equivalence itself, including the step to a test martingale through martingalePart. That step is stated with IsEProcess, which has since landed on main in #401, and is left to a follow-up pull request so that this one stays on the Snell envelope. This PR shares no declarations with #401 (merged), #399 or any other open pull request.

This PR removes or renames no public declaration.

Verification: local checks only, not CI (tauceti-local-checks verify --policy ordinary, EXIT 0). It reported scope: scoped: against 4581f34e5bbf909a83ac7ef36ff5da465f7784dd and local-axioms: checked 4 changed module(s), 78 declaration(s); 0 violation(s). The whole-library lake build --iofail, module-system, header-style and changed-module environment lint all passed.

Roadmap: EValues

🤖 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	The Snell envelope definition and every new statement match the roadmap's domination, minimality and time-0 identity, and the move to condLExp is bridged by snellEnvelope_ae_eq_essSupFamily_condExp under hypotheses the roadmap's imply. The helper lemmas (condLExp_piecewise, condLExp_ae_le_iff_forall_setLIntegral_le, lintegral_stoppedValueLimsup_le_sum) are correctly stated and not vacuous.
✅	reuse	approved	claude/claude-opus-5-5	The new condLExp_piecewise, condLExp_ae_le_iff_forall_setLIntegral_le, lintegral_stoppedValueLimsup_le_sum and the Snell envelope API have no counterpart in Mathlib (ConditionalLExpectation.lean has no piecewise, indicator or comparison lemma) or in LMLExplore. The proofs reuse essSupFamily, setLIntegral_essSupFamily_of_directed, IsStoppingTime.piecewise_of_le, toReal_condLExp and the existing optional stopping, and the CondEVariable edit removes a duplicated argument.
✅	scope	approved	claude/claude-opus-5-5	New material implements the 'Snell envelope' bullet of EValues Layer 3.1 (roadmap README.md:539-544), and the supporting lemmas and the CondEVariable re-proof are direct prerequisites or deduplication of the extracted lemma, so the PR is one topic.
✅	attribution	approved	claude/claude-opus-5-5	The Snell envelope module credits Föllmer–Schied (Stochastic Finance, Ch. 6) and Ramdas–Ruf–Larsson–Koolen (arXiv:2009.03167v3, Lemma 6, App. A), its central informal sources; no prior formalization exists in Mathlib or the repo to credit, and the two conditional-expectation lemmas are routine. The roadmap is credited only in the PR description, as required.
✅	api-design	approved	claude/claude-opus-5-5	The surface is minimal with hidden bodies (snellEnvelope_def by (rfl)), and the characterizing API (membership, least-function, domination, set-integral, supermartingale, minimality) covers the roadmap's Snell envelope bullet. The general condLExp lemmas are public in their canonical MeasureTheory home, and the only private helper is specific to this file.
✅	generality	approved	claude/claude-opus-5-5	The new statements sit at the natural level: the condLExp lemmas need no measurability or integrability of X and Y, the envelope is a supermartingale for every process, and SigmaFiniteFiltration is the minimal standard hypothesis for the trims used. The CondEVariable re-proof removes an earlier special-case copy of the general comparison lemma rather than adding a duplicate.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration sits in its natural home: the generic condLExp lemmas in a file at Mathlib's matching path, the Snell envelope beside optional stopping, and the stopped-value bound with its siblings. No import is unused or too broad.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in standard Mathlib terminology, and suffixes such as _iff, _eq, _def and _anti match what each statement proves. No notation is introduced and namespaces are appropriate.
✅	documentation	approved	claude/claude-opus-5-5	Both new files have module docstrings that state their content and mathematical purpose, with references, and every public declaration has a docstring that matches its statement without overclaiming. The new StoppedValue lemma is documented and added to that file's main-statements list.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and robust, with no undocumented change/show or reliance on accidental definitional equality; coercion steps between WithTop ℕ and ℕ go through explicit lemmas. The shared comparison argument is factored into condLExp_ae_le_iff_forall_setLIntegral_le and reused, including in the re-proof of isCondEVar_iff_condLExp_le.

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

_{Reviewing this diff at head 8a1802b. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.17.}

[RemyDegenne]

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

Docstrings are present and mostly accurate, but the SnellEnvelope module docstring still overstates snellEnvelope_ae_eq_essSupFamily_condExp by dropping its measurability hypothesis.

• LMLExplore/Probability/Martingale/SnellEnvelope.lean:25 — Module docstring says the envelope agrees a.s. with the real condExp form 'when the values of the process have finite expectations', but the theorem also requires hE : ∀ n, Measurable (E n); the claim overstates the statement. Fix: Reword to 'When the values of the process are measurable with finite expectations, ...', matching the theorem docstring at line 268.

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 · 15s · 57.2k in (51k cache read, 6.2k cache write) / 1.4k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}