[RemyDegenne]

This pull request proves that the effective null is closed in total variation, so that a null whose closure in total variation contains every probability measure has, for every finite number of i.i.d. observations, the e-variables of the null of all laws; and it applies this to the laws on ℝ with mean 0 and a finite, positive variance, which therefore cannot be tested with e-variables against i.i.d. alternatives (the form for e-variables of the theorem of Bahadur and Savage [BS56]). It adds three new files, LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean, LMLExplore/EValues/EffectiveSet/TotalVariation.lean and LMLExplore/EValues/MeanZeroNull.lean, and adds general lemmas to the existing LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean, LMLExplore/MeasureTheory/Constructions/Pi.lean and LMLExplore/Basic/ENNReal/BigOperators.lean.

Main declarations

In MeasureTheory (general measure theory):

• measure_le_add_etvDist (in the existing TotalVariation/Basic.lean): μ s ≤ ν s + etvDist μ ν for every measurable s, for any two measures. The ℝ≥0∞ companion of Tau Ceti's abs_measureReal_sub_le_tvDist.
• isProbabilityMeasure_of_forall_exists_etvDist_lt (in TotalVariation/Basic.lean): a limit in total variation of probability measures is a probability measure.
• exists_le_le_add_etvDist (in TotalVariation/Basic.lean): two finite measures have a common minorant ρ with μ univ + ν univ = 2 * ρ univ + etvDist μ ν (on a Hahn decomposition).
• Measure.pi_mono (in the existing Constructions/Pi.lean, @[gcongr]): Measure.pi μ ≤ Measure.pi ν when μ i ≤ ν i for every i and the ν i are finite.
• ENNReal.one_sub_prod_le_sum_one_sub (in the existing Basic/ENNReal/BigOperators.lean): 1 - ∏ i ∈ s, m i ≤ ∑ i ∈ s, (1 - m i) for m i ≤ 1.
• etvDist_pi_le_sum (new TotalVariation/Pi.lean): etvDist (Measure.pi μ) (Measure.pi ν) ≤ ∑ i, etvDist (μ i) (ν i) for finite products of probability measures.

In ProbabilityTheory, LMLExplore/EValues/EffectiveSet/TotalVariation.lean (general nulls):

• mem_effectiveSet_of_forall_exists_etvDist_lt: the effective null effectiveSet S is closed in total variation (no hypothesis on S).
• isEVar_iff_of_forall_exists_etvDist_dirac_lt: if every point mass is a limit in total variation of members of a null of measures of mass at most 1, its e-variables are the measurable functions bounded by 1 everywhere.
• isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt: the same for the null Measure.infinitePi '' {P : ι → Measure 𝓧 | ∀ i, P i ∈ S} of the laws of independent sequences with marginals in S, for a countable ι and measurable singletons.
• pi_mem_effectiveSet_of_forall_exists_etvDist_lt: if Q is a limit in total variation of members of a null S of probability measures, then Measure.pi (fun _ : ι ↦ Q) is in the effective null of (fun P ↦ Measure.pi fun _ : ι ↦ P) '' S, for every finite ι.
• isEVar_pi_iff_of_forall_exists_etvDist_lt: the corollary of the roadmap. If every probability measure is a limit in total variation of members of S, then IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' S) ↔ IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' {P | IsProbabilityMeasure P}).
• measure_pi_le_of_forall_exists_etvDist_lt, maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt, bipolarRate_eq_zero_of_forall_exists_etvDist_lt: against a Q that is a limit in total variation of members of S, a measurable set of ι observations of probability at most α under every P ^ ι, P ∈ S, has probability at most α under Q ^ ι, and maxLogGrowth Q S n = 0, bipolarRate Q S = 0.

In ProbabilityTheory, LMLExplore/EValues/MeanZeroNull.lean (the instance):

• meanZeroPosVarNull : Set (Measure ℝ): {μ | IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧ ∫ x, x ∂μ = 0 ∧ 0 < variance id μ}, with mem_meanZeroPosVarNull_iff and isProbabilityMeasure_of_mem_meanZeroPosVarNull (the definition is not exposed).
• exists_mem_meanZeroPosVarNull_etvDist_lt: the null is dense in total variation among the probability measures on ℝ.
• isEVar_pi_meanZeroPosVarNull_iff: its ι-sample e-variables are those of the i.i.d. laws of all probability measures on ℝ.
• isEVar_meanZeroPosVarNull_iff: its one-observation e-variables are the measurable functions bounded by 1 everywhere.
• maxLogGrowth_meanZeroPosVarNull, bipolarRate_meanZeroPosVarNull: maxLogGrowth Q meanZeroPosVarNull n = 0 and bipolarRate Q meanZeroPosVarNull = 0 for every probability measure Q on ℝ.
• measure_pi_le_of_forall_meanZeroPosVarNull: a measurable set of ι observations of probability at most α under every i.i.d. law of the null has probability at most α under every i.i.d. law.
• le_one_of_isEProcess_infinitePi_meanZeroPosVarNull: every e-process, for any filtration on ℕ → ℝ, for the laws of the independent sequences with marginals in the null is at most 1 at every time and on every sequence.

Roadmap coverage (EValues, Layer 1, item 1, and Layer 6, item 2)

Covered:

• Layer 1, item 1, the bullet "Corollary: a null S such that every probability measure on 𝓧 is a limit in total variation of members of S …", with its instance (density of the mean-zero null and its one-observation e-variables).
• Layer 6, item 2, the bullet "Instance without power [BS56]": a n = 0, d = 0, the bound on tests and the bound on e-processes.

Not covered, and not asked by these two bullets: the other bullets of both items.

Notes for reviewers

• Route. As the roadmap asks, the corollary is derived from the closure of the effective null under setwise convergence, in the form mem_effectiveSet_of_measure_le_liminf of EffectiveSet.lean: along the filter of members of the effective null whose distance to μ tends to 0, μ s ≤ liminf ν s by measure_le_add_etvDist. The truncation of unbounded e-variables is inside that closure lemma, so no truncation argument appears here. Products enter only through etvDist_pi_le_sum, which is proved with the common minorant μ.restrict s + ν.restrict sᶜ on a Hahn decomposition and 1 - ∏ m i ≤ ∑ (1 - m i). The consequences for one observation and for independent sequences go through the same closure: a point mass is in the effective null, and X x = ∫⁻ X ∂(dirac x) ≤ 1; for sequences, the marginals are chosen to miss masses of small sum at the given sequence.
• Total variation. Density is stated with Mathlib's etvDist as ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε, the form of Metric.mem_closure_iff; there is no topology of total variation on Measure to state it as a closure. Mathlib normalizes etvDist to [0, 2] on probability measures; the density hypotheses do not depend on the normalization.
• Generality beyond the roadmap's wording. The consequences listed for the instance in Layer 6.2 are stated for every null of probability measures and every Q that is a limit in total variation of members of the null (a hypothesis at Q only), and the instance theorems are one-line corollaries. The one-observation characterization assumes only that the members of the null have mass at most 1 and that the point masses are limits in total variation of them. The general theorems do not assume IsProbabilityMeasure Q: it follows from the density hypothesis (isProbabilityMeasure_of_forall_exists_etvDist_lt). The e-variable statement for sequences is for any countable index type; the e-process statement is for ℕ → ℝ, as the roadmap states it.
• The null of independent sequences is written Measure.infinitePi '' {P : ι → Measure 𝓧 | ∀ i, P i ∈ S}, with no new definition: it appears in two statements, and Layer 4.5 of the roadmap will define the sequential null (conditional laws in S₁), which contains these laws; a definition now would be a second name for a subset of that one.
• The definition of the mean-zero null asks MemLp id 2 μ, ∫ x, x ∂μ = 0 and 0 < variance id μ: with MemLp id 2, Mathlib's real variance is the variance, so the last condition is "positive variance".
• Changed existing files. TotalVariation/Basic.lean gets measure_le_add_etvDist, measure_le_add_of_etvDist_le, isProbabilityMeasure_of_forall_exists_etvDist_lt and exists_le_le_add_etvDist; Constructions/Pi.lean gets Measure.pi_mono (no such lemma in Mathlib, Tau Ceti, LML, Statlib or LMLExplore; the proof uses Statlib's Measure.pi_eq_withDensity_prod_rnDeriv, now imported there); Basic/ENNReal/BigOperators.lean gets ENNReal.one_sub_prod_le_sum_one_sub. Each with a module-docstring bullet, and nothing else.
• Renamed module. LMLExplore.EValues.EffectiveSet is moved to LMLExplore.EValues.EffectiveSet.Basic (no declaration changes; its importers Numeraire.lean and EffectiveSet/TotalVariation.lean are updated, and there is no forwarding module). Downstream projects should import LMLExplore.EValues.EffectiveSet.Basic.
• Private helpers. EffectiveSet/TotalVariation.lean has three proof helpers (approximation by members of S, approximation of products, approximation of point masses by independent sequences). MeanZeroNull.lean has the integrability and mean of the two-atom measure dirac (z - 1) + dirac (z + 1), and three steps of the construction: the identity is not almost everywhere 0 once two atoms at z ∓ 1 are added, the choice of an interval [-M, M] of mass above 1 - δ, and the completion of a measure of mass less than 1 carried by a bounded interval by two atoms that make the mean 0 and the variance positive.
• Overlap with open pull requests. None shares a declaration. 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 renames the module LMLExplore.EValues.BipolarRate to LMLExplore.EValues.BipolarRate.Basic; whichever lands second updates the import in EffectiveSet/TotalVariation.lean. The open feat: identifying numeraires through the effective null #410 changes EffectiveSet.lean but keeps subset_effectiveSet and mem_effectiveSet_of_measure_le_liminf, the two lemmas used here.
• Sources. The results about the mean-zero null and about nulls dense in total variation have no published source: the roadmap cites them [EVR26, Note 22]; the proofs are rewrites of the Lean proofs of the paper project, which proved the corollary directly (common minorants, Bernoulli's inequality and truncation), and its one-observation and sequence statements through the masses ⨆ P ∈ S, P {x}. [BS56] is cited, as in the roadmap, for the theorem of which this is the form for e-variables; its proofs are not used. The three new files credit [EVR26, Note 22] and EValuesResearch/Results/PowerlessNulls.lean (commit dd4072f) in their implementation notes and references.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R25

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

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

Both earlier findings are fixed: pi_mono is now public in Constructions/Pi.lean, the unused import in MeanZeroNull.lean is gone, and the module rename updated every importer without a forwarding module. The new TotalVariation/Pi.lean imports Mathlib.MeasureTheory.Measure.TotalVariation.Basic but uses nothing from it.

• LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean:11 — import Mathlib.MeasureTheory.Measure.TotalVariation.Basic is unused. The file only uses etvDist_triangle, etvDist_of_ge and etvDist_of_le (from Defs), exists_le_le_add_etvDist (LMLExplore), Measure.pi_mono, Measure.pi_univ and ENNReal.one_sub_prod_le_sum_one_sub. Fix: Drop the import. The only place it is needed is LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean (for IsHahnDecomposition.etvDist_eq), which already imports it.

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

[RemyDegenne]

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

The undocumented defeq rfl steps, the private general helpers and the over-long proofs from the last round are fixed. One brittle chain of named rewrites remains in the completion lemma of MeanZeroNull.lean.

• LMLExplore/EValues/MeanZeroNull.lean — In exists_mem_meanZeroPosVarNull_le, hPprob is one rw chain of 10 named lemmas closed by ring, and hmean is a chain of 8 (integral_add_measure, integral_smul_measure, hD, integral_id_dirac_add_dirac, hct, hz, smul_eq_mul) closed by field_simp; ring. Both break on Mathlib renames or argument-order changes. Fix: Compute the mass in ℝ≥0∞ with simp [P, D, measure_univ] plus the c/b arithmetic, or split each chain into a short calc whose steps are simp. Do the same for hmean (e.g. simp [P, D, integral_add_measure, integral_id_dirac_add_dirac, hct, hz] then field_simp).

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 · 38s · 230.1k in (186.2k cache read, 43.9k cache write) / 3.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	stale (re-run pending)	claude/claude-opus-5-5	The definitions and statements match roadmap Layer 1.1 (density corollary and mean-zero instance) and Layer 6.2 (a n = 0, d = 0, bounds on tests and e-processes). Every general hypothesis is discharged for the concrete null meanZeroNull, which is non-empty, so no content has been moved into assumptions.
♻️	reuse	stale (re-run pending)	claude/claude-opus-5-5	No Mathlib or LMLExplore declaration replaces the new total-variation lemmas (measure_le_add_etvDist, etvDist_pi_le_sum, the minorant and product-monotonicity helpers, 1 - ∏ ≤ ∑ (1 - ·)) or meanZeroNull, and the proofs use existing API (mem_effectiveSet_of_measure_le_liminf, etvDist_of_ge/le, IsHahnDecomposition.etvDist_eq, measurePreserving_eval_infinitePi). Tau Ceti and Statlib sources were not in the checkout, so the claim that neither has Measure.pi monotonicity could not be checked.
♻️	scope	stale (re-run pending)	claude/claude-opus-5-5	The PR proves exactly the Layer 1.1 total-variation corollary with its mean-zero instance and the Layer 6.2 'Instance without power [BS56]' bullet, and its two total-variation lemmas are needed only for those. It is one topic, since Layer 1.1 itself points to Layer 6.2 for the consequences for power.
✅	attribution	approved	claude/claude-opus-5-5	All three new files now credit [EVR26, Note 22] and the paper project's Lean source EValuesResearch/Results/PowerlessNulls.lean (commit dd4072f), and cite [BS56] only for the classical theorem; the prior findings are resolved. The general lemmas added to existing files are routine and the roadmap is not cited in code.
✅	api-design	approved	claude/claude-opus-5-5	The four general helpers flagged earlier are now public in their proper files, the remaining private declarations are proof-specific steps, and the module rename has no compatibility shim. meanZeroPosVarNull has an unexposed body and its membership lemma.
♻️	generality	stale (re-run pending)	claude/claude-opus-5-5	The general theorems on nulls dense in total variation are stated at the natural level with hypotheses no stronger than needed, and the mean-zero results are one-line corollaries of them. There are no unused or too-strong public assumptions and no proofs duplicated for special cases.
🟡	placement	changes requested	claude/claude-opus-5-5	Both earlier findings are fixed: pi_mono is now public in Constructions/Pi.lean, the unused import in MeanZeroNull.lean is gone, and the module rename updated every importer without a forwarding module. The new TotalVariation/Pi.lean imports Mathlib.MeasureTheory.Measure.TotalVariation.Basic but uses nothing from it.
✅	naming	approved	claude/claude-opus-5-5	The prior finding is resolved: the definition is now meanZeroPosVarNull, which names all its conditions, and no stale meanZeroNull references remain. All new names describe their conclusions in standard terminology, match their statement strength, and no notation is introduced.
♻️	documentation	stale (re-run pending)	claude/claude-opus-5-5	All three new files have accurate module docstrings, and every public declaration is documented without overclaiming; the claims checked against Mathlib's etvDist, maxLogGrowth and mem_effectiveSet_of_measure_le_liminf match the statements.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	The undocumented defeq rfl steps, the private general helpers and the over-long proofs from the last round are fixed. One brittle chain of named rewrites remains in the completion lemma of MeanZeroNull.lean.

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

_{Reviewing this diff at head 1c65063. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.19.}

[lmlexplore-automation]

⚠️ This PR no longer merges into main. Rebase it onto current main (or merge main into it) and push — nothing downstream can make progress until then, since a green build and an approving review on this head still cannot merge.

Do check what the conflict actually is before resolving it mechanically. If main has since landed its own version of something this PR adds, part of it may be superseded, and the right answer is to drop that part — or close the PR — rather than to reconcile the text. That is an authoring decision.