[RemyDegenne]

This PR builds most of the EValues Layer 2.1 milestone, Conditional e-variables, test supermartingales and wealth [RW, Definitions 7.3(i) and 7.19, Propositions 7.9 and 7.20; GdHK24, Definition 1, Proposition 2; WSR24, Proposition 3; WSJ26; ShSVV11]. It adds the three process predicates of the roadmap, the bridges with Mathlib's real supermartingales, the wealth of portfolios with its special cases, and the converse factorization. Everything is in ℝ≥0∞, stated with set integrals, for any filtration and any null S : Set (Measure Ω), in the namespace ProbabilityTheory next to Statlib's IsEVar, as the roadmap's Conventions ask.

Roadmap: EValues

Here is how each item of Layer 2.1 is covered:

• IsCondEVar X m S (∫⁻ ω in s, X ω ∂P ≤ P s for every P ∈ S and m-measurable s) and its exact version IsExactCondEVar (= P s), in EValues/CondEVariable.lean. They come with:
  • the completion-check API anti_set, of_le (coarser σ-algebra) and congr;
  • the characterizations isCondEVar_iff_withDensity_trim_le and isExactCondEVar_iff_withDensity_trim_eq;
  • the bridges with Mathlib's ℝ≥0∞ conditional expectation condLExp, when the restrictions P.trim hm are σ-finite: isCondEVar_iff_condLExp_le (P⁻[X|m] ≤ᵐ[P] 1) and isExactCondEVar_iff_condLExp_eq (P⁻[X|m] =ᵐ[P] 1). The set-integral definition is kept because it needs no σ-finiteness;
  • isCondEVar_bot_iff: given ⊥, these are exactly Statlib's e-variables; IsCondEVar.isEVar;
  • pulling out a known factor: IsCondEVar.lintegral_mul_le, setLIntegral_mul_le and the exact …_mul_eq versions;
  • isCondEVar_one and isExactCondEVar_one;
  • portfolios isCondEVar_sum_mul (weights summing to at most 1) and isExactCondEVar_sum_mul (summing to 1).
• IsENNSupermartingale M ℱ S, IsTestSupermartingale M ℱ S (which extends it with ∫⁻ M 0 ∂P ≤ 1) and IsTestMartingale M ℱ S, with the field shapes of Suggested.lean. Adaptedness is Mathlib's Adapted ℱ M. These live in EValues/TestSupermartingale.lean, with measurable, anti_set and congr for each, plus:
  • setLIntegral_le and lintegral_le (monotonicity across any i ≤ j), and for test martingales setLIntegral_eq and lintegral_eq;
  • for test supermartingales, lintegral_le_one and isEVar (every M n is an e-variable);
  • IsTestMartingale.isTestSupermartingale and isTestMartingale_one (the completion check "the constant process 1 is a test martingale").
• Bridges:
  • Supermartingale.isTestSupermartingale_ofReal: a real nonnegative supermartingale with ∫ M 0 ≤ 1 gives a test supermartingale for {P} through ENNReal.ofReal.
  • IsTestSupermartingale.ae_lt_top: a test supermartingale is almost surely finite at every time.
  • IsTestSupermartingale.supermartingale_toReal: its toReal is a real supermartingale. This goes through the existing LMLExplore.supermartingale_of_setLIntegral_succ_le, as the roadmap prescribes.
  • The IsENNSupermartingale versions of the last two assume only ∫⁻ M 0 ∂P ≠ ∞.
• Wealth of portfolios:
  • isTestSupermartingale_mul_prod and isTestMartingale_mul_prod: M₀ * ∏ k < n, F k for an ℱ 0-measurable M₀ with ∫⁻ M₀ ≤ 1 and ℱ (k + 1)-measurable (exact) conditional e-variables F k.
  • isTestSupermartingale_portfolio and isTestMartingale_portfolio [WSJ26]: the Suggested.lean statement, with a general initial M₀. For the supermartingale version the weights need only sum to at most 1.
  • Derived from these as the roadmap asks: the products of sequential e-variables isTestSupermartingale_prod and isTestMartingale_prod [RW, Proposition 7.20; GdHK24, Proposition 2] (one coordinate), and betting ∏ (1 - c k + c k * E k) with c k ≤ 1, isTestSupermartingale_betting_condEVar and isTestMartingale_betting_condEVar [RW, Definition 7.21]. The _condEVar suffix leaves the name isTestSupermartingale_betting free for the Layer 4.4 theorem on betting against conditional constraints (two coordinates, one of which is 1).
• The converse [WSR24, Proposition 3]:
  • IsENNSupermartingale.isCondEVar_div: the ratios M (k + 1) / M k are conditional e-variables. No hypothesis is needed, because x / ∞ = 0 and (M k)⁻¹ * M k ≤ 1.
  • IsENNSupermartingale.ae_eq_mul_prod_div and IsTestSupermartingale.ae_eq_mul_prod_div: almost surely, M n = M 0 * ∏ k < n, M (k + 1) / M k, with 0 / 0 = 0.

One general measure-theory tool goes in its own file, MeasureTheory/Measure/WithDensity.lean, next to Mathlib's trim_withDensity. It is lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le: if the set integrals of f are at most those of g over the m-measurable sets, then ∫⁻ Y * f ≤ ∫⁻ Y * g for every m-measurable Y : Ω → ℝ≥0∞. Its equality version, the two characterizations withDensity_trim_{le,eq}_withDensity_trim_iff behind them, and lintegral_mul_eq_lintegral_trim_withDensity come with it. This is the ℝ≥0∞ "pull out what is known" step with no integrability. It is used for conditional e-variables (g = 1) and for the supermartingale ratios (f = M (k + 1), g = M k). The existing LMLExplore.lintegral_mul_ofReal_le_of_condExp_le (MeasureTheory/Function/ConditionalExpectation/LebesgueBochner.lean) proved the same pull-out step by its own Measurable.ennreal_induction. As the reuse review asked, it is now derived from the new lemma, and the induction is deleted. Its statement does not change, so its two callers are untouched.

Before writing, I checked for duplicates. I searched the pinned Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for conditional e-variables, ℝ≥0∞-valued or test (super)martingales (TestMartingale, CondEVar, ENNSupermartingale), wealth and product processes, and the pulling-out lemma (forall_setLIntegral, withDensity/trim comparisons). None of these exist. Mathlib has trim_withDensity, the conditional expectation condLExp of ℝ≥0∞-valued variables (bridged to above) and ae_le_of_forall_setLIntegral_le_of_sigmaFinite (the converse direction), and these are not restated. The proofs reuse Mathlib's lintegral_trim, lintegral_withDensity_eq_lintegral_mul₀, Measure.le_iff, Supermartingale.setIntegral_le and ofReal_integral_eq_lintegral_ofReal, and LMLExplore's supermartingale_of_setLIntegral_succ_le. No proof is longer than 30 lines. The adaptedness of the wealth M₀ * ∏ k < n, F k is the public MeasureTheory.adapted_mul_prod_range, for any commutative monoid with measurable multiplication, in its own file Probability/Process/Adapted.lean, next to Mathlib's Adapted. No public declaration is removed or renamed.

This PR does not depend on the open Layer 0.1 PR #384: it uses only Statlib's IsEVar, and the two touch disjoint files.

Milestone: EValues Layer 2.1. After this PR, what remains of Layer 2.1 is the last bullet: mixtures ∫⁻ θ, M θ n ω ∂π of test supermartingales, minima of two test supermartingales, stopped processes and optional continuation [RW, Proposition 7.9]. Layer 2.2 (convergence and optional stopping) and Layer 3 (e-processes) consume the predicates defined here.

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

• scope: scoped: against c4a9e04dde775bf5a60d932b093c88ab01b9246a
• Whole-library lake build --iofail succeeded (8579 jobs).
• local-axioms: checked 5 changed module(s), 109 declaration(s); 0 violation(s)
• The module-system, header-style and local-lint checks passed.

🤖 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 definitions match the roadmap's Suggested.lean, and the conditional e-variable, wealth, portfolio, betting and ratio-factorization statements state the cited results faithfully, in places more generally. I tried the edge cases (0/0, x/∞, x/0 on null sets, infinite set integrals, non-probability nulls) and could not break any statement.
✅	reuse	approved	claude/claude-opus-5-5	Both earlier reuse findings are fixed: the old pull-out lemma is now derived from the new withDensity/trim lemma, and IsCondEVar is bridged to Mathlib's condLExp using Mathlib's own lemmas. Searches of Mathlib and LMLExplore found no existing version of the new predicates, trim comparisons, adapted-product lemma or wealth constructions.
✅	scope	approved	claude/claude-opus-5-5	The PR implements EValues Layer 2.1 (roadmap README.md:469-491) as one unit: the conditional e-variable and ℝ≥0∞ supermartingale predicates, the Supermartingale bridges, the portfolio/product/betting wealth processes and the WSR24 converse, with the mixtures/minima/stopping bullet (README.md:492-495) left for later. The WithDensity pulling-out lemma and adapted_mul_prod_range are direct prerequisites, and re-deriving lintegral_mul_ofReal_le_of_condExp_le from the new lemma removes a duplicated proof rather than adding a second topic.
✅	attribution	approved	claude/claude-opus-5-5	The central sources (RW, GdHK24, ShSVV11, WSR24, WSJ26) are cited at the definitions and theorems that use them, and their entries match the roadmap bibliography. The code does not mention the roadmap, and the withDensity/trim and adapted-product helpers are routine and need no credit.
✅	api-design	approved	claude/claude-opus-5-5	The public surface covers the Layer 2.1 predicates with constructors and projections, monotonicity, congruence, the withDensity/trim and condLExp characterizations, and the @[simp] constant-1 lemmas. General infrastructure is public in its proper files, and nothing survives only for compatibility.
✅	generality	approved	claude/claude-opus-5-5	General wealth lemmas isTestSupermartingale_mul_prod/isTestMartingale_mul_prod and the generic pull-out lemma are proved once and portfolios, products, betting and the old lintegral_mul_ofReal_le_of_condExp_le are derived from them; remaining assumptions (SigmaFiniteFiltration, IsFiniteMeasure, IsProbabilityMeasure, c k ≤ 1) are each required by the cited lemmas or truncated subtraction.
✅	placement	approved	claude/claude-opus-5-5	Roadmap material sits in LMLExplore/EValues/, the home README.md:49 of the EValues roadmap names, and the generic withDensity/trim pull-out lemmas and adapted_mul_prod_range sit in files mirroring their Mathlib homes. Every new import is used and none is broad.
✅	naming	approved	claude/claude-opus-5-5	The betting pair is renamed isTestSupermartingale_betting_condEVar and isTestMartingale_betting_condEVar, so isTestSupermartingale_betting is free for the Layer 4.4 theorem (roadmap Suggested.lean:303). The other names describe their conclusions, match the roadmap's Suggested.lean, put the Supermartingale result under Mathlib's MeasureTheory.Supermartingale namespace, and the PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	Every new file has an accurate module docstring, and every public definition and main theorem is documented in line with its hypotheses, with no overclaims or process narrative. The rewritten LebesgueBochner proof leaves that file's module docstring accurate, since it describes only the statement.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and all go through one shared pull-out lemma, with no long rewrite chains, no change/show and no undocumented definitional-equality tricks. The products and betting results come from the portfolio lemma, and the two longest proofs have comments explaining their structure.

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

_{Reviewing this diff at head 64cf215. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $5.81.}