[RemyDegenne]

This PR builds the first two bullets of the EValues Layer 1.1 milestone, The effective null [LRR25, Definition 3.1; RW, §6.3.1, Theorem 6.10]. It describes the structure of Statlib's ProbabilityTheory.effectiveSet S (the measures under which every e-variable for S has ∫⁻ X ≤ 1) for any set of measures on any measurable space, with no dominating measure, and proves [RW, Theorem 6.10]: powered tests exist exactly outside the effective null.

Roadmap: EValues

Here is how the two bullets are covered, in LMLExplore/EValues/EffectiveSet.lean (namespace ProbabilityTheory, next to Statlib's definition):

• Mixtures: comp_mem_effectiveSet shows the effective null is closed under mixtures κ ∘ₘ π over a measure π of mass at most 1, when κ θ is π-a.e. in it. The roadmap's statement, mixtures of members of S, is comp_mem_effectiveSet_of_mem, derived from it. Underneath are mem_effectiveSet_of_mem, mem_effectiveSet_iff_of_mem (a member of S is in its effective null exactly when its mass is at most 1) and subset_effectiveSet.
• Convex hull: convex_effectiveSet (Convex ℝ≥0∞, the same convexity as Statlib's convex_isEVar) and convexHull_subset_effectiveSet.
• Solid: mem_effectiveSet_of_le.
• Closed under setwise convergence along any filter: mem_effectiveSet_of_frequently_of_forall_measure_le_liminf and mem_effectiveSet_of_forall_measure_le_liminf. These are the two forms of Mathlib's IsClosed.mem_of_frequently_of_tendsto / IsClosed.mem_of_tendsto. They assume only the lower bound μ s ≤ liminf (fun i ↦ μs i s) l on measurable sets, the hypothesis form of Mathlib's Portmanteau lemma; setwise convergence gives it through Tendsto.liminf_eq.
• Same e-variables: isEVar_effectiveSet_inter_iff says that for a null of probability measures, S and effectiveSet S ∩ {μ | IsProbabilityMeasure μ} have the same e-variables. Hence effectiveSet_effectiveSet_inter: the effective null of the latter is effectiveSet S again.
• Also included: monotonicity in the null, effectiveSet_mono, the "monotonicity in the null" lemma the Completion checks ask for.
• [RW, Theorem 6.10]: exists_powered_test_iff, with the statement of Suggested.lean, minus the unused [IsProbabilityMeasure Q]. Some measurable φ ≤ 1 of level α ∈ (0, 1) for S has α < ∫⁻ φ ∂Q exactly when Q ∉ effectiveSet S. The truncation step goes through mem_effectiveSet_iff_forall_bounded: for a null of finite measures, bounded e-variables are enough to test membership. Dividing a bounded e-variable by max C 2 then gives the test [RW, Fact 3.6]. The two halves of Fact 3.6 are separate lemmas: isEVar_inv_mul_of_lintegral_le (a test of level α, divided by α, is an e-variable) and IsEVar.lintegral_const_mul_le (∫⁻ c * X ∂P ≤ c * P univ for an e-variable X).

The closedness needs one general tool, which goes in its own file, LMLExplore/MeasureTheory/Integral/Lebesgue/Setwise.lean:

• MeasureTheory.lintegral_le_liminf_lintegral_of_forall_measure_le_liminf_measure is Fatou's lemma for varying measures, named after Mathlib's Portmanteau lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure. If μ s ≤ liminf (fun i ↦ μs i s) l for every measurable s (for instance under setwise convergence), then ∫⁻ f ∂μ ≤ liminf ∫⁻ f ∂μs i for every f : α → ℝ≥0∞, with no measurability or finiteness assumption.
• Its corollary lintegral_le_of_frequently_of_forall_measure_le_liminf_measure comes with it.
• The proof writes the integral as a supremum of finite-valued simple functions (lintegral_eq_nnreal). The simple-function step uses Tau Ceti's ENNReal.le_liminf_add (superadditivity of liminf in ℝ≥0∞) and Mathlib's ENNReal.liminf_const_mul_of_ne_top.

Before writing, I searched the pinned Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for duplicates:

• effectiveSet only appears in Statlib's EValues/RIPr.lean, which has the definition, mem_effectiveSet_iff, measure_univ_le_one_of_mem_effectiveSet, isFiniteMeasure_of_mem_effectiveSet and the duality. None of the statements here are there. The proofs reuse its IsEVar.lintegral_le_measure_univ, IsEVar.of_lintegral_le_one, IsEVar.anti_set and IsEVar.mono.
• For setwise convergence, the only hit was Tau Ceti's Vague.lean, which proves setwise convergence from vague convergence and has no integral bound. Mathlib's liminf bounds for integrals (lintegral_liminf_le', Portmanteau) vary the function or need weak convergence.
• Mixtures use Mathlib's Measure.lintegral_bind, and the truncation uses lintegral_iSup.

No public declaration is removed or renamed. The PR does not depend on the open EValues PRs #384, #385 and #388: it uses only Statlib's IsEVar and effectiveSet, and it touches disjoint files.

Milestone: EValues Layer 1.1. After this PR, what remains of Layer 1.1 is the dominated description of [LRR25, Lemma 4.5] through the Brannath–Schachermayer bipolar theorem, and its corollary for finite nulls [LRR25, Corollary 4.6]. Two later items consume this PR: Layer 1.2's criterion P* ∈ effectiveSet S, and Layer 3.2's closure of e-processes under the probability measures of effectiveSet S (through isEVar_effectiveSet_inter_iff).

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

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

🤖 Prepared with Claude Code

[RemyDegenne]

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

The setwise Fatou lemma and the two effective-null closedness lemmas built on it assume setwise convergence, but the proof only needs the Portmanteau-style lower bound μ s ≤ liminf μs i s. Every other statement is at the natural level.

• LMLExplore/MeasureTheory/Integral/Lebesgue/Setwise.lean:42 — lintegral_le_liminf_of_tendsto_measure assumes Tendsto (fun i ↦ μs i s) l (𝓝 (μ s)), but the conclusion only needs μ s ≤ liminf (fun i ↦ μs i s) l for measurable s. That is the hypothesis form of Mathlib's analogous Portmanteau lemma. The same over-strong hypothesis is in lintegral_le_of_frequently_of_tendsto_measure (Setwise.lean:63), mem_effectiveSet_of_frequently_of_tendsto (EffectiveSet.lean:131) and mem_effectiveSet_of_tendsto (EffectiveSet.lean:140). Fix: Take h : ∀ s, MeasurableSet s → μ s ≤ liminf (fun i ↦ μs i s) l. For a nontrivial l, prove the simple-function step by Finset induction with le_liminf_add and ENNReal.liminf_const_mul_of_ne_top instead of tendsto_finsetSum. Propagate the weaker hypothesis to the corollary and both effective-null closedness lemmas; the convergent case follows from Tendsto.liminf_eq.

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 · 67s · 289.3k in (267.9k cache read, 21.4k cache write) / 5.7k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

Proofs are short, robust and free of defeq tricks, but exists_powered_test_iff inlines the test ↔ e-variable conversion it cites as [RW, Fact 3.6] and repeats the same multiplication-by-inverse sequence in both directions.

• LMLExplore/EValues/EffectiveSet.lean:190 — exists_powered_test_iff (~45 lines) inlines two reusable facts: a level-α test scaled by α⁻¹ is an e-variable (forward direction), and a bounded e-variable X ≤ C scaled by (max C 2)⁻¹ is a test of level (max C 2)⁻¹ (reverse direction, cited inline as [RW, Fact 3.6]). Both directions repeat the same lintegral_const_mul/gcongr/ENNReal.inv_mul_cancel/ENNReal.mul_lt_mul_right sequence. Fix: Pull these out as two lemmas, e.g. IsEVar.of_test (φ of level α ≠ 0, ∞ gives IsEVar (α⁻¹ * φ) S) and IsEVar.test_of_le (X ≤ D, D ≠ 0, ∞, gives D⁻¹ * X ≤ 1 with ∫⁻ D⁻¹ * X ∂P ≤ D⁻¹). Then prove the theorem from them, plus a shared D⁻¹ < D⁻¹ * ∫⁻ X ∂Q ↔ 1 < ∫⁻ X ∂Q step.

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 · 21s · 43.8k in (38.5k cache read, 5.3k cache write) / 2k 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	All new statements match the roadmap's Layer 1.1 bullets and [RW, Theorem 6.10], and the mixture, Fatou and powered-test statements generalise them; I tested edge cases (S = ∅, trivial filter, a null measure Q) and none was vacuous or mis-stated.
✅	reuse	approved	claude/claude-opus-5-5	No located Mathlib or LMLExplore declaration replaces any new lemma: the setwise Fatou lemma differs from lintegral_liminf_le' (varying functions) and the Portmanteau open-set bound (topological, continuous f, ℕ-indexed), and the proofs reuse lintegral_mono', Measure.lintegral_bind, convexHull_min, lintegral_eq_nnreal, lintegral_iSup and ENNReal.iSup_natCast. Statlib source was not available in the checkout, so overlap with RIPr.lean could not be independently grepped.
✅	scope	approved	claude/claude-opus-5-5	This PR covers the first two bullets of EValues Layer 1.1 'The effective null' (README.md:312-322), and the target is getting closer. The setwise Fatou lemma in Setwise.lean is a direct prerequisite for the closedness bullet, so the PR is a single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The informal sources ([RW] Theorem 6.10, Fact 3.6 and §6.3.1; [LRR25] Definition 3.1) are cited in the module docstring and next to the relevant declarations, and they match the roadmap milestone's sources. The setwise Fatou lemma is a routine supremum-of-simple-functions argument that follows no identifiable source needing credit.
✅	api-design	approved	claude/claude-opus-5-5	The new surface is the roadmap's Layer 1.1 products plus reusable lemmas, and the general setwise-Fatou result is public in its own MeasureTheory file. No definitions, exposed bodies, compatibility artifacts or missing characteristic annotations.
🟡	generality	changes requested	claude/claude-opus-5-5	The setwise Fatou lemma and the two effective-null closedness lemmas built on it assume setwise convergence, but the proof only needs the Portmanteau-style lower bound μ s ≤ liminf μs i s. Every other statement is at the natural level.
✅	placement	approved	claude/claude-opus-5-5	The effective-null structure results sit in a new EValues file built on Statlib's definition, and the general setwise Fatou lemma sits in the matching generic Lebesgue-integral directory. Every import is specific and used.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in the existing Statlib effectiveSet terminology, _iff/equality names match their statements, and exists_powered_test_iff keeps the roadmap name; no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Both new files have module docstrings that state their content and purpose, and every public declaration's docstring matches its statement without describing the proof, project process, or claiming more than is proved. References stay in the file; roadmap attribution is only in the PR description.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	Proofs are short, robust and free of defeq tricks, but exists_powered_test_iff inlines the test ↔ e-variable conversion it cites as [RW, Fact 3.6] and repeats the same multiplication-by-inverse sequence in both directions.

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

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

[lmlexplore-automation]

Closing automatically: this PR authors the same roadmap target (effective-null) as the older open #389. The queue housekeeping keeps the earlier PR and closes this duplicate to avoid redundant review. The branch is kept; add the keep label if it is intentionally distinct.