[RemyDegenne]

This PR builds on the numeraire file that #411 merged (LMLExplore/EValues/Numeraire.lean, [LRR25, Theorem 4.1]). It adds the material from the roadmap item that is not on main yet: absolute continuity with respect to a set of measures, the e-variable characterization of it [LRR25, Theorem 2.6], the verification theorem under the weaker hypothesis that the candidate numeraire is almost surely finite, the dominated criterion [LRR25, Theorem 4.7], and the identification of the reverse information projection from a likelihood ratio.

Roadmap target: EValues, Layer 1, item 2, Identifying numeraires [LRR25, Theorem 2.6, Theorem 4.1, Corollary 4.2, Theorem 4.7; RW, Theorem 6.15].

Roadmap: EValues

Contents:

• MeasureTheory.Measure.AbsolutelyContinuousSet Q S (new file LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean) is the Q ≪ S of [LRR25]: every measurable set that is null for every member of S is Q-null. Its API: absolutelyContinuousSet_iff, measure_eq_zero, ae_of_forall_ae, absolutelyContinuous (transfer to a dominating measure), mono, @[simp] absolutelyContinuousSet_singleton_iff (it is Q ≪ P for {P}), AbsolutelyContinuous.trans_absolutelyContinuousSet and AbsolutelyContinuous.absolutelyContinuousSet.
• In EVariable.lean: isEVar_piecewise_top (the e-variable that is ∞ on a null set and 1 elsewhere), AbsolutelyContinuousSet.ae_ne_top, and absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top: Q ≪ S holds exactly when every e-variable is Q-almost surely finite [LRR25, Theorem 2.6].
• In EffectiveSet.lean: absolutelyContinuousSet_of_mem_effectiveSet. measure_eq_zero_of_mem_effectiveSet and absolutelyContinuous_of_mem_effectiveSet are now derived from the shared lemmas, and their statements are unchanged.
• In Numeraire.lean:
  • withDensity_inv_mem_effectiveSet_iff: Q.withDensity X⁻¹ is in the effective null exactly when ∫⁻ Y / X ∂Q ≤ 1 for every e-variable Y.
  • isNumeraire_of_withDensity_inv_mem_effectiveSet, and the verification theorem isNumeraire_iff_withDensity_inv_mem_effectiveSet, now assume only that X is Q-almost surely finite (hX_top). This is weaker than Q ≪ S, which implies it through AbsolutelyContinuousSet.ae_ne_top.
  • ripr_eq_of_isEVar_rnDeriv: a member R of the effective null that is equivalent to Q, whose likelihood ratio Q.rnDeriv R is an e-variable, is the reverse information projection. ripr_singleton_eq is its special case for simple nulls.
  • isNumeraire_div_rnDeriv_iff: the dominated criterion ∫⁻ p / r ∂Q ≤ 1 ∀ P ∈ S [LRR25, Theorem 4.7], for any σ-finite reference measure.

Changes to declarations already on main (from #411):

• Removed ProbabilityTheory.IsEVar.ae_ne_top_of_forall_measure_eq_zero. Use MeasureTheory.Measure.AbsolutelyContinuousSet.ae_ne_top instead: hX.ae_ne_top_of_forall_measure_eq_zero hQS becomes hQS.ae_ne_top hX.
• Replaced ProbabilityTheory.IsEVar.measure_fsupport_eq_measure_univ (which assumed IsFiniteMeasure Q, IsEVar X S and Q ≪ S) with ProbabilityTheory.measure_fsupport_eq_measure_univ (hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞) (hX₀ : ∀ᵐ ω ∂Q, X ω ≠ 0) : Q X.fsupport = Q univ, which needs no other hypothesis: hX.measure_fsupport_eq_measure_univ hQS hX₀ becomes measure_fsupport_eq_measure_univ (hQS.ae_ne_top hX) hX₀. isNumeraire_of_withDensity_inv_mem_effectiveSet now uses it instead of repeating its proof.
• The hypothesis hQS : ∀ s, MeasurableSet s → (∀ P ∈ S, P s = 0) → Q s = 0 is now hQS : Q.AbsolutelyContinuousSet S in absolutelyContinuous_ripr, IsNumeraire.eq_withDensity_inv_of_le and isNumeraire_iff_exists_ae_eq_rnDeriv.
• These three are generalised: isNumeraire_iff_withDensity_inv_mem_effectiveSet, isNumeraire_of_lintegral_div_le_one and ripr_mem_of_lintegral_div_le_one. Each one replaces the hypotheses hQS (and hX₀ for the first) with hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞, and callers pass hQS.ae_ne_top hX.

Several declarations in this PR's earlier version duplicated declarations that #411 put on main, so they were dropped in favour of the main versions:

• IsNumeraire.ripr_eq_withDensity duplicated IsNumeraire.ripr_eq.
• AbsolutelyContinuousSet.absolutelyContinuous_ripr duplicated absolutelyContinuous_ripr.
• isNumeraire_iff_isEVar_of_ae_eq_rnDeriv and isNumeraire_rnDeriv_iff duplicated isNumeraire_of_ae_eq_rnDeriv.
• isNumeraire_iff_isEVar_of_withDensity_inv_le duplicated isNumeraire_of_smul_withDensity_inv_le.
• isNumeraire_rnDeriv_singleton duplicated isNumeraire_rnDeriv.
• IsEVar.isNumeraire_of_generating duplicated isNumeraire_of_lintegral_div_le_one and ripr_mem_of_lintegral_div_le_one.

The proofs reuse Statlib's isNumeraire_iff, isNumeraire_of_lintegral_div_le, IsNumeraire.ae_unique, rnDeriv_ripr, ripr_mem_effectiveSet and absolutelyContinuous_ripr_of_ae_ne_top. From Mathlib they use Measure.inv_rnDeriv, Measure.rnDeriv_eq_div, lintegral_rnDeriv_mul and withDensity_rnDeriv_le. From LMLExplore they use lintegral_withDensity_inv_eq_lintegral_div and mem_effectiveSet_of_le. No formalization was vendored.

Verification: the shared local checks (tauceti-local-checks verify --policy ordinary) pass at 39f9a4e (merged with main at ddb0c29). They report scope: scoped: against ddb0c29ede5c0e178f175e983edbeb22c06a9c07 and local-axioms: checked 4 changed module(s), 83 declaration(s); 0 violation(s). These are local checks, and CI verifies the pushed PR.

🤖 Generated with Claude Code

[RemyDegenne]

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

The docstrings match their statements, except the module-level summary of the dominated criterion in Numeraire.lean, which leaves r undefined and drops the hypotheses on R.

• LMLExplore/EValues/Numeraire.lean:55 — The Main-statements bullet for isNumeraire_div_rnDeriv_iff says 'with densities q, p and r with respect to a σ-finite reference measure, q / r is the numeraire exactly when ...' but never says that r is the density of a member R of the effective null with Q ≪ R. It also omits that S consists of probability measures, so it claims more than the theorem proves. Fix: Rewrite the bullet as '... with r the density of a member R of the effective null with Q ≪ R, for a null S of probability measures, q / r is the numeraire exactly when ∫⁻ p / r ∂Q ≤ 1 for every P ∈ S.'

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 · 28s · 67.1k in (59.6k cache read, 7.5k cache write) / 2.3k 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	AbsolutelyContinuousSet is LRR25's Q ≪ S, and the Theorem 2.6 iff, the a.s.-finite verification theorem (Theorem 4.1), the dominated criterion (Theorem 4.7), the generated-null criteria and the RIPr identifications match the source and only weaken hypotheses. Attempts to break them on degenerate cases (empty S, 0/0 and p/0 densities, sub-probability R) found no mismatch.
✅	reuse	approved	claude/claude-opus-5-5	The PR adds new material (set-wise absolute continuity, LRR25 Thm 2.6, the verification theorem under an a.s.-finite hypothesis, the dominated criterion, identification of the reverse information projection) and builds on existing lemmas (isEVar_piecewise_top replaces an inline proof; the new iff is built from existing lemmas); greps of Mathlib and LMLExplore found no duplicate. Statlib's source is not in the checkout, so for measure_fsupport_eq_measure_univ, ripr_eq_of_isEVar_rnDeriv and ripr_singleton_eq the absence of a Statlib duplicate rests on the PR description.
✅	scope	approved	claude/claude-opus-5-5	The PR directly advances EValues Layer 1 item 2 'Identifying numeraires' (roadmap/LMLRoadmaps/EValues/README.md:347). It adds the roadmap's Q ≪ S notion, the dominated criterion [LRR25, Theorem 4.7] and the identification of ripr from a likelihood ratio, and the edits to merged declarations only switch them to the new notion, keeping this one coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The material follows LRR25 (Theorems 2.6, 4.1, 4.7 and Corollary 4.2) and RW (Theorem 6.15), and both are cited in the module references and in the docstrings of the declarations that follow them. Nothing is vendored or closely followed without credit, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	AbsolutelyContinuousSet keeps its body hidden and has its full API (iff restatement, measure_eq_zero/ae_of_forall_ae elimination, mono, transitivity, dominating-measure transfer, introduction from a member, @[simp] singleton iff), and all callers go through it. The verification theorem and derived criteria are exposed under weakened hypotheses, and the removed declarations leave no compatibility aliases or shims.
✅	generality	approved	claude/claude-opus-5-5	Statements sit at the natural level: the verification theorem and Corollary 4.2 now assume only Q-a.s. finiteness of X, and the singleton and dominated-criterion results are derived from the general likelihood-ratio criterion. The new AbsolutelyContinuousSet notion has no Mathlib counterpart, and every extra hypothesis (probability null, R ≪ Q, finite null) is used in the proofs.
✅	placement	approved	claude/claude-opus-5-5	The new AbsolutelyContinuousSet.lean sits in MeasureTheory/Measure/ with a minimal Mathlib import, and each new e-variable, effective-null and numeraire declaration lives in its topical file. No sibling files need a subdirectory, and no import is unused or unnecessarily broad.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in the terminology of adjacent EffectiveSet/Statlib declarations, no _iff/_eq name overstates its statement, and AbsolutelyContinuousSet with its API lives in MeasureTheory.Measure (and Measure.AbsolutelyContinuous) so dot notation works. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new file has an accurate module docstring, the changed files' module docstrings are updated to match, and every new or changed public declaration has a docstring whose hypotheses match its statement (including the weaker hX_top assumption and the dominated criterion). The docstrings contain no roadmap or process material.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and robust: the null-set e-variable is factored once as isEVar_piecewise_top and reused, the a.s.-finite verification theorem is derived from measure_fsupport_eq_measure_univ, and the dominated criterion's rewrite chain is brief and commented. There are no brittle rewrite chains, no change or goal-changing show, and no undocumented definitional-equality manipulation.

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

_{Reviewing this diff at head 39f9a4e. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.83.}

[RemyDegenne]

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

IsEVar.measure_fsupport_eq_measure_univ keeps the stronger Q.AbsolutelyContinuousSet S hypothesis although it only uses the consequence that X is Q-almost surely finite, and isNumeraire_of_withDensity_inv_mem_effectiveSet re-proves the same full-support argument inline because the lemma is stated too strongly. The other new statements are at the right level of generality.

• LMLExplore/EValues/Numeraire.lean:182 — IsEVar.measure_fsupport_eq_measure_univ assumes hQS : Q.AbsolutelyContinuousSet S, but uses it only through hQS.ae_ne_top hX; it does not need IsEVar either, only Measurable X. This is inconsistent with the PR's own weakening of three other theorems to hX_top. Fix: Restate it as theorem measure_fsupport_eq_measure_univ [IsFiniteMeasure Q] (hX : Measurable X) (hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞) (hX₀ : ∀ᵐ ω ∂Q, X ω ≠ 0) : Q X.fsupport = Q univ. In IsNumeraire.eq_withDensity_inv_of_le (line 219), pass hQS.ae_ne_top hX.isEVar, or weaken that theorem to hX_top as well, since that is its only use of hQS.
• LMLExplore/EValues/Numeraire.lean:160 — isNumeraire_of_withDensity_inv_mem_effectiveSet re-proves the generalised lemma inline: its h_supp block (ae_iff_measure_eq hX.measurable_fsupport.nullMeasurableSet + filter_upwards [hX_top, hX_zero]) duplicates the body of measure_fsupport_eq_measure_univ. Fix: After generalising the lemma as above, replace the h_supp block with (hX.measurable.measure_fsupport_eq_measure_univ hX_top hX_zero).trans measure_univ, or the equivalent call.

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 · 28s · 70.9k in (59.6k cache read, 11.2k cache write) / 2.6k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}