[RemyDegenne]

This pull request adds admissible e-variables, with the parts of the target that need no further theory. It adds one new file, LMLExplore/EValues/Admissible.lean (240 lines), and changes no existing file.

The definitions

• ProbabilityTheory.IsAdmissibleEVar E S is a structure extending Statlib's IsEVar E S with one field: every e-variable F for S with E ≤ᵐ[P] F for all P ∈ S has F ≤ᵐ[P] E for all P ∈ S. The definition of [RW, Definition 2.11], with domination everywhere, is isAdmissibleEVar_iff_forall_le.
• ProbabilityTheory.IsStronglyAdmissibleEVar E S extends IsEVar E S with: every measurable set charged by some member of S is charged by a member P of S with ∫⁻ E ∂P = P univ. This is the sufficient condition of [RW, Corollary 2.15 (a)], as the roadmap names it; for probability measures the integral condition is expectation one.

Main declarations

• IsAdmissibleEVar.ae_le, IsAdmissibleEVar.ae_eq, IsAdmissibleEVar.congr: the elimination forms, and invariance under almost sure equality.
• isAdmissibleEVar_iff_forall_le: IsAdmissibleEVar E S ↔ IsEVar E S ∧ ∀ F, IsEVar F S → E ≤ F → ∀ P ∈ S, F =ᵐ[P] E.
• IsStronglyAdmissibleEVar.isAdmissibleEVar: for a null of finite measures, strongly admissible implies admissible [RW, Corollary 2.15 (a)].
• IsExactEVar.isStronglyAdmissibleEVar and IsExactEVar.isAdmissibleEVar: exact e-variables (LMLExplore's IsExactEVar) are strongly admissible, hence admissible for a null of finite measures.
• IsAdmissibleEVar.isExactEVar_singleton and isAdmissibleEVar_singleton_iff: for a simple null {P} with P finite, admissible and exact coincide [RW, Proposition 2.12].
• isExactEVar_singleton_iff_exists_rnDeriv: the exact e-variables for {P} are the measurable functions P-almost surely equal to Q.rnDeriv P for a measure Q ≪ P with Q univ = P univ [RW, Proposition 2.12].
• IsStronglyAdmissibleEVar.prod: the product fun p ↦ E p.1 * F p.2 of two strongly admissible e-variables is strongly admissible for Set.image2 Measure.prod S T, for nulls of finite measures [RW, Proposition 2.17].

Roadmap coverage (EValues, Layer 0, item 5)

Covered:

• the definition of an admissible e-variable;
• the simple null: admissible and exact coincide, and exact e-variables are likelihood ratios [RW, Proposition 2.12];
• strong admissibility, that it implies admissibility, and its stability under products [RW, Corollary 2.15 (a), Proposition 2.17].

Left for later pull requests:

• the characterization of [RW, Theorem 2.14] by the liminf condition;
• the other sufficient conditions of [RW, Corollary 2.15], derived from the characterization;
• the necessary condition of [RW, Proposition 2.13].

This pull request shares no content with the open #399, #401, #402 and #403.

Notes for reviewers

• The definition asks for domination almost surely under every member of the null, not everywhere. The two forms are equivalent (isAdmissibleEVar_iff_forall_le: replace F by max E F), and the almost sure form is the one that later statements produce.
• Exactness and strong admissibility use the normalization ∫⁻ E ∂P = P univ of IsExactEVar, so the statements hold for nulls of finite measures, not only of probability measures. The hypotheses ∀ P ∈ S, IsFiniteMeasure P are used: Statlib's IsEVar gives ∫⁻ E ∂P ≤ P univ, which says nothing for an infinite measure.
• The paper project uses IsAdmissibleEVar in a statement on nulls generated by constraints, which will follow once feat: nulls generated by constraints, their bets, and the complete class theorem for finitely many constraints #402 is merged.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R5

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

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

The two new definitions and their results are new material and mostly reuse existing API (isExactEVar_rnDeriv, Measure.rnDeriv_withDensity, lintegral_prod_mul). One proof re-derives Mathlib's ae_eq_of_ae_le_of_lintegral_le through subtraction.

• LMLExplore/EValues/Admissible.lean:134 — Lines 134-141 of IsStronglyAdmissibleEVar.isAdmissibleEVar show by hand that E =ᵐ[P] F from E ≤ᵐ[P] F and ∫⁻ F ∂P ≤ ∫⁻ E ∂P < ∞, going through lintegral_sub, lintegral_eq_zero_iff and tsub_eq_zero_iff_le. Mathlib already has this as a lemma. Fix: Use have h_eq := ae_eq_of_ae_le_of_lintegral_le (hEF P hP) (by rw [hPE]; exact measure_ne_top P univ) hF.measurable.aemeasurable (by rw [hPE]; exact hF.lintegral_le_measure_univ P hP), then close with hPA (ae_iff.1 (h_eq.mono fun ω hω ↦ by simp [hω])) or similar. This removes h_sub, the rw ... at h_sub step and h_le.

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 · 40s · 210.6k in (190.8k cache read, 19.8k cache write) / 3.4k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

IsStronglyAdmissibleEVar lacks part of its characterizing API: an a.s.-invariance (congr) lemma and the form with expectation one for probability nulls that the roadmap uses.

• LMLExplore/EValues/Admissible.lean:115 — No IsStronglyAdmissibleEVar.congr, although the file proves IsAdmissibleEVar.congr and IsExactEVar.congr exists; consumers must unfold the structure to move along a.s. equality. Fix: Add IsStronglyAdmissibleEVar.congr (hE : IsStronglyAdmissibleEVar E S) (hF : Measurable F) (hEF : ∀ P ∈ S, E =ᵐ[P] F) : IsStronglyAdmissibleEVar F S, via hE.toIsEVar.congr and lintegral_congr_ae.
• LMLExplore/EValues/Admissible.lean:115 — Roadmap item 5 states strong admissibility with ∫⁻ E ∂P = 1, but the API offers only the P univ form; there is nothing for probability nulls like isExactEVar_iff / IsExactEVar.of_lintegral_eq_one. Fix: Add isStronglyAdmissibleEVar_iff (hS : ∀ P ∈ S, IsProbabilityMeasure P) : IsStronglyAdmissibleEVar E S ↔ IsEVar E S ∧ ∀ A, MeasurableSet A → (∃ P ∈ S, P A ≠ 0) → ∃ P ∈ S, P A ≠ 0 ∧ ∫⁻ ω, E ω ∂P = 1 (plus an of_lintegral_eq_one constructor).

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 · 27s · 76.5k in (60.6k cache read, 15.9k cache write) / 2.5k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

Most proofs are readable and robust, but IsStronglyAdmissibleEVar.prod relies on an undocumented definitional equality between f ⁻¹' {0}ᶜ and Function.support f. It also repeats the same 'the product charges A iff the slice set is charged' step four times, which should be one helper lemma.

• LMLExplore/EValues/Admissible.lean:219 — hE.exists_lintegral_eq _ (hB (measurableSet_singleton 0).compl) produces facts about (fun x ↦ P' (Prod.mk x ⁻¹' A)) ⁻¹' {0}ᶜ, and the proof consumes them as 0 < P₁ (Function.support _) through lintegral_pos_iff_support (lines 221, 225). This relies on an undocumented definitional equality between the preimage of {0}ᶜ and Function.support. The same happens at line 229, consumed at lines 231 and 236. Fix: Use measurableSet_support hB and measurableSet_support hC so the sets appear syntactically as Function.support _, or add a comment that explains the coercion.
• LMLExplore/EValues/Admissible.lean:220 — The step 'the product charges A iff the set of points whose slice of A is charged has positive measure' is proved inline four times. Each copy is a chain of Measure.prod_apply/prod_apply_symm, lintegral_pos_iff_support and pos_iff_ne_zero (lines 220–221, 223–225, 230–231, 235–236). This hides a reusable fact and makes the proof brittle. Fix: Factor out lemmas such as prod_apply_ne_zero_iff (hA : MeasurableSet A) : μ.prod ν A ≠ 0 ↔ μ {x | ν (Prod.mk x ⁻¹' A) ≠ 0} ≠ 0 and its symmetric version, for example from Measure.measure_prod_null, and use them at each site.

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 · 44s · 111.8k in (103.3k cache read, 8.5k cache write) / 3.5k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[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	The definitions match RW Definition 2.11 and the hypothesis of Corollary 2.15 (a), and the singleton characterization (Proposition 2.12) and the product stability statement (Proposition 2.17) are faithful, with the finiteness hypotheses genuinely needed; I tried to break each statement and found no degenerate or vacuous case.
✅	reuse	approved	claude/claude-opus-5-5	The admissible and strongly admissible e-variable API is new; nothing like it exists in LMLExplore or Mathlib (Statlib was not in the checkout, so it went unsearched), and the proofs reuse existing lemmas (isExactEVar_rnDeriv, IsExactEVar.congr, ae_eq_of_ae_le_of_lintegral_le, Measure.rnDeriv_withDensity, lintegral_prod_mul). The new prod_apply_ne_zero_iff lemmas restate Mathlib's measure_prod_null with Function.support, the form IsStronglyAdmissibleEVar.prod needs, and do not duplicate an existing declaration.
✅	scope	approved	claude/claude-opus-5-5	The PR directly advances EValues Layer 0 item 5 (Admissibility, README.md:287-299): definition, strong admissibility, Corollary 2.15(a), simple-null Proposition 2.12 and the product result of Proposition 2.17. It is one coherent unit, and the Prod.lean lemmas are prerequisites used by IsStronglyAdmissibleEVar.prod.
✅	attribution	approved	claude/claude-opus-5-5	Every result in the new file credits its matching item in Ramdas–Wang (Definition 2.11, Proposition 2.12, Corollary 2.15 (a), Proposition 2.17), and the Statlib and project definitions it builds on are named. The two product-measure helper lemmas are routine Mathlib rewrites that need no credit.
✅	api-design	approved	claude/claude-opus-5-5	The surface is minimal and well placed: both new structures carry introduction, elimination, congr and iff characterizations, and the general product-measure lemmas are public in LMLExplore/MeasureTheory/Measure/Prod.lean. Nothing duplicates existing API, and there is no compatibility layer and no exposed body.
✅	generality	approved	claude/claude-opus-5-5	Every hypothesis is used or required by the lemma it calls (isExactEVar_rnDeriv, prod_apply, prod_apply_symm), and the probability-measure lemmas are corollaries of the general P univ-normalized form. No unused or overly strong hypotheses and no special-case re-proofs.
✅	placement	approved	claude/claude-opus-5-5	Admissible.lean sits correctly in EValues/ next to EVariable.lean, and the generic product-measure positivity lemmas belong in LMLExplore/MeasureTheory/Measure/Prod.lean. All three imports are used and none is too broad.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions and match the neighbouring IsExactEVar and Measure.prod_apply_symm names; every _iff lemma is a genuine equivalence, the namespace matches IsExactEVar, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstrings and all public declaration docstrings in Admissible.lean and the Prod.lean additions match their statements and hypotheses, cite [RW] correctly, and do not overclaim. They contain no roadmap or process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, use targeted rewrites and filter_upwards, have no change/show or undocumented defeq, and factor the repeated product-slice reasoning into the two prod_apply_ne_zero_iff lemmas. No proof-quality issues found.

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

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