[RemyDegenne]

This pull request proves that for a convex i.i.d. null, a test martingale is still a test martingale under the i.i.d. law of every probability measure in the linear span of the null, so it has no power one against such an alternative. It also proves that convexity is needed: for the null of the two point masses on Bool, some test martingale tends to ∞ almost surely under i.i.d. fair coin flips. It adds LMLExplore/EValues/PowerOne/TestMartingale.lean, and, as public prerequisites, the generic lemmas on products of mixtures and finite convex combinations that the proof uses (listed below).

Main declarations

• isTestMartingale_infinitePi_of_add_sum_eq_sum: let S₁ : Set (Measure 𝓧) be convex (Convex ℝ≥0∞ S₁), P : ι → Measure 𝓧 finitely many probability measures in S₁, b c : ι → ℝ≥0, and Q₁ a probability measure with Q₁ + ∑ i, b i • P i = ∑ i, c i • P i. Let ℱ be a filtration on ℕ → 𝓧 with ∀ n, ∃ N, ℱ n ≤ Filtration.piLE N. Then an M with IsTestMartingale M ℱ ((fun P ↦ Measure.infinitePi fun _ ↦ P) '' S₁) and ∫⁻ ω, M 0 ω ∂Measure.infinitePi (fun _ ↦ P) = 1 for every P ∈ S₁ satisfies IsTestMartingale M ℱ {Measure.infinitePi fun _ ↦ Q₁}.
• ae_limsup_lt_top_infinitePi_of_add_sum_eq_sum: under the same hypotheses, ∀ᵐ ω ∂Measure.infinitePi (fun _ ↦ Q₁), limsup (fun n ↦ M n ω) atTop < ∞. So M neither tends to ∞ nor has an infinite limsup on a set of positive probability: it does not have power one against Q₁.
• exists_isTestMartingale_dirac_tendsto_top: there is M : ℕ → (ℕ → Bool) → ℝ≥0∞ with M 0 = 1, a test martingale for Filtration.piLE and the i.i.d. laws of {dirac false, dirac true}, that tends to ∞ almost surely under the i.i.d. law of 2⁻¹ • (dirac false + dirac true). The fair coin is the midpoint of the null, so it lies in the span; the null is not convex.

Supporting public lemmas

• LMLExplore/MeasureTheory/Constructions/Pi.lean (existing file): MeasureTheory.Measure.pi_const_smul (Measure.pi (fun _ ↦ s • ν) = s ^ card ι • Measure.pi (fun _ ↦ ν)), MeasureTheory.Measure.pi_sum_smul (Measure.pi (fun _ ↦ ∑ k, w k • R k) = ∑ e, (∏ i, w (e i)) • Measure.pi (fun i ↦ R (e i))), its integral form MeasureTheory.Measure.lintegral_pi_sum_smul, and the polarization lemma MeasureTheory.Measure.lintegral_pi_eq_of_add_sum_eq_sum (if Q + ∑ b k • P k = ∑ c k • P k, equal integrals under the products of copies of every convex combination of the P k give equal integrals under the product of copies of Q), with its private identity-theorem helper sum_prod_bif_mul_eq_of_one_lt.
• LMLExplore/Probability/ProductMeasure.lean (existing file): MeasureTheory.Measure.lintegral_infinitePi_eq_of_add_sum_eq_sum, the same polarization for i.i.d. laws of Filtration.piLE N-measurable functions.
• LMLExplore/Algebra/BigOperators/Field.lean (new): Finset.sum_smul_eq_smul_sum_div_smul (over any semifield).
• LMLExplore/Analysis/Convex/ENNReal.lean (new): Convex.sum_nnreal_smul_mem (a set convex over ℝ≥0∞ in any ℝ≥0∞-module contains its finite combinations with ℝ≥0 weights of sum 1; Mathlib's Convex.sum_mem needs a field acting on an additive group).
• LMLExplore/MeasureTheory/Measure/Typeclasses/Probability.lean (new): MeasureTheory.isProbabilityMeasure_sum_smul, the finite form of Tau Ceti's isProbabilityMeasure_smul_add_smul.

Roadmap coverage (EValues, Layer 6, item 2)

Covered: the bullet "Test martingales [ZRW24, §7]", that is, the statement for convex S₁, its consequence "none has power one against Q₁", and the counterexample showing that convexity is needed. Not covered: the other bullets of item 2 (the equivalences of [Ram26, Theorem 3.1], the expected stopping times of [Ram26, Corollary 3.2], [RR26, Theorem 3.14], the instance without power [BS56], and [RW, Proposition 3.12, Theorem 3.14]).

The two theorems have no published source: [ZRW24, §7] states the question, and the roadmap cites the answer [EVR26, Note 03]. The proofs here rewrite the Lean proofs of the paper project (EValuesResearch/Results/TestMartingaleConverse.lean, commit 6f05c5f), credited in the file with the reference [EVR26, Note 03, Theorem 1 and Counterexample 1].

Notes for reviewers

• How the proof goes. An ℱ n-measurable set and the values M n and M (n + 1) are measurable for some Filtration.piLE N. So they factor through the first N + 1 observations (Mathlib's Measurable.exists_eq_measurable_comp), and their integrals under Measure.infinitePi are integrals under Measure.pi over Finset.Iic N (lintegral_restrict_infinitePi). The finite-dimensional step is a polarization argument in one variable. Put B = ∑ i, b i • P i. Expanding the product of copies of Q₁ + t • B shows that the integral of a function of the observations is a polynomial in t with coefficients in ℝ≥0∞. Those coefficients are finite, as the case t = 1 shows. For t ≥ 1, Q₁ + t • B = ∑ i, (c i + (t - 1) * b i) • P i is a positive multiple of a convex combination of the P i, which lies in the null, so the martingale identities hold there. The real polynomials are analytic and agree on (1, ∞), so they agree at t = 0 (AnalyticOnNhd.eq_of_eventuallyEq). The two polarization lemmas are public (above); the identity-theorem step for the polynomials (sum_prod_bif_mul_eq_of_one_lt) and the counterexample process are private.
• Convexity. The hypothesis is Mathlib's Convex ℝ≥0∞ S₁. That is how convex sets of measures are stated in LMLExplore (convex_effectiveSet), Statlib (convex_isEVar) and Tau Ceti (the sets of exchangeable laws). With ℝ≥0∞ scalars, a + b = 1 makes both weights finite. Mathlib's Convex.sum_mem needs a field and an additive group, so the file proves the finite convex combinations (Convex.sum_nnreal_smul_mem), by induction. The proof only uses the convex combinations of the P i. The statement with convexHull ℝ≥0∞ (Set.range P) ⊆ S₁ in place of the convexity of S₁ is the theorem applied to that convex hull, a one-line term (convex_convexHull, subset_convexHull, IsTestMartingale.anti_set; checked to compile), so it is not stated separately.
• Deviations from the roadmap's wording.
  • The roadmap says "with initial value 1". The hypothesis here is weaker: ∫⁻ M 0 = 1 under the i.i.d. law of every member of S₁, which M 0 = 1 implies. It enters the proof through one more polarization step, for M 0 against the constant 1. The counterexample has M 0 = 1 and satisfies every hypothesis of the theorem except convexity.
  • The roadmap's convention assumes ∀ P ∈ S₁, IsProbabilityMeasure P. The theorems assume it only for the P i, which is all the proof uses.
  • The weights are b c : ι → ℝ≥0, acting on measures through ℝ≥0. They must be finite: with b i = c i = ∞, the identity Q₁ + ∞ • P i = ∞ • P i holds for every Q₁ ≪ P i.
  • "None has power one" is stated as the almost sure finiteness of the limsup under Q₁, from IsTestSupermartingale.ae_limsup_lt_top. This excludes both forms of power one in item 2, tending to ∞ and having an infinite limsup.
  • The two-point space is Bool, and the fair coin is 2⁻¹ • (dirac false + dirac true).
• Placement. The file opens the folder LMLExplore/EValues/PowerOne/, named after item 2 of Layer 6, for the other bullets of that item. The i.i.d. growth rates of item 1 are in LMLExplore/EValues/BipolarRate/.
• Open pull requests. None of them covers this item, and nothing here is shared with them. 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 initSeg and lemmas on functions of the first n observations. This pull request does not use them: it works with Mathlib's Filtration.piLE_eq_comap_frestrictLe, Measurable.exists_eq_measurable_comp and lintegral_restrict_infinitePi.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R17

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

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

The main file credits [ZRW24, §7], [EVR26, Note 03], and the adapted formalization TestMartingaleConverse.lean at commit 6f05c5f. The polarization argument at the heart of Note 03, Theorem 1 now lives in generic files that carry no credit.

• LMLExplore/MeasureTheory/Constructions/Pi.lean — lintegral_pi_eq_of_add_sum_eq_sum and its helper sum_prod_bif_mul_eq_of_one_lt are the central proof of [EVR26, Note 03, Theorem 1]: expand the product of copies of Q + t•B as a polynomial in t, check it for t ≥ 1, then use the identity theorem. The PR says this was rewritten from the paper project's Lean proof, but neither the module docstring nor the declaration docstrings name that source. Fix: Add a sentence to the module docstring's mixtures paragraph (or to the lemma docstring) saying the polarization argument is adapted from [EVR26, Note 03, Theorem 1] / EValuesResearch/Results/TestMartingaleConverse.lean (commit 6f05c5f). Add a matching References entry.
• LMLExplore/Probability/ProductMeasure.lean:96 — Same issue here: lintegral_infinitePi_eq_of_add_sum_eq_sum, the i.i.d. form of the same polarization step taken from the paper project, credits no source. Fix: Cite [EVR26, Note 03, Theorem 1] and the adapted formalization in the lemma docstring or the module docstring.

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 · 22s · 72.2k in (65.3k cache read, 7k cache write) / 2k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

The module and theorem docstrings are accurate and describe the statements, not the process. But the file cites [ZRW24, §7] only for the conjecture and never cites [EVR26, Note 03], the only source of the result it formalizes.

• LMLExplore/EValues/PowerOne/TestMartingale.lean:58 — The ## References section lists only [ZRW24]. That paper only states the question, so the convexity theorem and the Bool counterexample have no source cited in the file. The roadmap credits both to [EVR26, Note 03], and the PR description says the proofs rewrite that project's Lean proofs. Fix: Add an [EVR26, Note 03] entry to ## References. Cite it in the module docstring, where the result and the counterexample are stated, and in the docstrings of isTestMartingale_infinitePi_of_add_sum_eq_sum and exists_isTestMartingale_dirac_tendsto_top.

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 · 92.9k in (84.2k cache read, 8.6k cache write) / 2.3k 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 main theorem, its no-power-one corollary and the Bool counterexample faithfully state the roadmap bullet (EValues README:971-977), with a weaker hypothesis on the initial value; the supporting polarization and convex-combination lemmas match their docstrings. I tried to find vacuity, wrong quantifiers or weakened conclusions and found none.
✅	reuse	approved	claude/claude-opus-5-5	No new declaration duplicates Mathlib or LMLExplore: Mathlib's Convex.sum_mem/centerMass need a field and an additive group, and there is no Mathlib lemma for finite sums of probability measures or for products of copies of scaled or mixed measures. The proofs reuse existing Mathlib API, including Fintype.prod_sum, Measure.infinitePi_dirac and restrict_dirac'.
✅	scope	approved	claude/claude-opus-5-5	The PR implements the 'Test martingales [ZRW24, §7]' bullet of EValues Layer 6 item 2 (README.md:971-977) in full: the convex-null theorem, the no-power-one consequence and the convexity counterexample. Its supporting lemmas are prerequisites used directly by the main proof, so the PR is one coherent topic.
🟡	attribution	changes requested	claude/claude-opus-5-5	The main file credits [ZRW24, §7], [EVR26, Note 03], and the adapted formalization TestMartingaleConverse.lean at commit 6f05c5f. The polarization argument at the heart of Note 03, Theorem 1 now lives in generic files that carry no credit.
✅	api-design	approved	claude/claude-opus-5-5	The general polarization, product-of-mixture, convex-combination and normalization lemmas are now public in their canonical homes, and only the polynomial identity-theorem helper and the counterexample process stay private. There is no compatibility layer, no exposed body and no public definition lacking API.
✅	generality	approved	claude/claude-opus-5-5	Statements are at the natural level: the theorem's hypotheses are minimal for the claim (weaker initial-value condition, probability only for the P i, finite ℝ≥0 weights), polarization is proved once generally and the i.i.d. form derived from it, and the helper lemmas fill gaps Mathlib does not cover (Convex.sum_mem needs a field over an AddCommGroup; only Dirac-specific mixture-probability lemmas exist).
✅	placement	approved	claude/claude-opus-5-5	Both earlier placement findings are fixed: the semifield lemma now lives in Algebra/BigOperators/Field.lean and the probability-measure lemma in MeasureTheory/Measure/Typeclasses/Probability.lean. Every new declaration is in its natural home and no import is unused or too broad.
✅	naming	approved	claude/claude-opus-5-5	New declaration names describe their conclusions in standard Mathlib terminology, match adjacent declarations, and sit in appropriate namespaces (ProbabilityTheory, MeasureTheory.Measure, Convex. dot notation, Finset.). No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Each new file has an accurate module docstring and every public lemma and main theorem has a docstring matching its statement, with hypotheses (finitely-generated filtration, initial expectation 1, finite weights) reflected and no roadmap or process narrative in the files.
✅	proof-quality	approved	claude/claude-opus-5-5	The proofs are robust and readable: the identity-theorem step is a separate helper lemma, the long polarization proof has comments explaining its structure, and the earlier undocumented definitional-equality step in hadapted now carries a comment (congr over Decidable instances). No proof-quality issues remain.

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

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