[RemyDegenne]

This pull request answers the question of [RGVS23, §8.2.4] on whether the numeraires of the n-sample nulls, as a process, form an e-process for the i.i.d. null. In general they do not. For the null {Ber(1/5), Ber(4/5)} and the alternative Ber(1/2), a stopping time with values in {0, 1} gives them the mean 367 / 340 under the i.i.d. law of Ber(1/5), and half of the process is an e-process. For a null {P₁, P₂} on a finite space, with Q₁, P₁ and P₂ charging every point, they form an e-process exactly when E_{Q₁}[p₂ / p₁] ≤ 1 or E_{Q₁}[p₁ / p₂] ≤ 1, which is also exactly when they are products. It adds one new file, LMLExplore/EValues/Numeraire/Sequential.lean (1176 lines), and changes no existing file.

Main declarations

All statements are in ProbabilityTheory. They take any family X : (n : ℕ) → (Fin (n + 1) → α) → ℝ≥0∞ with IsNumeraire (X n) ((fun P ↦ Measure.pi fun _ : Fin (n + 1) ↦ P) '' S₁) (Measure.pi fun _ ↦ Q₁) for every n: X n is a numeraire (Statlib's) of n + 1 observations. The process is fun n ω ↦ X n fun i ↦ ω i on ℕ → α, with Filtration.piLE, so its time n has seen n + 1 observations. The null of the e-process is (fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁.

• lintegral_numeraires_bernoulli_stop_eq: for S₁ = {Ber(true, false, 1/5), Ber(true, false, 4/5)} and Q₁ = Ber(true, false, 1/2) on Bool, fun ω ↦ if ω 0 then 1 else 0 is a stopping time for Filtration.piLE, and ∫⁻ ω, X (if ω 0 then 1 else 0) (fun i ↦ ω i) ∂(Ber(1/5))^ℕ = 367 / 340.
• not_isEProcess_numeraires_bernoulli: in the same setting, ¬ IsEProcess (fun n ω ↦ X n fun i ↦ ω i) ….
• isEProcess_half_numeraires_bernoulli: in the same setting, IsEProcess (fun n ω ↦ 2⁻¹ * X n fun i ↦ ω i) ….
• isEProcess_numeraires_pair_iff: for [MeasurableSingletonClass α] [Finite α], probability measures Q₁, P₁, P₂ charging every point (∀ x, Q₁ {x} ≠ 0, …) and S₁ = {P₁, P₂}, the process is an e-process iff ∫⁻ x, P₂ {x} / P₁ {x} ∂Q₁ ≤ 1 ∨ ∫⁻ x, P₁ {x} / P₂ {x} ∂Q₁ ≤ 1.
• exists_prod_eq_numeraires_pair_iff: under the same hypotheses, (∃ e : α → ℝ≥0∞, ∀ n x, X n x = ∏ i, e (x i)) iff the same condition.

Roadmap coverage (EValues, Layer 6, item 1)

Covered: the whole bullet "The numeraires of the n-sample nulls, as a process, are not an e-process in general, a question of [RGVS23, §8.2.4]…". That is the counterexample with its stopping time and the mean 367/340, half of the process being an e-process, and the criterion for two-point nulls on a finite space together with "that is, when they are products".

Left for other pull requests: the other bullets of item 1. This pull request does not touch them.

Notes for reviewers

• Which process. A numeraire is unique only Q₁ ^ (n + 1)-almost surely. Without full support, whether the process is an e-process can depend on the version. The statements therefore take every family of numeraires rather than a fixed one. Statlib's chosen version numeraire is one such family (isNumeraire_numeraire). Under the hypotheses, Q₁ ^ (n + 1) charges every point, so all versions agree everywhere (private eq_of_isNumeraire, from IsNumeraire.ae_unique). The numeraire of 0 observations is not part of the process.
• Proof of the two-point criterion. A likelihood ratio of Q₁ ^ n against a mixture w P₁ ^ n + (1 - w) P₂ ^ n with expectation at most 1 under both null products is the numeraire. This is checked through Statlib's isNumeraire_iff: the expectation under Q₁ ^ n of Y divided by this ratio is the expectation of Y under the mixture. If E_{Q₁}[p₂/p₁] ≤ 1, the weight w = 1 works for every n. The numeraires are then products of copies of the e-variable x ↦ Q₁ {x} / P₁ {x}, which form a test supermartingale (isTestSupermartingale_mul_prod) and hence an e-process (IsTestSupermartingale.isEProcess). If both expectations exceed 1, the intermediate value theorem gives an interior weight with both expectations equal to 1. Let k + 2 be the number of points of the space. The e-process property at the stopping times that stop at time k on one sample of k + 1 observations, and at time k + 1 otherwise, forces the mixtures of k + 1 and k + 2 observations to agree on the first k + 1 observations. It then forces the rational function s ↦ ∑ y, (p₁ y - p₂ y) q y / (p₁ y + s p₂ y) to vanish at k + 2 distinct points. Its numerator has degree at most k + 1, so it vanishes at 0, which contradicts E_{Q₁}[p₂/p₁] > 1. For the products criterion: if the numeraires are products of copies of e, then e is an e-variable (the numeraire of one observation), so the process is an e-process and the criterion applies.
• Proof for the counterexample. The negation of every observation fixes Ber(1/2) ^ n and exchanges the two null products. The likelihood ratio against their equal mixture therefore has expectation 1 under both, and it is the numeraire by the lemma above. Half of it is at most the likelihood ratio against each null product, which is a test supermartingale for that law. isEProcess_iff_forall_singleton and IsEProcess.mono then give the e-process.
• No published source. The counterexample, the value 367/340, the half e-process and the two-point criterion have no published source. The roadmap cites them [EVR26, Note 23]. The proofs here are rewritten from the Lean proofs of the paper project.
• Reuse, and what is not restated. Products of copies of an e-variable form a test supermartingale. That fact enters only as a private lemma (isEProcess_of_eq_prod), a direct application of isTestSupermartingale_mul_prod. It is not restated publicly, since it is the i.i.d. case of the sequential numeraires of Layer 4.5. I looked at LMLExplore/EValues/Numeraire.lean: going through the effective null (isNumeraire_of_ae_eq_rnDeriv) to identify the numeraire of the two-point null is not shorter than the direct check through Statlib's isNumeraire_iff, so that file is not imported. This pull request does not touch it either, so it does not interact with the open feat: identifying numeraires through the effective null #410.
• Overlap with open pull requests. The open feat: admissible e-processes, and the admissibility of the sub-Gaussian exponential e-process for nonatomic i.i.d. laws #434 (LMLExplore/EValues/SubGaussian/AdmissibleEProcess.lean) has the same two private lemmas as here, indep_piLE_comap_eval_succ and setLIntegral_comp_eval_succ (the coordinate n + 1 of an i.i.d. sequence is independent of Filtration.piLE n). The open feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3] #413 adds the public initSeg and measurePreserving_initSeg. Here the same fact is the private measurePreserving_fin, for fun ω (i : Fin n) ↦ ω i. This pull request cannot depend on either one, so it keeps private copies. Whichever lands second can replace them. No public name is shared with an open pull request.
• Deviations from the roadmap's wording.
  • Ber(p) is Mathlib's Ber(true, false, p), with mass p at true and p in unitInterval written ⟨1 / 5, by norm_num⟩. The observation 0 is false.
  • With Filtration.piLE, "stops after one observation" is time 0.
  • $\mathbb E_{Q_1}[p_2/p_1]$ is ∫⁻ x, P₂ {x} / P₁ {x} ∂Q₁.
  • "That is, when they are products" is the separate theorem exists_prod_eq_numeraires_pair_iff, about products of copies of one function e : α → ℝ≥0∞.
  • The statements hold for every family of numeraires, not only Statlib's numeraire.
  • The hypotheses are those of the roadmap: a finite space with measurable singletons, and Q₁, P₁, P₂ probability measures charging every point.
• Placement. The file is new and sits in LMLExplore/EValues/Numeraire/, next to LMLExplore/EValues/Numeraire.lean. It fits the 1500-line limit, so the Bernoulli example is not split into a second module. The helpers (masses of products, mixtures, the interior weight, the two-valued stopping times, the polynomial argument) are private.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R26

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

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

The PR description says the proofs are rewritten from the Lean proofs of the paper project (EVR26, Note 23), but the file credits only RGVS23, which posed the question. The closely followed prior formalization and its informal source have to be named in the code.

• LMLExplore/EValues/Numeraire/Sequential.lean:76 — The References and module docstring credit only [RGVS23] (the question). The results (the Bernoulli counterexample, 367/340, the half e-process, the two-point criterion) and their proofs come from EVR26 Note 23 and the Lean proofs of the paper project RemyDegenne/evalues_research. The PR description says so, but the code never mentions it. Fix: Add an attribution paragraph to the module docstring, e.g. 'The statements and proofs are adapted from the formalization of [EVR26, Note 23] in the paper project RemyDegenne/evalues_research (file EValuesResearch/..., commit ...).' Also add an [EVR26] entry to References.
• LMLExplore/EValues/Numeraire/Sequential.lean — The main theorems (isEProcess_numeraires_pair_iff, exists_prod_eq_numeraires_pair_iff, lintegral_numeraires_bernoulli_stop_eq, not_isEProcess_numeraires_bernoulli, isEProcess_half_numeraires_bernoulli) cite only [RGVS23, §8.2.4], as if this file originated the answers. Fix: Have each of these theorem docstrings cite [EVR26, Note 23] as the source of the result, keeping [RGVS23, §8.2.4] for the question.

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 · 29s · 234.5k in (178.6k cache read, 55.9k cache write) / 2.4k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

The five public theorems are well scoped, but general facts about infinite products, Filtration.piLE and numeraire uniqueness are hidden as private in a file about one specific counterexample, instead of being public in their natural homes.

• LMLExplore/EValues/Numeraire/Sequential.lean:96 — measurePreserving_fin is private but is a pure Mathlib-type fact: the first n coordinates of infinitePi have the law Measure.pi. LMLExplore/Probability/ProductMeasure.lean:54-56 already proves the same map identity inline (h_pi). Fix: Move it, as a public MeasureTheory.Measure lemma, to LMLExplore/Probability/ProductMeasure.lean, and use it in infinitePi_fin_mem_and_forall_add_mem in place of the inline h_pi.
• LMLExplore/EValues/Numeraire/Sequential.lean:119 — indep_piLE_comap_eval_succ and setLIntegral_comp_eval_succ (line 132) are private. They are general facts about i.i.d. sequences and Filtration.piLE, unrelated to numeraires, and the PR says open feat: admissible e-processes, and the admissibility of the sub-Gaussian exponential e-process for nonatomic i.i.d. laws #434 holds identical private copies. Duplicating hidden infrastructure across PRs is the under-exposure this rubric flags. Fix: Make both public in a shared probability file, e.g. LMLExplore/Probability/ProductMeasure.lean, so that feat: admissible e-processes, and the admissibility of the sub-Gaussian exponential e-process for nonatomic i.i.d. laws #434 and later Layer 6 items reuse them.
• LMLExplore/EValues/Numeraire/Sequential.lean:105 — measurable_piLE_fin, adapted_comp_fin (line 112) and isStoppingTime_comp_fin (line 522) are private. They are general facts about measurability, adaptedness and stopping times for Filtration.piLE over initial segments, independent of this file's subject. Fix: Expose them publicly next to the other piLE lemmas, in the same shared file as the independence lemmas above.
• LMLExplore/EValues/Numeraire/Sequential.lean:192 — eq_of_isNumeraire is private. It is a reusable part of the numeraire API: on a countable space where Q charges every point, two numeraires are equal. It is general to any null S and does not depend on the sequential subject. Fix: Make it public as IsNumeraire.eq_of_countable (or similar) in LMLExplore/EValues/Numeraire.lean, next to the existing numeraire API.

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 · 42s · 315.8k in (298.8k cache read, 17k cache write) / 3.8k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

File location and imports are fine, but three generic i.i.d. lemmas are kept private in the e-values file instead of in the existing product-measure file.

• LMLExplore/EValues/Numeraire/Sequential.lean:96 — measurePreserving_fin, indep_piLE_comap_eval_succ (l.119) and setLIntegral_comp_eval_succ (l.133) are generic facts about i.i.d. Measure.infinitePi sequences and Filtration.piLE, but they sit as private lemmas in an e-values numeraire file. The PR description says open feat: admissible e-processes, and the admissibility of the sub-Gaussian exponential e-process for nonatomic i.i.d. laws #434 keeps private copies of the same piLE lemmas. Fix: Move all three as public lemmas into LMLExplore/Probability/ProductMeasure.lean (namespace MeasureTheory.Measure/ProbabilityTheory), adding the needed imports there, and import that module here.

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 · 35s · 296.6k in (284.6k cache read, 12k cache write) / 3.1k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

The module docstring is accurate and its counterexample values check out (1, 25/34, 25/16, mean 367/340). Two public theorem docstrings describe the proof, and a third makes a claim the theorem statement does not deliver.

• LMLExplore/EValues/Numeraire/Sequential.lean:838 — The docstring of isEProcess_numeraires_pair_iff ends by describing the proof ('When both expectations exceed 1, the proof finds the failure at a stopping time…'), not the result. Fix: Delete that sentence; the module's Implementation notes already contain it.
• LMLExplore/EValues/Numeraire/Sequential.lean:1129 — The docstring of isEProcess_half_numeraires_bernoulli ends with a proof sketch ('half the likelihood ratio against the equal mixture … is at most the likelihood ratio against each of them, a test supermartingale under that law'). Fix: End the docstring at 'whatever numeraires X n are chosen.'
• LMLExplore/EValues/Numeraire/Sequential.lean:870 — The docstring of exists_prod_eq_numeraires_pair_iff says the likelihood ratio of Q₁ against P₁ or P₂ is the function e, but the statement only gives ∃ e; that choice is proved only in the private isEVar_div_and_eq_prod_of_le. Fix: Remove the last sentence, or put the explicit e = fun y ↦ Q₁ {y} / P₁ {y} (resp. P₂) into the public statement.

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 · 45s · 234.6k in (226.2k cache read, 8.4k cache write) / 4.1k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

🟡 proof-quality — request_changes claude/claude-opus-5-5

The proofs rest on uncommented change, show … from rfl and closing rfl steps that depend on definitional unfolding, and not_isEProcess_of_one_lt is a ~175-line proof hiding reusable sub-facts. Repeated side lemmas and a long rw chain in the Bernoulli computation also make the file fragile.

• LMLExplore/EValues/Numeraire/Sequential.lean:1086 — change X 0 (fun i ↦ ω i) = _ (and change X 1 … at line 1089) is uncommented and relies on if false then 1 else 0 reducing by defeq after cases hω : ω 0. Fix: Rewrite the index instead, e.g. rw [hω, if_neg Bool.false_ne_true] / rw [hω, if_pos rfl], or simp only [hω, Bool.false_eq_true, if_false].
• LMLExplore/EValues/Numeraire/Sequential.lean:529 — Uncommented change MeasurableSet[Filtration.piLE i] {ω | …} unfolds the IsStoppingTime goal through defeq. Fix: Use the set-builder unfolding lemma for stopping times or show it with a comment explaining why no rewrite works; or prove the emptiness by simp on the original goal.
• LMLExplore/EValues/Numeraire/Sequential.lean:250 — rw [show (fun x ↦ piMass μ x) = fun x ↦ ∏ i, μ.real {x i} from rfl, …] unfolds the private def by defeq. Closing rfls at line 186 (after mul_comm in isEProcess_of_eq_prod) and line 292 (piMass_snoc) also close goals only up to unfolding. Fix: Add @[simp] private lemma piMass_def (or use simp only [piMass] / unfold piMass), and finish lines 186/292 with an explicit rewrite.
• LMLExplore/EValues/Numeraire/Sequential.lean:701 — not_isEProcess_of_one_lt runs from line 701 to about 876 (~175 lines). It has two self-contained sub-facts inlined: the existence of y₁ y₂ with r y₁ < r y₂ (otherwise E_Q[p₂/p₁] = 1, lines 712–733) and the geometric-ratio samples x j with injective s (hratio, hinj, lines 799–840). Fix: Extract exists_ratio_lt_of_one_lt and a lemma giving the samples x j with piMass P₂ / piMass P₁ = r₂^(k+1) (r₁/r₂)^j and injectivity, so that the main proof only chains the e-process steps.
• LMLExplore/EValues/Numeraire/Sequential.lean:312 — The fact that every member of {P₁, P₂} is a probability measure is re-proved by the same 3-line block four times (lines 312, 429, 905, 935). Positivity of the mixture w·piMass P₁ + (1-w)·piMass P₂ is also re-derived in exists_weight_interior, not_isEProcess_of_one_lt (hmix) and mul_ofReal_div_mix_le. Fix: Add private lemmas isProbabilityMeasure_of_mem_pair and mix_pos (hw0 : 0 ≤ w) (hw1 : w ≤ 1) … and use them at each site.
• LMLExplore/EValues/Numeraire/Sequential.lean:1094 — The final computation of 367/340 is one long brittle rw chain (measurePreserving_fin, lintegral_fintype, pi_singleton_eq_ofReal_piMass, ENNReal.ofReal_sum_of_nonneg, finTwoArrowEquiv, Fintype.sum_prod_type, three Fintype.sum_bool), followed by simp only [… Matrix.cons_val_zero, Matrix.cons_val_one …]. It will break on Mathlib renames. Fix: Factor the step ∫⁻ f(first two coords) ∂P^ℕ = ∑ b₀ b₁, f ![b₀,b₁] * P{b₀} * P{b₁} into a lemma, then close the numeric goal with simp [Fin.prod_univ_two, Fintype.sum_bool, hP₁]; norm_num.

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 · 37s · 115k in (106.4k cache read, 8.6k cache write) / 3.8k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[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 statements match the roadmap bullet (EValues Layer 6 item 1): the stopping time and the value 367/340 check out by hand, half the process is shown to be an e-process via the bound against each null product, and the two-point criterion and the products criterion are stated over every family of numeraires, with full-support hypotheses that make the version irrelevant. The numeraire hypotheses are not vacuous, since the private lemmas build explicit numeraires (the likelihood ratio against a mixture), and IsEProcess is the repo's standard definition with finite stopping times.
✅	reuse	approved	claude/claude-opus-5-5	The new file adds results that do not exist in Mathlib or LMLExplore, and its private helpers are built from existing Mathlib, Statlib and LMLExplore API (map_infinitePi_infinitePi_of_inj, iIndepFun_infinitePi, isTestSupermartingale_mul_prod, isNumeraire_iff, IsNumeraire.ae_unique). The private i.i.d. helpers have no landed counterpart at the PR head; the open #434 and #413 copies are not yet merged.
✅	scope	approved	claude/claude-opus-5-5	The PR implements one complete roadmap bullet, EValues README lines 926–932 (the numeraires as a process are not an e-process [RGVS23, §8.2.4], the Ber(1/5)/Ber(4/5) counterexample with mean 367/340, the half e-process, and the two-point criterion and product characterisation), as a single new file. Its private helpers serve only that bullet, and no other topic or refactor is bundled in.
🟡	attribution	changes requested	claude/claude-opus-5-5	The PR description says the proofs are rewritten from the Lean proofs of the paper project (EVR26, Note 23), but the file credits only RGVS23, which posed the question. The closely followed prior formalization and its informal source have to be named in the code.
🟡	api-design	changes requested	claude/claude-opus-5-5	The five public theorems are well scoped, but general facts about infinite products, Filtration.piLE and numeraire uniqueness are hidden as private in a file about one specific counterexample, instead of being public in their natural homes.
✅	generality	approved	claude/claude-opus-5-5	The public statements use exactly the roadmap's hypotheses (finite space, measurable singletons, full support, which is needed for version-independent statements) and hold for any family of numeraires. The Bernoulli negation is a short corollary of the computation the roadmap asks for, not a duplicate of the general criterion's proof, and the private helpers add no special-case duplication.
🟡	placement	changes requested	claude/claude-opus-5-5	File location and imports are fine, but three generic i.i.d. lemmas are kept private in the e-values file instead of in the existing product-measure file.
✅	naming	approved	claude/claude-opus-5-5	Public names (isEProcess_numeraires_pair_iff, exists_prod_eq_numeraires_pair_iff, not_isEProcess_numeraires_bernoulli, isEProcess_half_numeraires_bernoulli, lintegral_numeraires_bernoulli_stop_eq) describe their conclusions in standard terminology and live in ProbabilityTheory, as do all sibling EValues files; no notation is introduced.
🟡	documentation	changes requested	claude/claude-opus-5-5	The module docstring is accurate and its counterexample values check out (1, 25/34, 25/16, mean 367/340). Two public theorem docstrings describe the proof, and a third makes a claim the theorem statement does not deliver.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	The proofs rest on uncommented change, show … from rfl and closing rfl steps that depend on definitional unfolding, and not_isEProcess_of_one_lt is a ~175-line proof hiding reusable sub-facts. Repeated side lemmas and a long rw chain in the Bernoulli computation also make the file fragile.

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

_{Reviewing this diff at head 794fc47. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.07.}