[RemyDegenne]

This PR proves the structural properties of Statlib's effective null effectiveSet S for any null S : Set (Measure Ω) on any measurable space, with no dominating measure and no convexity. It adds LMLExplore/EValues/EffectiveSet.lean (251 lines, namespace ProbabilityTheory). It also adds the lower semicontinuity of ∫⁻ under setwise convergence (and under the weaker liminf hypothesis) to LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean (+61 lines). This is the EValues roadmap's Layer 1.1, The effective null [LRR25, Definition 3.1, Lemma 4.5, Corollary 4.6; RW, §6.3.1, Theorem 6.10].

Coverage of the milestone's bullets:

• Mixtures, convex hull, solidity, setwise closure, same e-variables (first bullet):
  • comp_mem_effectiveSet: κ ∘ₘ π ∈ effectiveSet S for π univ ≤ 1 and κ θ ∈ effectiveSet S for π-a.e. θ. Together with subset_effectiveSet this gives the roadmap's statement, a probability π and a kernel with values in S.
  • convex_effectiveSet is derived from comp_mem_effectiveSet through Kernel.boolKernel. convexHull_subset_effectiveSet follows from it.
  • isLowerSet_effectiveSet and mem_effectiveSet_of_le give solidity.
  • mem_effectiveSet_of_measure_le_liminf shows that μ ∈ effectiveSet S when μs i is eventually in it and μ s ≤ liminf μs i s for every measurable s, along any filter. Its corollary mem_effectiveSet_of_tendsto gives closedness under setwise convergence, so nets are covered as well as sequences.
  • isEVar_effectiveSet_inter_iff: S and effectiveSet S ∩ {μ | IsProbabilityMeasure μ} have the same e-variables. The direction that needs no hypothesis is IsEVar.effectiveSet_inter. The corollary effectiveSet_effectiveSet_inter says they have the same effective null.
• Tests against the effective null (second bullet): exists_powered_test_iff, under the roadmap's suggested name and signature [RW, Theorem 6.10], without its IsProbabilityMeasure Q hypothesis. Q ∉ effectiveSet S exactly when, for some α ∈ (0, 1), a measurable [0, 1]-valued φ with ∫⁻ φ ∂P ≤ α for all P ∈ S has α < ∫⁻ φ ∂Q. Its proof goes through exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet (for any null, a measure outside the effective null is detected by an e-variable bounded by some N ≥ 2, the truncation min X N), and then divides by the bound, as in [RW, Fact 3.6]. The test is stated explicitly rather than through a new predicate.
• Dominated case, first part (third bullet): absolutelyContinuous_of_mem_effectiveSet shows that the members of the effective null of a null dominated by ν are ≪ ν. It comes from measure_eq_zero_of_mem_effectiveSet: a measurable set null for every P ∈ S is null for every member of the effective null. This needs no finiteness of the members of S.
• API lemmas: effectiveSet_mono (monotonicity in the null) and subset_effectiveSet_iff (S ⊆ effectiveSet S ↔ ∀ P ∈ S, P univ ≤ 1).

The general lemma in Lebesgue/Add.lean is lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure. If μ s ≤ liminf μs i s along any filter for every measurable s (in particular under setwise convergence), then ∫⁻ f ∂μ ≤ liminf ∫⁻ f ∂μs i. It is proved through SimpleFunc.eapprox, using SimpleFunc.lintegral_le_liminf_lintegral (the same statement for simple functions with finite values, via Tau Ceti's ENNReal.sum_liminf_le_liminf_sum), and needs no countable generation of the filter. The file also has SimpleFunc.tendsto_lintegral_of_tendsto_measure, the continuity of the integral of such a simple function under setwise convergence. The main lemma is the measurable-set counterpart of Mathlib's portmanteau lemma lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure. mem_effectiveSet_of_measure_le_liminf consumes it.

Reuse: I searched the pinned Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for effectiveSet and for setwise-convergence statements of the form Tendsto (fun i ↦ μs i s). Statlib has only the definition, mem_effectiveSet_iff, measure_univ_le_one_of_mem_effectiveSet, isFiniteMeasure_of_mem_effectiveSet, ripr_mem_effectiveSet and the duality lemmas, which are consumed and not restated. Mathlib's setwise statements are π-system and portmanteau lemmas for probability measures, with no lower semicontinuity of ∫⁻. The proofs reuse Statlib's IsEVar.anti_set, IsEVar.congr, IsEVar.of_lintegral_le_one, IsEVar.lintegral_le_measure_univ and isEVar_one, and Mathlib's Measure.lintegral_bind, Kernel.boolKernel, Measure.comp_add, Measure.comp_smul, lintegral_eq_iSup_eapprox_lintegral and lintegral_tendsto_of_tendsto_of_monotone. The open PRs #384 (Layer 0.1) and #385 (Layer 2.1) touch LMLExplore/EValues/ but not the effective null. This PR does not depend on them. No public declaration is removed or renamed.

Milestone: EValues Layer 1.1. What remains after this PR is the dominated description of the effective null as the smallest convex, solid, closed-in-μ-probability set containing S [LRR25, Lemma 4.5], with the Brannath–Schachermayer bipolar theorem in L⁰₊(μ), and its finite-S corollary [LRR25, Corollary 4.6]. The facts proved here (convexity, solidity, absolute continuity) are the easy inclusions that Lemma 4.5 consumes.

Roadmap: EValues

🤖 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	Every new statement matches the roadmap's Layer 1.1 targets and cited sources with correct quantifiers and edge cases; exists_powered_test_iff is the roadmap signature minus [IsProbabilityMeasure Q], hence strictly stronger, and the setwise lower-semicontinuity lemma is true along arbitrary NeBot filters.
✅	reuse	approved	claude/claude-opus-5-5	No new declaration duplicates Mathlib or LMLExplore API: the nearest Mathlib result is the portmanteau lemma for open sets and sequences (Portmanteau.lean:497), which the new lemma for measurable sets along any filter does not restate, and IsEVar/effectiveSet appear nowhere else in LMLExplore. Statlib's source is absent from the checkout, so IsEVar.min_const and effectiveSet_mono could not be checked against it.
✅	scope	approved	claude/claude-opus-5-5	The PR directly advances EValues Layer 1.1 'The effective null' (README.md:312-329): it proves the full first bullet, the powered-test characterization under the roadmap's suggested name, and the absolute-continuity part of the dominated bullet. The Lebesgue/Add.lean lower-semicontinuity lemma is a proximate prerequisite consumed by mem_effectiveSet_of_measure_le_liminf, so the PR is a single topic.
✅	attribution	approved	claude/claude-opus-5-5	The code credits its informal sources ([LRR25] Definition 3.1 and Lemma 4.5; [RW] Fact 3.6, §6.3.1 and Theorem 6.10) on the declarations that follow them and in the module references, and names Mathlib's portmanteau lemma as the counterpart of its eapprox-based lower-semicontinuity proof. The roadmap is credited only in the PR description, and no uncredited source is evident.
✅	api-design	approved	claude/claude-opus-5-5	The surface is minimal: the general lower-semicontinuity infrastructure is public in its canonical Lebesgue file, the effective-null API (monotonicity, membership characterizations, convexity, solidity, closure, test duality) is complete, and nothing is needlessly private or exposed. @[gcongr] on effectiveSet_mono is the only annotation needed, and there is no compatibility layer.
✅	generality	approved	claude/claude-opus-5-5	General results are proved first and specialized afterwards (convexity comes from comp_mem_effectiveSet, setwise closure from the liminf version, and the Add.lean lemma holds along any filter for any measurable f). The remaining hypotheses (probability nulls, NeBot, finite simple-function values) are either needed or follow Mathlib convention.
✅	placement	approved	claude/claude-opus-5-5	The new EValues/EffectiveSet.lean is in the roadmap's suggested LMLExplore/EValues/ folder and imports the Statlib module that defines effectiveSet. The generic setwise lower-semicontinuity lemmas sit in Lebesgue/Add.lean, matching Mathlib's Add.lean where lintegral_eq_iSup_eapprox_lintegral lives, and both new imports there are used.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in standard Mathlib terminology, _iff names state an Iff and the equality name states an equality, dot-notation lemmas are in the SimpleFunc and IsEVar namespaces, and the main integral lemma copies the name pattern of Mathlib's portmanteau ..._of_forall_isOpen_measure_le_liminf_measure. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstrings of EffectiveSet.lean and the new Setwise section of Lebesgue/Add.lean match their statements, with the mass-at-most-1 and probability-measure hypotheses stated where they apply. Every public declaration has an accurate docstring that describes the result, not the proof or the project process.
✅	proof-quality	approved	claude/claude-opus-5-5	The prior finding is resolved: the truncation argument is now the standalone, commented lemma IsEVar.min_const, and exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet uses it. The remaining proofs are short or commented, use no change/show, and lean on simp/gcongr/fun_prop rather than brittle rewrite chains.

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

_{Reviewing this diff at head 2ff1ca4. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.42.}