From 718482e22073b7392dd4fd8e34ab936df8c21625 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 15 Nov 2026 11:54:57 +0100
Subject: [PATCH 1/6] feat: identifying numeraires through the effective null
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The verification theorem of Larsson, Ramdas and Ruf (LRR25, Theorem 4.1):
a Q-almost surely finite e-variable X is the numeraire exactly when
Q.withDensity X⁻¹ is in the effective null, which is then the reverse
information projection. With absolute continuity with respect to a set of
measures, the likelihood-ratio, dominated and generating-family criteria,
and the numeraire of a simple null.

Co-Authored-By: Claude Code <noreply@github.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 LMLExplore/EValues/Numeraire.lean | 340 ++++++++++++++++++++++++++++++
 1 file changed, 340 insertions(+)
 create mode 100644 LMLExplore/EValues/Numeraire.lean

diff --git a/LMLExplore/EValues/Numeraire.lean b/LMLExplore/EValues/Numeraire.lean
new file mode 100644
index 00000000..84f8e6f1
--- /dev/null
+++ b/LMLExplore/EValues/Numeraire.lean
@@ -0,0 +1,340 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import LMLExplore.EValues.EffectiveSet
+public import LMLExplore.EValues.EVariable
+
+/-!
+# Identifying numeraires through the effective null
+
+The numeraire of a null `S` under an alternative `Q` is Statlib's `IsNumeraire X S Q`: the
+e-variable `X` for which `∫⁻ Y / X ∂Q` is at most the `Q`-mass of `{0 < X < ∞}` for every
+e-variable `Y`, which is the log-optimal e-variable. Statlib proves that it exists and is unique;
+this file gives a way to recognise it. To an e-variable `X` that is `Q`-almost surely finite
+associate the measure `Q.withDensity X⁻¹`, under which every e-variable `Y` has expectation
+`∫⁻ Y / X ∂Q`. Then `X` is the numeraire exactly when this measure belongs to the effective null
+`effectiveSet S`, and it is then Statlib's reverse information projection `ripr Q S` [LRR25,
+Theorem 4.1]. In other words, the numeraire is the only e-variable that is the likelihood ratio of
+`Q` against an element of the effective null equivalent to `Q` [RW, Theorem 6.15].
+
+The finiteness of `X` is automatic when `Q` is absolutely continuous with respect to the null,
+`Q.AbsolutelyContinuousSet S`: every measurable set that is null for every member of `S` is
+`Q`-null. This holds exactly when every e-variable for `S` is `Q`-almost surely finite
+[LRR25, Theorem 2.6].
+
+The verification theorem turns the search for the numeraire into checking one integral inequality
+per e-variable, or per member of the null. For a likelihood ratio `Q.rnDeriv R` against a member
+`R` of the effective null, it suffices that the likelihood ratio is an e-variable; with densities
+`q`, `p` and `r` with respect to a reference measure, this is the dominated criterion
+`∫⁻ p / r ∂Q ≤ 1` for every `P ∈ S` [LRR25, Theorem 4.7]; and for a null described by a
+generating family of e-variables, it suffices to check the generating family [LRR25,
+Corollary 4.2]. The simple null `{P}` with `Q ≪ P`, whose numeraire is the likelihood ratio
+`Q.rnDeriv P` [RW, Theorem 3.20], is the first instance. No dominating measure, convexity or
+topology is assumed, except in the dominated criterion, which names its reference measure.
+
+## Main definitions
+
+* `MeasureTheory.Measure.AbsolutelyContinuousSet Q S`: every measurable set that is null for every
+  member of `S` is `Q`-null.
+
+## Main statements
+
+* `ProbabilityTheory.absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top`: `Q` is absolutely
+  continuous with respect to `S` exactly when every e-variable for `S` is `Q`-almost surely finite
+  [LRR25, Theorem 2.6].
+* `ProbabilityTheory.withDensity_inv_mem_effectiveSet_iff`: `Q.withDensity X⁻¹` is in the
+  effective null exactly when `∫⁻ Y / X ∂Q ≤ 1` for every e-variable `Y`.
+* `ProbabilityTheory.isNumeraire_iff_withDensity_inv_mem_effectiveSet`: **the verification
+  theorem** [LRR25, Theorem 4.1]: a `Q`-almost surely finite e-variable `X` is the numeraire
+  exactly when `Q.withDensity X⁻¹` is in the effective null.
+* `ProbabilityTheory.IsNumeraire.ripr_eq_withDensity`: the reverse information projection is then
+  `Q.withDensity X⁻¹`, and, for `Q` absolutely continuous with respect to the null, it is
+  equivalent to `Q` (`MeasureTheory.Measure.AbsolutelyContinuousSet.absolutelyContinuous_ripr`).
+* `ProbabilityTheory.isNumeraire_iff_exists_ae_eq_rnDeriv`: for `Q` absolutely continuous with
+  respect to the null, the numeraire is the only e-variable that is `Q`-almost surely the
+  likelihood ratio of `Q` against an element of the effective null equivalent to `Q`
+  [RW, Theorem 6.15].
+* `ProbabilityTheory.isNumeraire_rnDeriv_iff`, `ProbabilityTheory.ripr_eq_of_isEVar_rnDeriv`:
+  for `R` in the effective null with `Q ≪ R`, the likelihood ratio `Q.rnDeriv R` is the numeraire
+  as soon as it is an e-variable, and `R` is then the reverse information projection when `R ≪ Q`.
+* `ProbabilityTheory.isNumeraire_rnDeriv_singleton`: the likelihood ratio `Q.rnDeriv P` is the
+  numeraire of the simple null `{P}` when `Q ≪ P` [RW, Theorem 3.20]. Its expected logarithm is
+  Statlib's `maxUtility_singleton_eq_klDiv`.
+* `ProbabilityTheory.isNumeraire_div_rnDeriv_iff`: **the dominated criterion** [LRR25,
+  Theorem 4.7].
+* `ProbabilityTheory.IsEVar.isNumeraire_of_generating`: **the criterion with a generating family**
+  [LRR25, Corollary 4.2].
+
+## References
+
+* [LRR25] M. Larsson, A. Ramdas and J. Ruf, *The numeraire e-variable and reverse information
+  projection*, Ann. Statist. 53 (2025), arXiv:2402.18810v4, Theorem 2.6, Theorem 4.1,
+  Corollary 4.2 and Theorem 4.7.
+* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in
+  Statistics 1 (2025), arXiv:2410.23614v6, Theorems 3.20 and 6.15.
+-/
+
+public section
+
+open MeasureTheory Set
+
+open scoped ENNReal
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S T : Set (Measure Ω)} {P Q Q' R : Measure Ω}
+  {X : Ω → ℝ≥0∞}
+
+namespace MeasureTheory.Measure
+
+/-! ### Absolute continuity with respect to a set of measures -/
+
+/-- A measure `Q` is absolutely continuous with respect to a set of measures `S` when every
+measurable set that is null for every member of `S` is `Q`-null. For a singleton `{P}` this is
+`Q ≪ P` (`MeasureTheory.Measure.absolutelyContinuousSet_singleton_iff`). -/
+def AbsolutelyContinuousSet (Q : Measure Ω) (S : Set (Measure Ω)) : Prop :=
+  ∀ ⦃s : Set Ω⦄, MeasurableSet s → (∀ P ∈ S, P s = 0) → Q s = 0
+
+/-- The defining property of `MeasureTheory.Measure.AbsolutelyContinuousSet`. -/
+theorem absolutelyContinuousSet_iff :
+    Q.AbsolutelyContinuousSet S ↔
+      ∀ ⦃s : Set Ω⦄, MeasurableSet s → (∀ P ∈ S, P s = 0) → Q s = 0 :=
+  Iff.rfl
+
+/-- A measurable set that is null for every member of `S` is null for a measure absolutely
+continuous with respect to `S`. -/
+theorem AbsolutelyContinuousSet.measure_eq_zero (hQS : Q.AbsolutelyContinuousSet S) {s : Set Ω}
+    (hs : MeasurableSet s) (h : ∀ P ∈ S, P s = 0) : Q s = 0 :=
+  hQS hs h
+
+/-- Absolute continuity with respect to a set of measures is monotone in the set. -/
+theorem AbsolutelyContinuousSet.mono (hQS : Q.AbsolutelyContinuousSet S) (hST : S ⊆ T) :
+    Q.AbsolutelyContinuousSet T :=
+  fun _ hs h ↦ hQS hs fun P hP ↦ h P (hST hP)
+
+/-- A measure absolutely continuous with respect to a measure absolutely continuous with respect
+to `S` is absolutely continuous with respect to `S`. -/
+theorem AbsolutelyContinuous.trans_absolutelyContinuousSet (hQ'Q : Q' ≪ Q)
+    (hQS : Q.AbsolutelyContinuousSet S) : Q'.AbsolutelyContinuousSet S :=
+  fun _ hs h ↦ hQ'Q (hQS hs h)
+
+/-- Absolute continuity with respect to a singleton is absolute continuity. -/
+@[simp]
+theorem absolutelyContinuousSet_singleton_iff : Q.AbsolutelyContinuousSet {P} ↔ Q ≪ P :=
+  ⟨fun h ↦ .mk fun _ hs hPs ↦ h hs (by simpa using hPs), fun h _ _ hs ↦ h (hs P rfl)⟩
+
+/-- A measure absolutely continuous with respect to a member of `S` is absolutely continuous
+with respect to `S`. -/
+theorem AbsolutelyContinuous.absolutelyContinuousSet (hQP : Q ≪ P) (hP : P ∈ S) :
+    Q.AbsolutelyContinuousSet S :=
+  (absolutelyContinuousSet_singleton_iff.mpr hQP).mono (singleton_subset_iff.mpr hP)
+
+end MeasureTheory.Measure
+
+namespace ProbabilityTheory
+
+open Measure
+
+/-- Every member of the effective null of `S` is absolutely continuous with respect to `S`. -/
+theorem absolutelyContinuousSet_of_mem_effectiveSet (hμ : Q ∈ effectiveSet S) :
+    Q.AbsolutelyContinuousSet S :=
+  fun _ hs h ↦ measure_eq_zero_of_mem_effectiveSet hμ hs h
+
+/-- An e-variable for `S` is almost surely finite under a measure absolutely continuous with
+respect to `S` [LRR25, Theorem 2.6]. -/
+theorem _root_.MeasureTheory.Measure.AbsolutelyContinuousSet.ae_ne_top
+    (hQS : Q.AbsolutelyContinuousSet S) (hX : IsEVar X S) : ∀ᵐ ω ∂Q, X ω ≠ ∞ := by
+  refine ae_iff.mpr (hQS ?_ fun P hP ↦ ae_iff.mp (hX.ae_ne_top hP))
+  exact (measurableSet_singleton ∞).preimage hX.measurable |>.congr (by ext; simp)
+
+/-- A measure is absolutely continuous with respect to `S` exactly when every e-variable for `S`
+is almost surely finite under it [LRR25, Theorem 2.6]. -/
+theorem absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top :
+    Q.AbsolutelyContinuousSet S ↔ ∀ X, IsEVar X S → ∀ᵐ ω ∂Q, X ω ≠ ∞ := by
+  classical
+  refine ⟨fun hQS _ hX ↦ hQS.ae_ne_top hX, fun h s hs hS ↦ ?_⟩
+  -- The function equal to `∞` on `s` and to `1` elsewhere is an e-variable for `S`.
+  have hX : IsEVar (s.piecewise (fun _ ↦ ∞) 1) S :=
+    (isEVar_one S).congr (measurable_const.piecewise hs measurable_const) fun P hP ↦ by
+      filter_upwards [measure_eq_zero_iff_ae_notMem.mp (hS P hP)] with ω hω
+      simp [hω]
+  refine measure_mono_null (fun ω hω ↦ ?_) (ae_iff.mp (h _ hX))
+  simp [hω]
+
+/-! ### The verification theorem -/
+
+/-- The measure `Q.withDensity X⁻¹` is in the effective null exactly when every e-variable `Y`
+has `∫⁻ Y / X ∂Q ≤ 1`: under `Q.withDensity X⁻¹`, `Y` has expectation `∫⁻ Y / X ∂Q`. -/
+theorem withDensity_inv_mem_effectiveSet_iff (hX : Measurable X) :
+    Q.withDensity X⁻¹ ∈ effectiveSet S ↔ ∀ Y, IsEVar Y S → ∫⁻ ω, Y ω / X ω ∂Q ≤ 1 := by
+  refine forall₂_congr fun Y hY ↦ ?_
+  rw [lintegral_withDensity_eq_lintegral_mul _ hX.inv hY.measurable]
+  simp [ENNReal.div_eq_inv_mul]
+
+/-- The measure `Q.withDensity X⁻¹` of a numeraire `X` is in the effective null. -/
+theorem IsNumeraire.withDensity_inv_mem_effectiveSet [IsProbabilityMeasure Q]
+    (hX : IsNumeraire X S Q) : Q.withDensity X⁻¹ ∈ effectiveSet S :=
+  (withDensity_inv_mem_effectiveSet_iff hX.isEVar.measurable).mpr fun _ ↦ hX.lintegral_div_le_one
+
+/-- A `Q`-almost surely finite e-variable `X` for which `Q.withDensity X⁻¹` is in the effective
+null is the numeraire. -/
+theorem isNumeraire_of_withDensity_inv_mem_effectiveSet [IsProbabilityMeasure Q]
+    (hX : IsEVar X S) (hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞) (h : Q.withDensity X⁻¹ ∈ effectiveSet S) :
+    IsNumeraire X S Q := by
+  have h_div := (withDensity_inv_mem_effectiveSet_iff hX.measurable).mp h
+  -- The expectation of `X⁻¹` is finite, so that `X` is almost surely positive.
+  have hX_zero : ∀ᵐ ω ∂Q, X ω ≠ 0 := by
+    have h_inv : ∫⁻ ω, (X ω)⁻¹ ∂Q ≠ ∞ :=
+      ne_top_of_le_ne_top ENNReal.one_ne_top (by simpa using h_div 1 (isEVar_one S))
+    filter_upwards [ae_lt_top hX.measurable.inv h_inv] with ω hω
+    simpa using hω.ne
+  have h_supp : Q X.fsupport = 1 := by
+    rw [← prob_compl_eq_zero_iff hX.measurable_fsupport, Function.fsupport_compl,
+      ← nonpos_iff_eq_zero]
+    refine (measure_union_le _ _).trans ?_
+    simp only [nonpos_iff_eq_zero, add_eq_zero]
+    exact ⟨by simpa using ae_iff.mp hX_top, by simpa using ae_iff.mp hX_zero⟩
+  exact isNumeraire_of_lintegral_div_le hX (by simp [h_supp]) fun Y hY ↦ h_supp ▸ h_div Y hY
+
+/-- **The verification theorem** [LRR25, Theorem 4.1]: a `Q`-almost surely finite e-variable `X`
+is the numeraire exactly when `Q.withDensity X⁻¹` is in the effective null. For `Q` absolutely
+continuous with respect to the null, every e-variable is `Q`-almost surely finite
+(`MeasureTheory.Measure.AbsolutelyContinuousSet.ae_ne_top`). -/
+theorem isNumeraire_iff_withDensity_inv_mem_effectiveSet [IsProbabilityMeasure Q]
+    (hX : IsEVar X S) (hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞) :
+    IsNumeraire X S Q ↔ Q.withDensity X⁻¹ ∈ effectiveSet S :=
+  ⟨IsNumeraire.withDensity_inv_mem_effectiveSet,
+    isNumeraire_of_withDensity_inv_mem_effectiveSet hX hX_top⟩
+
+/-- A `Q`-almost surely finite `X` for which `Q.withDensity X⁻¹` lies below a member of the
+effective null is the numeraire as soon as it is an e-variable. -/
+theorem isNumeraire_iff_isEVar_of_withDensity_inv_le [IsProbabilityMeasure Q]
+    (hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞) (hR : R ∈ effectiveSet S) (h : Q.withDensity X⁻¹ ≤ R) :
+    IsNumeraire X S Q ↔ IsEVar X S :=
+  ⟨IsNumeraire.isEVar, fun hX ↦ isNumeraire_of_withDensity_inv_mem_effectiveSet hX hX_top
+    (mem_effectiveSet_of_le hR h)⟩
+
+/-- The reverse information projection of `Q` onto `S` is `Q.withDensity X⁻¹` for the numeraire
+`X` [LRR25, Theorem 4.1]. -/
+theorem IsNumeraire.ripr_eq_withDensity [IsFiniteMeasure Q] (hS : ∀ P ∈ S, IsFiniteMeasure P)
+    (hX : IsNumeraire X S Q) : ripr Q S = Q.withDensity X⁻¹ :=
+  withDensity_congr_ae <| (hX.ae_eq_numeraire hS).symm.mono fun ω hω ↦ by simp [hω]
+
+/-- For `Q` absolutely continuous with respect to a null of finite measures, `Q` is absolutely
+continuous with respect to its reverse information projection, so that the two are
+equivalent. -/
+theorem _root_.MeasureTheory.Measure.AbsolutelyContinuousSet.absolutelyContinuous_ripr
+    (hQS : Q.AbsolutelyContinuousSet S) : Q ≪ ripr Q S :=
+  absolutelyContinuous_ripr_of_ae_ne_top (hQS.ae_ne_top (isEVar_numeraire Q S))
+
+/-! ### Likelihood ratios against the effective null -/
+
+/-- For `R` in the effective null with `Q ≪ R`, the likelihood ratio `Q.rnDeriv R` is the
+numeraire exactly when it is an e-variable. -/
+theorem isNumeraire_rnDeriv_iff [IsProbabilityMeasure Q] (hR : R ∈ effectiveSet S)
+    (hQR : Q ≪ R) : IsNumeraire (Q.rnDeriv R) S Q ↔ IsEVar (Q.rnDeriv R) S := by
+  have := isFiniteMeasure_of_mem_effectiveSet hR
+  -- `Q.withDensity (Q.rnDeriv R)⁻¹ = Q.withDensity (R.rnDeriv Q)` lies below `R`.
+  exact isNumeraire_iff_isEVar_of_withDensity_inv_le (hQR.ae_le (rnDeriv_ne_top Q R)) hR
+    ((withDensity_congr_ae (inv_rnDeriv hQR)).trans_le (withDensity_rnDeriv_le R Q))
+
+/-- For `R` in the effective null equivalent to `Q`, if the likelihood ratio `Q.rnDeriv R` is an
+e-variable, then `R` is the reverse information projection of `Q` onto `S`. -/
+theorem ripr_eq_of_isEVar_rnDeriv [IsProbabilityMeasure Q] (hS : ∀ P ∈ S, IsFiniteMeasure P)
+    (hR : R ∈ effectiveSet S) (hQR : Q ≪ R) (hRQ : R ≪ Q) (hX : IsEVar (Q.rnDeriv R) S) :
+    ripr Q S = R := by
+  have := isFiniteMeasure_of_mem_effectiveSet hR
+  rw [((isNumeraire_rnDeriv_iff hR hQR).mpr hX).ripr_eq_withDensity hS,
+    withDensity_congr_ae (inv_rnDeriv hQR), withDensity_rnDeriv_eq R Q hRQ]
+
+/-- For `Q` absolutely continuous with respect to a null of finite measures, the numeraire is the
+only e-variable that is `Q`-almost surely the likelihood ratio of `Q` against an element of the
+effective null equivalent to `Q` [LRR25, Theorem 4.1; RW, Theorem 6.15]. -/
+theorem isNumeraire_iff_exists_ae_eq_rnDeriv [IsProbabilityMeasure Q]
+    (hS : ∀ P ∈ S, IsFiniteMeasure P) (hQS : Q.AbsolutelyContinuousSet S) :
+    IsNumeraire X S Q ↔
+      IsEVar X S ∧ ∃ R ∈ effectiveSet S, Q ≪ R ∧ R ≪ Q ∧ X =ᵐ[Q] Q.rnDeriv R := by
+  refine ⟨fun hX ↦ ⟨hX.isEVar, ripr Q S, ripr_mem_effectiveSet Q hS, hQS.absolutelyContinuous_ripr,
+    withDensity_absolutelyContinuous _ _, ?_⟩, fun ⟨hX, R, hR, hQR, _, hXR⟩ ↦ ?_⟩
+  · exact (hX.ae_eq_numeraire hS).trans
+      (rnDeriv_ripr hS (hQS.ae_ne_top (isEVar_numeraire Q S))).symm
+  · have := isFiniteMeasure_of_mem_effectiveSet hR
+    refine (isNumeraire_iff_isEVar_of_withDensity_inv_le (hQS.ae_ne_top hX) hR ?_).mpr hX
+    exact (withDensity_congr_ae (f := X⁻¹) (g := R.rnDeriv Q)
+      ((hXR.fun_comp Inv.inv).trans (inv_rnDeriv hQR))).trans_le (withDensity_rnDeriv_le R Q)
+
+/-- **The likelihood ratio is the numeraire of a simple null** [RW, Theorem 3.20]: for
+probability measures `Q ≪ P`, `Q.rnDeriv P` is the numeraire of `{P}` under `Q`. Its expected
+logarithm, the maximal expected logarithm of an e-variable for `{P}`, is `klDiv Q P` (Statlib's
+`ProbabilityTheory.maxUtility_singleton_eq_klDiv`). -/
+theorem isNumeraire_rnDeriv_singleton [IsProbabilityMeasure Q] [IsProbabilityMeasure P]
+    (hQP : Q ≪ P) : IsNumeraire (Q.rnDeriv P) {P} Q :=
+  (isNumeraire_rnDeriv_iff (subset_effectiveSet (by simp) rfl) hQP).mpr
+    (isExactEVar_rnDeriv hQP (by simp)).toIsEVar
+
+/-- For probability measures `Q ≪ P` with `P ≪ Q`, the reverse information projection of `Q`
+onto `{P}` is `P`. -/
+theorem ripr_singleton_eq [IsProbabilityMeasure Q] [IsProbabilityMeasure P] (hQP : Q ≪ P)
+    (hPQ : P ≪ Q) : ripr Q {P} = P :=
+  ripr_eq_of_isEVar_rnDeriv (by rintro _ rfl; infer_instance)
+    (subset_effectiveSet (by simp) rfl) hQP hPQ (isExactEVar_rnDeriv hQP (by simp)).toIsEVar
+
+/-! ### The dominated criterion -/
+
+/-- **The dominated criterion** [LRR25, Theorem 4.7]. Let `Q` and the members of a null `S` of
+probability measures be absolutely continuous with respect to a σ-finite measure `μ`, with
+densities `q` and `p`, and let `R` be a member of the effective null with density `r` and
+`Q ≪ R`. Then `q / r` is the numeraire exactly when `∫⁻ p / r ∂Q ≤ 1` for every `P ∈ S`. -/
+theorem isNumeraire_div_rnDeriv_iff [IsProbabilityMeasure Q] {μ : Measure Ω} [SigmaFinite μ]
+    (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hSμ : ∀ P ∈ S, P ≪ μ) (hQμ : Q ≪ μ)
+    (hR : R ∈ effectiveSet S) (hQR : Q ≪ R) :
+    IsNumeraire (fun ω ↦ Q.rnDeriv μ ω / R.rnDeriv μ ω) S Q ↔
+      ∀ P ∈ S, ∫⁻ ω, P.rnDeriv μ ω / R.rnDeriv μ ω ∂Q ≤ 1 := by
+  have := isFiniteMeasure_of_mem_effectiveSet hR
+  have hRμ : R ≪ μ := absolutelyContinuous_of_mem_effectiveSet hR hSμ
+  have hX_meas : Measurable fun ω ↦ Q.rnDeriv μ ω / R.rnDeriv μ ω := by fun_prop
+  -- `q / r` is `Q`-almost surely the likelihood ratio `Q.rnDeriv R`.
+  have h_eq : (fun ω ↦ Q.rnDeriv μ ω / R.rnDeriv μ ω) =ᵐ[Q] Q.rnDeriv R :=
+    hQR.ae_le (rnDeriv_eq_div hQμ hRμ).symm
+  have hX_top : ∀ᵐ ω ∂Q, Q.rnDeriv μ ω / R.rnDeriv μ ω ≠ ∞ := by
+    filter_upwards [h_eq, hQR.ae_le (rnDeriv_ne_top Q R)] with ω h h_top
+    rwa [h]
+  have h_le : Q.withDensity (fun ω ↦ Q.rnDeriv μ ω / R.rnDeriv μ ω)⁻¹ ≤ R :=
+    (withDensity_congr_ae (f := (fun ω ↦ Q.rnDeriv μ ω / R.rnDeriv μ ω)⁻¹) (g := R.rnDeriv Q)
+      ((h_eq.fun_comp Inv.inv).trans (inv_rnDeriv hQR))).trans_le (withDensity_rnDeriv_le R Q)
+  rw [isNumeraire_iff_isEVar_of_withDensity_inv_le hX_top hR h_le, isEVar_iff_lintegral_le_one hS,
+    and_iff_right hX_meas]
+  refine forall₂_congr fun P hP ↦ ?_
+  have := hS P hP
+  -- `∫⁻ q / r ∂P = ∫⁻ p * (q / r) ∂μ = ∫⁻ q * (p / r) ∂μ = ∫⁻ p / r ∂Q`.
+  rw [← lintegral_rnDeriv_mul (hSμ P hP) hX_meas.aemeasurable,
+    ← lintegral_rnDeriv_mul hQμ
+      (by fun_prop : Measurable fun ω ↦ P.rnDeriv μ ω / R.rnDeriv μ ω).aemeasurable]
+  simp_rw [div_eq_mul_inv, mul_left_comm (P.rnDeriv μ _)]
+
+/-! ### Generating families -/
+
+/-- **The criterion with a generating family** [LRR25, Corollary 4.2]. Let `𝓔₀` be a family of
+measurable functions that generates the null `S`, in the sense that every probability measure
+under which each member of `𝓔₀` has expectation at most `1` is in `S`. A `Q`-almost surely finite
+e-variable `X` with `∫⁻ X⁻¹ ∂Q = 1` and `∫⁻ Y / X ∂Q ≤ 1` for every `Y ∈ 𝓔₀` is the numeraire,
+and `Q.withDensity X⁻¹`, the reverse information projection when `S` consists of finite
+measures, belongs to `S`. -/
+theorem IsEVar.isNumeraire_of_generating [IsProbabilityMeasure Q] {𝓔₀ : Set (Ω → ℝ≥0∞)}
+    (h𝓔₀ : ∀ Y ∈ 𝓔₀, Measurable Y)
+    (hS : ∀ P : Measure Ω, IsProbabilityMeasure P → (∀ Y ∈ 𝓔₀, ∫⁻ ω, Y ω ∂P ≤ 1) → P ∈ S)
+    (hX : IsEVar X S) (hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞) (hX_inv : ∫⁻ ω, (X ω)⁻¹ ∂Q = 1)
+    (hX_div : ∀ Y ∈ 𝓔₀, ∫⁻ ω, Y ω / X ω ∂Q ≤ 1) :
+    IsNumeraire X S Q ∧ Q.withDensity X⁻¹ ∈ S := by
+  have : IsProbabilityMeasure (Q.withDensity X⁻¹) :=
+    ⟨by rw [withDensity_apply _ .univ, setLIntegral_univ]; exact hX_inv⟩
+  have h_mem : Q.withDensity X⁻¹ ∈ S := hS _ this fun Y hY ↦ by
+    rw [lintegral_withDensity_eq_lintegral_mul _ hX.measurable.inv (h𝓔₀ Y hY)]
+    simpa [ENNReal.div_eq_inv_mul] using hX_div Y hY
+  -- As a probability measure of `S`, `Q.withDensity X⁻¹` is in the effective null.
+  refine ⟨isNumeraire_of_withDensity_inv_mem_effectiveSet hX hX_top fun Y hY ↦ ?_, h_mem⟩
+  simpa using hY.lintegral_le_measure_univ _ h_mem
+
+end ProbabilityTheory

From f330864f8bcbb4c7828f4bd52b9808cc543f4c3e Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 15 Nov 2026 12:22:21 +0100
Subject: [PATCH 2/6] refactor: move AbsolutelyContinuousSet to measure theory
 and share likelihood-ratio lemmas

Move `MeasureTheory.Measure.AbsolutelyContinuousSet` and its basic API to
`LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean`, adding
`AbsolutelyContinuousSet.ae_of_forall_ae` and
`AbsolutelyContinuousSet.absolutelyContinuous`. Move
`absolutelyContinuousSet_of_mem_effectiveSet` to `EffectiveSet.lean`, factor out
`isEVar_piecewise_top`, and derive `ae_ne_top` and
`absolutelyContinuous_of_mem_effectiveSet` from the new lemmas. Add
`isNumeraire_iff_isEVar_of_ae_eq_rnDeriv`, from which the likelihood-ratio
criteria follow, unfold `ripr` explicitly, and fix the docstrings' hypotheses.

Co-Authored-By: Claude Code <noreply@github.com>
---
 LMLExplore/EValues/EffectiveSet.lean          |  29 +++-
 LMLExplore/EValues/Numeraire.lean             | 157 ++++++------------
 .../Measure/AbsolutelyContinuousSet.lean      | 100 +++++++++++
 3 files changed, 172 insertions(+), 114 deletions(-)
 create mode 100644 LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean

diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean
index 039a2cbb..bddce8b3 100644
--- a/LMLExplore/EValues/EffectiveSet.lean
+++ b/LMLExplore/EValues/EffectiveSet.lean
@@ -7,6 +7,7 @@ module
 
 public import Statlib.EValues.RIPr
 public import LMLExplore.MeasureTheory.Integral.Lebesgue.Add
+public import LMLExplore.MeasureTheory.Measure.AbsolutelyContinuousSet
 
 /-!
 # The effective null
@@ -40,6 +41,9 @@ measures `S`.
 * `ProbabilityTheory.isEVar_effectiveSet_inter_iff`: for a null `S` of probability measures, `S`
   and the probability measures of its effective null have the same e-variables, and hence
   (`ProbabilityTheory.effectiveSet_effectiveSet_inter`) the same effective null.
+* `ProbabilityTheory.absolutelyContinuousSet_of_mem_effectiveSet`: every member of the effective
+  null is absolutely continuous with respect to `S`
+  (`MeasureTheory.Measure.AbsolutelyContinuousSet`).
 * `ProbabilityTheory.absolutelyContinuous_of_mem_effectiveSet`: if every member of `S` is
   absolutely continuous with respect to `μ`, so is every member of the effective null.
 * `ProbabilityTheory.exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet`: a measure outside the
@@ -137,29 +141,36 @@ theorem mem_effectiveSet_of_tendsto {ι : Type*} {l : Filter ι} [l.NeBot] {μs
     μ ∈ effectiveSet S :=
   mem_effectiveSet_of_measure_le_liminf hμs fun s hs ↦ (h s hs).liminf_eq.ge
 
+/-- For a measurable set `s` that is null for every member of `S`, the function equal to `∞` on
+`s` and to `1` elsewhere is an e-variable for `S`. -/
+theorem isEVar_piecewise_top {s : Set Ω} [DecidablePred (· ∈ s)] (hs : MeasurableSet s)
+    (hS : ∀ P ∈ S, P s = 0) : IsEVar (s.piecewise (fun _ ↦ ∞) 1) S :=
+  (isEVar_one S).congr (measurable_const.piecewise hs measurable_const) fun P hP ↦ by
+    filter_upwards [measure_eq_zero_iff_ae_notMem.mp (hS P hP)] with ω hω
+    simp [hω]
+
 /-- A measurable set that is null for every member of `S` is null for every member of the
 effective null of `S`. -/
 theorem measure_eq_zero_of_mem_effectiveSet (hμ : μ ∈ effectiveSet S) {s : Set Ω}
     (hs : MeasurableSet s) (hS : ∀ P ∈ S, P s = 0) : μ s = 0 := by
   classical
-  -- The function equal to `∞` on `s` and to `1` elsewhere is an e-variable for `S`.
-  have hX : IsEVar (s.piecewise (fun _ ↦ ∞) 1) S :=
-    (isEVar_one S).congr (measurable_const.piecewise hs measurable_const) fun P hP ↦ by
-      filter_upwards [measure_eq_zero_iff_ae_notMem.mp (hS P hP)] with ω hω
-      simp [hω]
   have h : ∞ * μ s ≤ 1 := by
     rw [← lintegral_indicator_const hs]
-    refine (lintegral_mono fun ω ↦ ?_).trans (hμ _ hX)
+    refine (lintegral_mono fun ω ↦ ?_).trans (hμ _ (isEVar_piecewise_top hs hS))
     by_cases hω : ω ∈ s <;> simp [hω]
   by_contra h_ne
   simp [ENNReal.top_mul h_ne] at h
 
+/-- Every member of the effective null of `S` is absolutely continuous with respect to `S`. -/
+theorem absolutelyContinuousSet_of_mem_effectiveSet (hμ : μ ∈ effectiveSet S) :
+    μ.AbsolutelyContinuousSet S :=
+  Measure.absolutelyContinuousSet_iff.mpr fun _ hs h ↦ measure_eq_zero_of_mem_effectiveSet hμ hs h
+
 /-- If every member of `S` is absolutely continuous with respect to a measure `ν`, so is every
 member of the effective null of `S`. -/
 theorem absolutelyContinuous_of_mem_effectiveSet (hμ : μ ∈ effectiveSet S)
-    (hS : ∀ P ∈ S, P ≪ ν) : μ ≪ ν := by
-  refine Measure.AbsolutelyContinuous.mk fun s hs hνs ↦ ?_
-  exact measure_eq_zero_of_mem_effectiveSet hμ hs fun P hP ↦ hS P hP hνs
+    (hS : ∀ P ∈ S, P ≪ ν) : μ ≪ ν :=
+  (absolutelyContinuousSet_of_mem_effectiveSet hμ).absolutelyContinuous hS
 
 /-- An e-variable for `S` is an e-variable for the probability measures of the effective null of
 `S`. -/
diff --git a/LMLExplore/EValues/Numeraire.lean b/LMLExplore/EValues/Numeraire.lean
index 84f8e6f1..060fd427 100644
--- a/LMLExplore/EValues/Numeraire.lean
+++ b/LMLExplore/EValues/Numeraire.lean
@@ -7,6 +7,7 @@ module
 
 public import LMLExplore.EValues.EffectiveSet
 public import LMLExplore.EValues.EVariable
+public import LMLExplore.MeasureTheory.Measure.AbsolutelyContinuousSet
 
 /-!
 # Identifying numeraires through the effective null
@@ -17,14 +18,16 @@ e-variable `Y`, which is the log-optimal e-variable. Statlib proves that it exis
 this file gives a way to recognise it. To an e-variable `X` that is `Q`-almost surely finite
 associate the measure `Q.withDensity X⁻¹`, under which every e-variable `Y` has expectation
 `∫⁻ Y / X ∂Q`. Then `X` is the numeraire exactly when this measure belongs to the effective null
-`effectiveSet S`, and it is then Statlib's reverse information projection `ripr Q S` [LRR25,
-Theorem 4.1]. In other words, the numeraire is the only e-variable that is the likelihood ratio of
-`Q` against an element of the effective null equivalent to `Q` [RW, Theorem 6.15].
+`effectiveSet S`, and, when the members of `S` are finite measures, it is then Statlib's reverse
+information projection `ripr Q S` [LRR25, Theorem 4.1]. When `Q` is absolutely continuous with
+respect to a null of finite measures, the numeraire is the only e-variable that is the likelihood
+ratio of `Q` against an element of the effective null equivalent to `Q` [RW, Theorem 6.15].
 
 The finiteness of `X` is automatic when `Q` is absolutely continuous with respect to the null,
-`Q.AbsolutelyContinuousSet S`: every measurable set that is null for every member of `S` is
-`Q`-null. This holds exactly when every e-variable for `S` is `Q`-almost surely finite
-[LRR25, Theorem 2.6].
+`Q.AbsolutelyContinuousSet S`, defined in
+`LMLExplore.MeasureTheory.Measure.AbsolutelyContinuousSet`: every measurable set that is null for
+every member of `S` is `Q`-null. This holds exactly when every e-variable for `S` is `Q`-almost
+surely finite [LRR25, Theorem 2.6].
 
 The verification theorem turns the search for the numeraire into checking one integral inequality
 per e-variable, or per member of the null. For a likelihood ratio `Q.rnDeriv R` against a member
@@ -36,11 +39,6 @@ Corollary 4.2]. The simple null `{P}` with `Q ≪ P`, whose numeraire is the lik
 `Q.rnDeriv P` [RW, Theorem 3.20], is the first instance. No dominating measure, convexity or
 topology is assumed, except in the dominated criterion, which names its reference measure.
 
-## Main definitions
-
-* `MeasureTheory.Measure.AbsolutelyContinuousSet Q S`: every measurable set that is null for every
-  member of `S` is `Q`-null.
-
 ## Main statements
 
 * `ProbabilityTheory.absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top`: `Q` is absolutely
@@ -51,16 +49,19 @@ topology is assumed, except in the dominated criterion, which names its referenc
 * `ProbabilityTheory.isNumeraire_iff_withDensity_inv_mem_effectiveSet`: **the verification
   theorem** [LRR25, Theorem 4.1]: a `Q`-almost surely finite e-variable `X` is the numeraire
   exactly when `Q.withDensity X⁻¹` is in the effective null.
-* `ProbabilityTheory.IsNumeraire.ripr_eq_withDensity`: the reverse information projection is then
-  `Q.withDensity X⁻¹`, and, for `Q` absolutely continuous with respect to the null, it is
-  equivalent to `Q` (`MeasureTheory.Measure.AbsolutelyContinuousSet.absolutelyContinuous_ripr`).
+* `ProbabilityTheory.IsNumeraire.ripr_eq_withDensity`: for a null of finite measures, the reverse
+  information projection is then `Q.withDensity X⁻¹`, and, for `Q` absolutely continuous with
+  respect to the null, `Q` is absolutely continuous with respect to it
+  (`MeasureTheory.Measure.AbsolutelyContinuousSet.absolutelyContinuous_ripr`).
 * `ProbabilityTheory.isNumeraire_iff_exists_ae_eq_rnDeriv`: for `Q` absolutely continuous with
-  respect to the null, the numeraire is the only e-variable that is `Q`-almost surely the
-  likelihood ratio of `Q` against an element of the effective null equivalent to `Q`
+  respect to a null of finite measures, the numeraire is the only e-variable that is `Q`-almost
+  surely the likelihood ratio of `Q` against an element of the effective null equivalent to `Q`
   [RW, Theorem 6.15].
-* `ProbabilityTheory.isNumeraire_rnDeriv_iff`, `ProbabilityTheory.ripr_eq_of_isEVar_rnDeriv`:
-  for `R` in the effective null with `Q ≪ R`, the likelihood ratio `Q.rnDeriv R` is the numeraire
-  as soon as it is an e-variable, and `R` is then the reverse information projection when `R ≪ Q`.
+* `ProbabilityTheory.isNumeraire_iff_isEVar_of_ae_eq_rnDeriv`,
+  `ProbabilityTheory.isNumeraire_rnDeriv_iff`, `ProbabilityTheory.ripr_eq_of_isEVar_rnDeriv`:
+  for `R` in the effective null with `Q ≪ R`, a function `Q`-almost surely equal to the likelihood
+  ratio `Q.rnDeriv R` is the numeraire as soon as it is an e-variable, and `R` is then the reverse
+  information projection when `R ≪ Q`.
 * `ProbabilityTheory.isNumeraire_rnDeriv_singleton`: the likelihood ratio `Q.rnDeriv P` is the
   numeraire of the simple null `{P}` when `Q ≪ P` [RW, Theorem 3.20]. Its expected logarithm is
   Statlib's `maxUtility_singleton_eq_klDiv`.
@@ -84,83 +85,27 @@ open MeasureTheory Set
 
 open scoped ENNReal
 
-variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S T : Set (Measure Ω)} {P Q Q' R : Measure Ω}
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S : Set (Measure Ω)} {P Q R : Measure Ω}
   {X : Ω → ℝ≥0∞}
 
-namespace MeasureTheory.Measure
-
-/-! ### Absolute continuity with respect to a set of measures -/
-
-/-- A measure `Q` is absolutely continuous with respect to a set of measures `S` when every
-measurable set that is null for every member of `S` is `Q`-null. For a singleton `{P}` this is
-`Q ≪ P` (`MeasureTheory.Measure.absolutelyContinuousSet_singleton_iff`). -/
-def AbsolutelyContinuousSet (Q : Measure Ω) (S : Set (Measure Ω)) : Prop :=
-  ∀ ⦃s : Set Ω⦄, MeasurableSet s → (∀ P ∈ S, P s = 0) → Q s = 0
-
-/-- The defining property of `MeasureTheory.Measure.AbsolutelyContinuousSet`. -/
-theorem absolutelyContinuousSet_iff :
-    Q.AbsolutelyContinuousSet S ↔
-      ∀ ⦃s : Set Ω⦄, MeasurableSet s → (∀ P ∈ S, P s = 0) → Q s = 0 :=
-  Iff.rfl
-
-/-- A measurable set that is null for every member of `S` is null for a measure absolutely
-continuous with respect to `S`. -/
-theorem AbsolutelyContinuousSet.measure_eq_zero (hQS : Q.AbsolutelyContinuousSet S) {s : Set Ω}
-    (hs : MeasurableSet s) (h : ∀ P ∈ S, P s = 0) : Q s = 0 :=
-  hQS hs h
-
-/-- Absolute continuity with respect to a set of measures is monotone in the set. -/
-theorem AbsolutelyContinuousSet.mono (hQS : Q.AbsolutelyContinuousSet S) (hST : S ⊆ T) :
-    Q.AbsolutelyContinuousSet T :=
-  fun _ hs h ↦ hQS hs fun P hP ↦ h P (hST hP)
-
-/-- A measure absolutely continuous with respect to a measure absolutely continuous with respect
-to `S` is absolutely continuous with respect to `S`. -/
-theorem AbsolutelyContinuous.trans_absolutelyContinuousSet (hQ'Q : Q' ≪ Q)
-    (hQS : Q.AbsolutelyContinuousSet S) : Q'.AbsolutelyContinuousSet S :=
-  fun _ hs h ↦ hQ'Q (hQS hs h)
-
-/-- Absolute continuity with respect to a singleton is absolute continuity. -/
-@[simp]
-theorem absolutelyContinuousSet_singleton_iff : Q.AbsolutelyContinuousSet {P} ↔ Q ≪ P :=
-  ⟨fun h ↦ .mk fun _ hs hPs ↦ h hs (by simpa using hPs), fun h _ _ hs ↦ h (hs P rfl)⟩
-
-/-- A measure absolutely continuous with respect to a member of `S` is absolutely continuous
-with respect to `S`. -/
-theorem AbsolutelyContinuous.absolutelyContinuousSet (hQP : Q ≪ P) (hP : P ∈ S) :
-    Q.AbsolutelyContinuousSet S :=
-  (absolutelyContinuousSet_singleton_iff.mpr hQP).mono (singleton_subset_iff.mpr hP)
-
-end MeasureTheory.Measure
-
 namespace ProbabilityTheory
 
 open Measure
 
-/-- Every member of the effective null of `S` is absolutely continuous with respect to `S`. -/
-theorem absolutelyContinuousSet_of_mem_effectiveSet (hμ : Q ∈ effectiveSet S) :
-    Q.AbsolutelyContinuousSet S :=
-  fun _ hs h ↦ measure_eq_zero_of_mem_effectiveSet hμ hs h
-
 /-- An e-variable for `S` is almost surely finite under a measure absolutely continuous with
 respect to `S` [LRR25, Theorem 2.6]. -/
 theorem _root_.MeasureTheory.Measure.AbsolutelyContinuousSet.ae_ne_top
-    (hQS : Q.AbsolutelyContinuousSet S) (hX : IsEVar X S) : ∀ᵐ ω ∂Q, X ω ≠ ∞ := by
-  refine ae_iff.mpr (hQS ?_ fun P hP ↦ ae_iff.mp (hX.ae_ne_top hP))
-  exact (measurableSet_singleton ∞).preimage hX.measurable |>.congr (by ext; simp)
+    (hQS : Q.AbsolutelyContinuousSet S) (hX : IsEVar X S) : ∀ᵐ ω ∂Q, X ω ≠ ∞ :=
+  hQS.ae_of_forall_ae ((measurableSet_singleton ∞).compl.preimage hX.measurable)
+    fun _ hP ↦ hX.ae_ne_top hP
 
 /-- A measure is absolutely continuous with respect to `S` exactly when every e-variable for `S`
 is almost surely finite under it [LRR25, Theorem 2.6]. -/
 theorem absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top :
     Q.AbsolutelyContinuousSet S ↔ ∀ X, IsEVar X S → ∀ᵐ ω ∂Q, X ω ≠ ∞ := by
   classical
-  refine ⟨fun hQS _ hX ↦ hQS.ae_ne_top hX, fun h s hs hS ↦ ?_⟩
-  -- The function equal to `∞` on `s` and to `1` elsewhere is an e-variable for `S`.
-  have hX : IsEVar (s.piecewise (fun _ ↦ ∞) 1) S :=
-    (isEVar_one S).congr (measurable_const.piecewise hs measurable_const) fun P hP ↦ by
-      filter_upwards [measure_eq_zero_iff_ae_notMem.mp (hS P hP)] with ω hω
-      simp [hω]
-  refine measure_mono_null (fun ω hω ↦ ?_) (ae_iff.mp (h _ hX))
+  refine ⟨fun hQS _ hX ↦ hQS.ae_ne_top hX, fun h ↦ absolutelyContinuousSet_iff.mpr fun s hs hS ↦ ?_⟩
+  refine measure_mono_null (fun ω hω ↦ ?_) (ae_iff.mp (h _ (isEVar_piecewise_top hs hS)))
   simp [hω]
 
 /-! ### The verification theorem -/
@@ -219,26 +164,37 @@ theorem isNumeraire_iff_isEVar_of_withDensity_inv_le [IsProbabilityMeasure Q]
 /-- The reverse information projection of `Q` onto `S` is `Q.withDensity X⁻¹` for the numeraire
 `X` [LRR25, Theorem 4.1]. -/
 theorem IsNumeraire.ripr_eq_withDensity [IsFiniteMeasure Q] (hS : ∀ P ∈ S, IsFiniteMeasure P)
-    (hX : IsNumeraire X S Q) : ripr Q S = Q.withDensity X⁻¹ :=
-  withDensity_congr_ae <| (hX.ae_eq_numeraire hS).symm.mono fun ω hω ↦ by simp [hω]
+    (hX : IsNumeraire X S Q) : ripr Q S = Q.withDensity X⁻¹ := by
+  rw [ripr]
+  exact withDensity_congr_ae <| (hX.ae_eq_numeraire hS).symm.mono fun ω hω ↦ by simp [hω]
 
-/-- For `Q` absolutely continuous with respect to a null of finite measures, `Q` is absolutely
-continuous with respect to its reverse information projection, so that the two are
-equivalent. -/
+/-- For `Q` absolutely continuous with respect to `S`, `Q` is absolutely continuous with respect
+to its reverse information projection onto `S`. The reverse `ripr Q S ≪ Q` holds because
+`ripr Q S` is a measure with density with respect to `Q` (`withDensity_absolutelyContinuous`). -/
 theorem _root_.MeasureTheory.Measure.AbsolutelyContinuousSet.absolutelyContinuous_ripr
     (hQS : Q.AbsolutelyContinuousSet S) : Q ≪ ripr Q S :=
   absolutelyContinuous_ripr_of_ae_ne_top (hQS.ae_ne_top (isEVar_numeraire Q S))
 
 /-! ### Likelihood ratios against the effective null -/
 
+/-- For `R` in the effective null with `Q ≪ R`, a function `X` that is `Q`-almost surely the
+likelihood ratio `Q.rnDeriv R` is the numeraire exactly when it is an e-variable. -/
+theorem isNumeraire_iff_isEVar_of_ae_eq_rnDeriv [IsProbabilityMeasure Q] (hR : R ∈ effectiveSet S)
+    (hQR : Q ≪ R) (hXR : X =ᵐ[Q] Q.rnDeriv R) : IsNumeraire X S Q ↔ IsEVar X S := by
+  have := isFiniteMeasure_of_mem_effectiveSet hR
+  have hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞ := by
+    filter_upwards [hXR, hQR.ae_le (rnDeriv_ne_top Q R)] with ω h h_top
+    rwa [h]
+  -- `Q.withDensity X⁻¹ = Q.withDensity (R.rnDeriv Q)` lies below `R`.
+  exact isNumeraire_iff_isEVar_of_withDensity_inv_le hX_top hR
+    ((withDensity_congr_ae (f := X⁻¹) (g := R.rnDeriv Q)
+      ((hXR.fun_comp Inv.inv).trans (inv_rnDeriv hQR))).trans_le (withDensity_rnDeriv_le R Q))
+
 /-- For `R` in the effective null with `Q ≪ R`, the likelihood ratio `Q.rnDeriv R` is the
 numeraire exactly when it is an e-variable. -/
 theorem isNumeraire_rnDeriv_iff [IsProbabilityMeasure Q] (hR : R ∈ effectiveSet S)
-    (hQR : Q ≪ R) : IsNumeraire (Q.rnDeriv R) S Q ↔ IsEVar (Q.rnDeriv R) S := by
-  have := isFiniteMeasure_of_mem_effectiveSet hR
-  -- `Q.withDensity (Q.rnDeriv R)⁻¹ = Q.withDensity (R.rnDeriv Q)` lies below `R`.
-  exact isNumeraire_iff_isEVar_of_withDensity_inv_le (hQR.ae_le (rnDeriv_ne_top Q R)) hR
-    ((withDensity_congr_ae (inv_rnDeriv hQR)).trans_le (withDensity_rnDeriv_le R Q))
+    (hQR : Q ≪ R) : IsNumeraire (Q.rnDeriv R) S Q ↔ IsEVar (Q.rnDeriv R) S :=
+  isNumeraire_iff_isEVar_of_ae_eq_rnDeriv hR hQR .rfl
 
 /-- For `R` in the effective null equivalent to `Q`, if the likelihood ratio `Q.rnDeriv R` is an
 e-variable, then `R` is the reverse information projection of `Q` onto `S`. -/
@@ -257,13 +213,10 @@ theorem isNumeraire_iff_exists_ae_eq_rnDeriv [IsProbabilityMeasure Q]
     IsNumeraire X S Q ↔
       IsEVar X S ∧ ∃ R ∈ effectiveSet S, Q ≪ R ∧ R ≪ Q ∧ X =ᵐ[Q] Q.rnDeriv R := by
   refine ⟨fun hX ↦ ⟨hX.isEVar, ripr Q S, ripr_mem_effectiveSet Q hS, hQS.absolutelyContinuous_ripr,
-    withDensity_absolutelyContinuous _ _, ?_⟩, fun ⟨hX, R, hR, hQR, _, hXR⟩ ↦ ?_⟩
-  · exact (hX.ae_eq_numeraire hS).trans
-      (rnDeriv_ripr hS (hQS.ae_ne_top (isEVar_numeraire Q S))).symm
-  · have := isFiniteMeasure_of_mem_effectiveSet hR
-    refine (isNumeraire_iff_isEVar_of_withDensity_inv_le (hQS.ae_ne_top hX) hR ?_).mpr hX
-    exact (withDensity_congr_ae (f := X⁻¹) (g := R.rnDeriv Q)
-      ((hXR.fun_comp Inv.inv).trans (inv_rnDeriv hQR))).trans_le (withDensity_rnDeriv_le R Q)
+    by rw [ripr]; exact withDensity_absolutelyContinuous _ _, ?_⟩,
+    fun ⟨hX, R, hR, hQR, _, hXR⟩ ↦ (isNumeraire_iff_isEVar_of_ae_eq_rnDeriv hR hQR hXR).mpr hX⟩
+  exact (hX.ae_eq_numeraire hS).trans
+    (rnDeriv_ripr hS (hQS.ae_ne_top (isEVar_numeraire Q S))).symm
 
 /-- **The likelihood ratio is the numeraire of a simple null** [RW, Theorem 3.20]: for
 probability measures `Q ≪ P`, `Q.rnDeriv P` is the numeraire of `{P}` under `Q`. Its expected
@@ -298,13 +251,7 @@ theorem isNumeraire_div_rnDeriv_iff [IsProbabilityMeasure Q] {μ : Measure Ω} [
   -- `q / r` is `Q`-almost surely the likelihood ratio `Q.rnDeriv R`.
   have h_eq : (fun ω ↦ Q.rnDeriv μ ω / R.rnDeriv μ ω) =ᵐ[Q] Q.rnDeriv R :=
     hQR.ae_le (rnDeriv_eq_div hQμ hRμ).symm
-  have hX_top : ∀ᵐ ω ∂Q, Q.rnDeriv μ ω / R.rnDeriv μ ω ≠ ∞ := by
-    filter_upwards [h_eq, hQR.ae_le (rnDeriv_ne_top Q R)] with ω h h_top
-    rwa [h]
-  have h_le : Q.withDensity (fun ω ↦ Q.rnDeriv μ ω / R.rnDeriv μ ω)⁻¹ ≤ R :=
-    (withDensity_congr_ae (f := (fun ω ↦ Q.rnDeriv μ ω / R.rnDeriv μ ω)⁻¹) (g := R.rnDeriv Q)
-      ((h_eq.fun_comp Inv.inv).trans (inv_rnDeriv hQR))).trans_le (withDensity_rnDeriv_le R Q)
-  rw [isNumeraire_iff_isEVar_of_withDensity_inv_le hX_top hR h_le, isEVar_iff_lintegral_le_one hS,
+  rw [isNumeraire_iff_isEVar_of_ae_eq_rnDeriv hR hQR h_eq, isEVar_iff_lintegral_le_one hS,
     and_iff_right hX_meas]
   refine forall₂_congr fun P hP ↦ ?_
   have := hS P hP
diff --git a/LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean b/LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean
new file mode 100644
index 00000000..ca39d322
--- /dev/null
+++ b/LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean
@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
+
+/-!
+# Absolute continuity with respect to a set of measures
+
+A measure `Q` is absolutely continuous with respect to a set of measures `S`,
+`Q.AbsolutelyContinuousSet S`, when every measurable set that is null for every member of `S` is
+`Q`-null. For a singleton `{P}` this is `Q ≪ P`. This is the condition `Q ≪ S` under which the
+e-variables for a null `S` are `Q`-almost surely finite [LRR25, Theorem 2.6].
+
+## Main definitions
+
+* `MeasureTheory.Measure.AbsolutelyContinuousSet Q S`: every measurable set that is null for every
+  member of `S` is `Q`-null.
+
+## Main statements
+
+* `MeasureTheory.Measure.AbsolutelyContinuousSet.ae_of_forall_ae`: a property of the points of a
+  measurable set that holds almost surely under every member of `S` holds `Q`-almost surely.
+* `MeasureTheory.Measure.AbsolutelyContinuousSet.absolutelyContinuous`: `Q` is absolutely
+  continuous with respect to every measure that dominates all members of `S`.
+* `MeasureTheory.Measure.absolutelyContinuousSet_singleton_iff`: absolute continuity with respect
+  to `{P}` is `Q ≪ P`.
+
+## References
+
+* [LRR25] M. Larsson, A. Ramdas and J. Ruf, *The numeraire e-variable and reverse information
+  projection*, Ann. Statist. 53 (2025), arXiv:2402.18810v4, Theorem 2.6.
+-/
+
+public section
+
+open MeasureTheory Set
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S T : Set (Measure Ω)} {P Q Q' ν : Measure Ω}
+
+namespace MeasureTheory.Measure
+
+/-- A measure `Q` is absolutely continuous with respect to a set of measures `S` when every
+measurable set that is null for every member of `S` is `Q`-null. For a singleton `{P}` this is
+`Q ≪ P` (`MeasureTheory.Measure.absolutelyContinuousSet_singleton_iff`). -/
+def AbsolutelyContinuousSet (Q : Measure Ω) (S : Set (Measure Ω)) : Prop :=
+  ∀ ⦃s : Set Ω⦄, MeasurableSet s → (∀ P ∈ S, P s = 0) → Q s = 0
+
+/-- The defining property of `MeasureTheory.Measure.AbsolutelyContinuousSet`. -/
+theorem absolutelyContinuousSet_iff :
+    Q.AbsolutelyContinuousSet S ↔
+      ∀ ⦃s : Set Ω⦄, MeasurableSet s → (∀ P ∈ S, P s = 0) → Q s = 0 :=
+  Iff.rfl
+
+/-- A measurable set that is null for every member of `S` is null for a measure absolutely
+continuous with respect to `S`. -/
+theorem AbsolutelyContinuousSet.measure_eq_zero (hQS : Q.AbsolutelyContinuousSet S) {s : Set Ω}
+    (hs : MeasurableSet s) (h : ∀ P ∈ S, P s = 0) : Q s = 0 :=
+  hQS hs h
+
+/-- A property of the points of a measurable set that holds almost surely under every member
+of `S` holds almost surely under a measure absolutely continuous with respect to `S`. This is the
+counterpart of `MeasureTheory.Measure.AbsolutelyContinuous.ae_le`. -/
+theorem AbsolutelyContinuousSet.ae_of_forall_ae (hQS : Q.AbsolutelyContinuousSet S)
+    {p : Ω → Prop} (hp : MeasurableSet {ω | p ω}) (h : ∀ P ∈ S, ∀ᵐ ω ∂P, p ω) :
+    ∀ᵐ ω ∂Q, p ω :=
+  ae_iff.mpr (hQS hp.compl fun P hP ↦ ae_iff.mp (h P hP))
+
+/-- A measure absolutely continuous with respect to `S` is absolutely continuous with respect to
+every measure `ν` that dominates all members of `S`. -/
+theorem AbsolutelyContinuousSet.absolutelyContinuous (hQS : Q.AbsolutelyContinuousSet S)
+    (h : ∀ P ∈ S, P ≪ ν) : Q ≪ ν :=
+  .mk fun _ hs hνs ↦ hQS hs fun P hP ↦ h P hP hνs
+
+/-- Absolute continuity with respect to a set of measures is monotone in the set. -/
+theorem AbsolutelyContinuousSet.mono (hQS : Q.AbsolutelyContinuousSet S) (hST : S ⊆ T) :
+    Q.AbsolutelyContinuousSet T :=
+  fun _ hs h ↦ hQS hs fun P hP ↦ h P (hST hP)
+
+/-- A measure absolutely continuous with respect to a measure absolutely continuous with respect
+to `S` is absolutely continuous with respect to `S`. -/
+theorem AbsolutelyContinuous.trans_absolutelyContinuousSet (hQ'Q : Q' ≪ Q)
+    (hQS : Q.AbsolutelyContinuousSet S) : Q'.AbsolutelyContinuousSet S :=
+  fun _ hs h ↦ hQ'Q (hQS hs h)
+
+/-- Absolute continuity with respect to a singleton is absolute continuity. -/
+@[simp]
+theorem absolutelyContinuousSet_singleton_iff : Q.AbsolutelyContinuousSet {P} ↔ Q ≪ P :=
+  ⟨fun h ↦ .mk fun _ hs hPs ↦ h hs (by simpa using hPs), fun h _ _ hs ↦ h (hs P rfl)⟩
+
+/-- A measure absolutely continuous with respect to a member of `S` is absolutely continuous
+with respect to `S`. -/
+theorem AbsolutelyContinuous.absolutelyContinuousSet (hQP : Q ≪ P) (hP : P ∈ S) :
+    Q.AbsolutelyContinuousSet S :=
+  (absolutelyContinuousSet_singleton_iff.mpr hQP).mono (singleton_subset_iff.mpr hP)
+
+end MeasureTheory.Measure

From 2ef74625a5d32843a5a4acfb0f4b1cd14c9fa9fe Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 15 Nov 2026 12:39:37 +0100
Subject: [PATCH 3/6] docs: state the finite-measure hypotheses of the ripr
 identifications

Co-Authored-By: Claude Code <noreply@github.com>
---
 LMLExplore/EValues/Numeraire.lean | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/LMLExplore/EValues/Numeraire.lean b/LMLExplore/EValues/Numeraire.lean
index 060fd427..159b4aaa 100644
--- a/LMLExplore/EValues/Numeraire.lean
+++ b/LMLExplore/EValues/Numeraire.lean
@@ -49,9 +49,9 @@ topology is assumed, except in the dominated criterion, which names its referenc
 * `ProbabilityTheory.isNumeraire_iff_withDensity_inv_mem_effectiveSet`: **the verification
   theorem** [LRR25, Theorem 4.1]: a `Q`-almost surely finite e-variable `X` is the numeraire
   exactly when `Q.withDensity X⁻¹` is in the effective null.
-* `ProbabilityTheory.IsNumeraire.ripr_eq_withDensity`: for a null of finite measures, the reverse
-  information projection is then `Q.withDensity X⁻¹`, and, for `Q` absolutely continuous with
-  respect to the null, `Q` is absolutely continuous with respect to it
+* `ProbabilityTheory.IsNumeraire.ripr_eq_withDensity`: for a finite `Q` and a null of finite
+  measures, the reverse information projection is then `Q.withDensity X⁻¹`, and, for `Q`
+  absolutely continuous with respect to the null, `Q` is absolutely continuous with respect to it
   (`MeasureTheory.Measure.AbsolutelyContinuousSet.absolutelyContinuous_ripr`).
 * `ProbabilityTheory.isNumeraire_iff_exists_ae_eq_rnDeriv`: for `Q` absolutely continuous with
   respect to a null of finite measures, the numeraire is the only e-variable that is `Q`-almost
@@ -61,7 +61,7 @@ topology is assumed, except in the dominated criterion, which names its referenc
   `ProbabilityTheory.isNumeraire_rnDeriv_iff`, `ProbabilityTheory.ripr_eq_of_isEVar_rnDeriv`:
   for `R` in the effective null with `Q ≪ R`, a function `Q`-almost surely equal to the likelihood
   ratio `Q.rnDeriv R` is the numeraire as soon as it is an e-variable, and `R` is then the reverse
-  information projection when `R ≪ Q`.
+  information projection when `R ≪ Q` and the members of `S` are finite measures.
 * `ProbabilityTheory.isNumeraire_rnDeriv_singleton`: the likelihood ratio `Q.rnDeriv P` is the
   numeraire of the simple null `{P}` when `Q ≪ P` [RW, Theorem 3.20]. Its expected logarithm is
   Statlib's `maxUtility_singleton_eq_klDiv`.
@@ -161,8 +161,8 @@ theorem isNumeraire_iff_isEVar_of_withDensity_inv_le [IsProbabilityMeasure Q]
   ⟨IsNumeraire.isEVar, fun hX ↦ isNumeraire_of_withDensity_inv_mem_effectiveSet hX hX_top
     (mem_effectiveSet_of_le hR h)⟩
 
-/-- The reverse information projection of `Q` onto `S` is `Q.withDensity X⁻¹` for the numeraire
-`X` [LRR25, Theorem 4.1]. -/
+/-- For a finite measure `Q` and a null `S` of finite measures, the reverse information
+projection of `Q` onto `S` is `Q.withDensity X⁻¹` for the numeraire `X` [LRR25, Theorem 4.1]. -/
 theorem IsNumeraire.ripr_eq_withDensity [IsFiniteMeasure Q] (hS : ∀ P ∈ S, IsFiniteMeasure P)
     (hX : IsNumeraire X S Q) : ripr Q S = Q.withDensity X⁻¹ := by
   rw [ripr]
@@ -196,8 +196,9 @@ theorem isNumeraire_rnDeriv_iff [IsProbabilityMeasure Q] (hR : R ∈ effectiveSe
     (hQR : Q ≪ R) : IsNumeraire (Q.rnDeriv R) S Q ↔ IsEVar (Q.rnDeriv R) S :=
   isNumeraire_iff_isEVar_of_ae_eq_rnDeriv hR hQR .rfl
 
-/-- For `R` in the effective null equivalent to `Q`, if the likelihood ratio `Q.rnDeriv R` is an
-e-variable, then `R` is the reverse information projection of `Q` onto `S`. -/
+/-- For a null `S` of finite measures and `R` in the effective null equivalent to `Q`, if the
+likelihood ratio `Q.rnDeriv R` is an e-variable, then `R` is the reverse information projection
+of `Q` onto `S`. -/
 theorem ripr_eq_of_isEVar_rnDeriv [IsProbabilityMeasure Q] (hS : ∀ P ∈ S, IsFiniteMeasure P)
     (hR : R ∈ effectiveSet S) (hQR : Q ≪ R) (hRQ : R ≪ Q) (hX : IsEVar (Q.rnDeriv R) S) :
     ripr Q S = R := by

From cefa2eb3f6c6642dd050dca5fc3270afefc29ac7 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 15 Nov 2026 13:00:17 +0100
Subject: [PATCH 4/6] =?UTF-8?q?docs:=20state=20Q=20=E2=89=AA=20R=20in=20th?=
 =?UTF-8?q?e=20likelihood-ratio=20criterion=20and=20the=20measurability=20?=
 =?UTF-8?q?hypothesis=20of=20ae=5Fof=5Fforall=5Fae?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-Authored-By: Claude Code <noreply@github.com>
---
 LMLExplore/EValues/Numeraire.lean                        | 8 ++++----
 .../MeasureTheory/Measure/AbsolutelyContinuousSet.lean   | 9 +++++----
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/LMLExplore/EValues/Numeraire.lean b/LMLExplore/EValues/Numeraire.lean
index 159b4aaa..9f07905b 100644
--- a/LMLExplore/EValues/Numeraire.lean
+++ b/LMLExplore/EValues/Numeraire.lean
@@ -31,10 +31,10 @@ surely finite [LRR25, Theorem 2.6].
 
 The verification theorem turns the search for the numeraire into checking one integral inequality
 per e-variable, or per member of the null. For a likelihood ratio `Q.rnDeriv R` against a member
-`R` of the effective null, it suffices that the likelihood ratio is an e-variable; with densities
-`q`, `p` and `r` with respect to a reference measure, this is the dominated criterion
-`∫⁻ p / r ∂Q ≤ 1` for every `P ∈ S` [LRR25, Theorem 4.7]; and for a null described by a
-generating family of e-variables, it suffices to check the generating family [LRR25,
+`R` of the effective null with `Q ≪ R`, it suffices that the likelihood ratio is an e-variable;
+with densities `q`, `p` and `r` with respect to a reference measure, this is the dominated
+criterion `∫⁻ p / r ∂Q ≤ 1` for every `P ∈ S` [LRR25, Theorem 4.7]; and for a null described by
+a generating family of e-variables, it suffices to check the generating family [LRR25,
 Corollary 4.2]. The simple null `{P}` with `Q ≪ P`, whose numeraire is the likelihood ratio
 `Q.rnDeriv P` [RW, Theorem 3.20], is the first instance. No dominating measure, convexity or
 topology is assumed, except in the dominated criterion, which names its reference measure.
diff --git a/LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean b/LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean
index ca39d322..ac1e0cb0 100644
--- a/LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean
+++ b/LMLExplore/MeasureTheory/Measure/AbsolutelyContinuousSet.lean
@@ -22,8 +22,9 @@ e-variables for a null `S` are `Q`-almost surely finite [LRR25, Theorem 2.6].
 
 ## Main statements
 
-* `MeasureTheory.Measure.AbsolutelyContinuousSet.ae_of_forall_ae`: a property of the points of a
-  measurable set that holds almost surely under every member of `S` holds `Q`-almost surely.
+* `MeasureTheory.Measure.AbsolutelyContinuousSet.ae_of_forall_ae`: a property `p` with
+  `{ω | p ω}` measurable that holds almost surely under every member of `S` holds `Q`-almost
+  surely.
 * `MeasureTheory.Measure.AbsolutelyContinuousSet.absolutelyContinuous`: `Q` is absolutely
   continuous with respect to every measure that dominates all members of `S`.
 * `MeasureTheory.Measure.absolutelyContinuousSet_singleton_iff`: absolute continuity with respect
@@ -61,8 +62,8 @@ theorem AbsolutelyContinuousSet.measure_eq_zero (hQS : Q.AbsolutelyContinuousSet
     (hs : MeasurableSet s) (h : ∀ P ∈ S, P s = 0) : Q s = 0 :=
   hQS hs h
 
-/-- A property of the points of a measurable set that holds almost surely under every member
-of `S` holds almost surely under a measure absolutely continuous with respect to `S`. This is the
+/-- A property `p` with `{ω | p ω}` measurable that holds almost surely under every member of `S`
+holds almost surely under a measure absolutely continuous with respect to `S`. This is the
 counterpart of `MeasureTheory.Measure.AbsolutelyContinuous.ae_le`. -/
 theorem AbsolutelyContinuousSet.ae_of_forall_ae (hQS : Q.AbsolutelyContinuousSet S)
     {p : Ω → Prop} (hp : MeasurableSet {ω | p ω}) (h : ∀ P ∈ S, ∀ᵐ ω ∂P, p ω) :

From fd6ebee321dccc7ff32c01aa83435d3fe2ad2ad3 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 15 Nov 2026 13:21:44 +0100
Subject: [PATCH 5/6] refactor: move the null-set e-variable lemmas to
 EVariable

Move `isEVar_piecewise_top` from `EffectiveSet.lean`, and the LRR25
Theorem 2.6 lemmas `AbsolutelyContinuousSet.ae_ne_top` and
`absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top` from
`Numeraire.lean`, to `EVariable.lean`: none of them involves the
effective null or numeraires. `EffectiveSet.lean` now imports
`LMLExplore.EValues.EVariable`. Names and statements are unchanged.

Co-Authored-By: Claude Code <noreply@github.com>
---
 LMLExplore/EValues/EVariable.lean    | 38 ++++++++++++++++++++++++++++
 LMLExplore/EValues/EffectiveSet.lean |  9 +------
 LMLExplore/EValues/Numeraire.lean    | 22 ++--------------
 3 files changed, 41 insertions(+), 28 deletions(-)

diff --git a/LMLExplore/EValues/EVariable.lean b/LMLExplore/EValues/EVariable.lean
index 30450c1a..3f01ff87 100644
--- a/LMLExplore/EValues/EVariable.lean
+++ b/LMLExplore/EValues/EVariable.lean
@@ -6,6 +6,7 @@ Authors: LMLExplore contributors
 module
 
 public import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
+public import LMLExplore.MeasureTheory.Measure.AbsolutelyContinuousSet
 public import LMLExplore.Probability.Independence.Integration
 public import Statlib.EValues.EVariable
 
@@ -21,6 +22,9 @@ under every probability measure of `S`. This file develops the first properties
 that hypothesis testing uses:
 
 * the exact e-variables, with `∫⁻ E ∂P = P univ` for every `P ∈ S`;
+* the e-variable equal to `∞` on a set null for every member of `S`, and the measures under which
+  every e-variable for `S` is almost surely finite, which are those absolutely continuous with
+  respect to `S`;
 * Markov's inequality, which makes `{α⁻¹ ≤ E}` the rejection region of a level-`α` test, and its
   smoothed form `min (α * E) 1`;
 * products of e-variables from a family that is independent under every member of the null.
@@ -41,6 +45,11 @@ e-variables are `ℝ≥0∞`-valued.
   of probability measures, the e-variables and the exact e-variables in terms of `∫⁻`.
 * `ProbabilityTheory.isExactEVar_rnDeriv`: for a finite measure `P`, a likelihood ratio
   `Q.rnDeriv P` with `Q ≪ P` and `Q univ = P univ` is an exact e-variable for `{P}`.
+* `ProbabilityTheory.isEVar_piecewise_top`: the function equal to `∞` on a measurable set null
+  for every member of `S`, and to `1` elsewhere, is an e-variable for `S`.
+* `ProbabilityTheory.absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top`: a measure `Q` is
+  absolutely continuous with respect to `S` (`MeasureTheory.Measure.AbsolutelyContinuousSet`)
+  exactly when every e-variable for `S` is `Q`-almost surely finite [LRR25, Theorem 2.6].
 * `ProbabilityTheory.IsEVar.measure_inv_le_le`: **Markov's inequality** for e-variables,
   `P {ω | α⁻¹ ≤ E ω} ≤ α`.
 * `ProbabilityTheory.IsEVar.lintegral_min_mul_le`: `∫⁻ ω, min (α * E ω) 1 ∂P ≤ α`.
@@ -51,6 +60,8 @@ e-variables are `ℝ≥0∞`-valued.
 
 ## References
 
+* [LRR25] M. Larsson, A. Ramdas and J. Ruf, *The numeraire e-variable and reverse information
+  projection*, Ann. Statist. 53 (2025), arXiv:2402.18810v4, Theorem 2.6.
 * A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in
   Statistics 1 (2025), arXiv:2410.23614v6: Definition 1.2, Fact 1.3 and Proposition 2.1.
 * V. Vovk and R. Wang, *E-values: calibration, combination and applications*, Ann. Statist. 49
@@ -143,6 +154,33 @@ theorem isExactEVar_rnDeriv {Q : Measure Ω} [IsFiniteMeasure P] [Q.HaveLebesgue
     (by simp [Measure.lintegral_rnDeriv hQP, hQ])
   lintegral_eq_measure_univ := by simp [Measure.lintegral_rnDeriv hQP, hQ]
 
+/-! ### E-variables and null sets -/
+
+/-- For a measurable set `s` that is null for every member of `S`, the function equal to `∞` on
+`s` and to `1` elsewhere is an e-variable for `S`. -/
+theorem isEVar_piecewise_top {s : Set Ω} [DecidablePred (· ∈ s)] (hs : MeasurableSet s)
+    (hS : ∀ P ∈ S, P s = 0) : IsEVar (s.piecewise (fun _ ↦ ∞) 1) S :=
+  (isEVar_one S).congr (measurable_const.piecewise hs measurable_const) fun P hP ↦ by
+    filter_upwards [measure_eq_zero_iff_ae_notMem.mp (hS P hP)] with ω hω
+    simp [hω]
+
+/-- An e-variable for `S` is almost surely finite under a measure absolutely continuous with
+respect to `S` [LRR25, Theorem 2.6]. -/
+theorem _root_.MeasureTheory.Measure.AbsolutelyContinuousSet.ae_ne_top {Q : Measure Ω}
+    (hQS : Q.AbsolutelyContinuousSet S) (hE : IsEVar E S) : ∀ᵐ ω ∂Q, E ω ≠ ∞ :=
+  hQS.ae_of_forall_ae ((measurableSet_singleton ∞).compl.preimage hE.measurable)
+    fun _ hP ↦ hE.ae_ne_top hP
+
+/-- A measure is absolutely continuous with respect to `S` exactly when every e-variable for `S`
+is almost surely finite under it [LRR25, Theorem 2.6]. -/
+theorem absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top {Q : Measure Ω} :
+    Q.AbsolutelyContinuousSet S ↔ ∀ E, IsEVar E S → ∀ᵐ ω ∂Q, E ω ≠ ∞ := by
+  classical
+  refine ⟨fun hQS _ hE ↦ hQS.ae_ne_top hE,
+    fun h ↦ Measure.absolutelyContinuousSet_iff.mpr fun s hs hS ↦ ?_⟩
+  refine measure_mono_null (fun ω hω ↦ ?_) (ae_iff.mp (h _ (isEVar_piecewise_top hs hS)))
+  simp [hω]
+
 /-! ### Markov's inequality -/
 
 /-- **Markov's inequality** for e-variables: for every probability measure `P` of the null and
diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean
index bddce8b3..cc55fcc8 100644
--- a/LMLExplore/EValues/EffectiveSet.lean
+++ b/LMLExplore/EValues/EffectiveSet.lean
@@ -6,6 +6,7 @@ Authors: LMLExplore contributors
 module
 
 public import Statlib.EValues.RIPr
+public import LMLExplore.EValues.EVariable
 public import LMLExplore.MeasureTheory.Integral.Lebesgue.Add
 public import LMLExplore.MeasureTheory.Measure.AbsolutelyContinuousSet
 
@@ -141,14 +142,6 @@ theorem mem_effectiveSet_of_tendsto {ι : Type*} {l : Filter ι} [l.NeBot] {μs
     μ ∈ effectiveSet S :=
   mem_effectiveSet_of_measure_le_liminf hμs fun s hs ↦ (h s hs).liminf_eq.ge
 
-/-- For a measurable set `s` that is null for every member of `S`, the function equal to `∞` on
-`s` and to `1` elsewhere is an e-variable for `S`. -/
-theorem isEVar_piecewise_top {s : Set Ω} [DecidablePred (· ∈ s)] (hs : MeasurableSet s)
-    (hS : ∀ P ∈ S, P s = 0) : IsEVar (s.piecewise (fun _ ↦ ∞) 1) S :=
-  (isEVar_one S).congr (measurable_const.piecewise hs measurable_const) fun P hP ↦ by
-    filter_upwards [measure_eq_zero_iff_ae_notMem.mp (hS P hP)] with ω hω
-    simp [hω]
-
 /-- A measurable set that is null for every member of `S` is null for every member of the
 effective null of `S`. -/
 theorem measure_eq_zero_of_mem_effectiveSet (hμ : μ ∈ effectiveSet S) {s : Set Ω}
diff --git a/LMLExplore/EValues/Numeraire.lean b/LMLExplore/EValues/Numeraire.lean
index 9f07905b..cad388bb 100644
--- a/LMLExplore/EValues/Numeraire.lean
+++ b/LMLExplore/EValues/Numeraire.lean
@@ -27,7 +27,8 @@ The finiteness of `X` is automatic when `Q` is absolutely continuous with respec
 `Q.AbsolutelyContinuousSet S`, defined in
 `LMLExplore.MeasureTheory.Measure.AbsolutelyContinuousSet`: every measurable set that is null for
 every member of `S` is `Q`-null. This holds exactly when every e-variable for `S` is `Q`-almost
-surely finite [LRR25, Theorem 2.6].
+surely finite (`ProbabilityTheory.absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top`, in
+`LMLExplore.EValues.EVariable`) [LRR25, Theorem 2.6].
 
 The verification theorem turns the search for the numeraire into checking one integral inequality
 per e-variable, or per member of the null. For a likelihood ratio `Q.rnDeriv R` against a member
@@ -41,9 +42,6 @@ topology is assumed, except in the dominated criterion, which names its referenc
 
 ## Main statements
 
-* `ProbabilityTheory.absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top`: `Q` is absolutely
-  continuous with respect to `S` exactly when every e-variable for `S` is `Q`-almost surely finite
-  [LRR25, Theorem 2.6].
 * `ProbabilityTheory.withDensity_inv_mem_effectiveSet_iff`: `Q.withDensity X⁻¹` is in the
   effective null exactly when `∫⁻ Y / X ∂Q ≤ 1` for every e-variable `Y`.
 * `ProbabilityTheory.isNumeraire_iff_withDensity_inv_mem_effectiveSet`: **the verification
@@ -92,22 +90,6 @@ namespace ProbabilityTheory
 
 open Measure
 
-/-- An e-variable for `S` is almost surely finite under a measure absolutely continuous with
-respect to `S` [LRR25, Theorem 2.6]. -/
-theorem _root_.MeasureTheory.Measure.AbsolutelyContinuousSet.ae_ne_top
-    (hQS : Q.AbsolutelyContinuousSet S) (hX : IsEVar X S) : ∀ᵐ ω ∂Q, X ω ≠ ∞ :=
-  hQS.ae_of_forall_ae ((measurableSet_singleton ∞).compl.preimage hX.measurable)
-    fun _ hP ↦ hX.ae_ne_top hP
-
-/-- A measure is absolutely continuous with respect to `S` exactly when every e-variable for `S`
-is almost surely finite under it [LRR25, Theorem 2.6]. -/
-theorem absolutelyContinuousSet_iff_forall_isEVar_ae_ne_top :
-    Q.AbsolutelyContinuousSet S ↔ ∀ X, IsEVar X S → ∀ᵐ ω ∂Q, X ω ≠ ∞ := by
-  classical
-  refine ⟨fun hQS _ hX ↦ hQS.ae_ne_top hX, fun h ↦ absolutelyContinuousSet_iff.mpr fun s hs hS ↦ ?_⟩
-  refine measure_mono_null (fun ω hω ↦ ?_) (ae_iff.mp (h _ (isEVar_piecewise_top hs hS)))
-  simp [hω]
-
 /-! ### The verification theorem -/
 
 /-- The measure `Q.withDensity X⁻¹` is in the effective null exactly when every e-variable `Y`

From 39f9a4efdcc5a15447dee1f2e697b891681060b3 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Sun, 15 Nov 2026 14:24:53 +0100
Subject: [PATCH 6/6] refactor: state measure_fsupport_eq_measure_univ for an
 almost surely finite function
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Replace `IsEVar.measure_fsupport_eq_measure_univ`, which assumed `Q ≪ S`, with
`measure_fsupport_eq_measure_univ`, which assumes only that the function is
`Q`-almost surely positive and finite, and reuse it in
`isNumeraire_of_withDensity_inv_mem_effectiveSet`. State the hypotheses of the
dominated criterion in the module docstring.

Co-Authored-By: Claude Code <noreply@github.com>
---
 LMLExplore/EValues/Numeraire.lean | 32 +++++++++++++++----------------
 1 file changed, 15 insertions(+), 17 deletions(-)

diff --git a/LMLExplore/EValues/Numeraire.lean b/LMLExplore/EValues/Numeraire.lean
index d53526de..3d4ee92b 100644
--- a/LMLExplore/EValues/Numeraire.lean
+++ b/LMLExplore/EValues/Numeraire.lean
@@ -53,8 +53,10 @@ finite.
   e-variable is the reverse information projection; for a simple null `{P}` with `P` equivalent
   to `Q`, the reverse information projection is `P`.
 * `ProbabilityTheory.isNumeraire_div_rnDeriv_iff`: **the dominated criterion** [LRR25,
-  Theorem 4.7]: with densities `q`, `p` and `r` with respect to a σ-finite reference measure,
-  `q / r` is the numeraire exactly when `∫⁻ p / r ∂Q ≤ 1` for every `P ∈ S`.
+  Theorem 4.7]: for a null `S` of probability measures, with densities `q` of `Q` and `p` of
+  `P ∈ S` with respect to a σ-finite reference measure, and with `r` the density of a member `R`
+  of the effective null with `Q ≪ R`, `q / r` is the numeraire exactly when `∫⁻ p / r ∂Q ≤ 1` for
+  every `P ∈ S`.
 * `ProbabilityTheory.isNumeraire_of_lintegral_div_le_one`,
   `ProbabilityTheory.ripr_mem_of_lintegral_div_le_one`: for a null `S` containing every
   probability measure under which each member of a family `𝓔₀` has expectation at most `1`, a
@@ -136,6 +138,13 @@ theorem isNumeraire_of_smul_withDensity_inv_le [IsFiniteMeasure Q] (hX : IsEVar
 
 /-! ### Almost surely finite e-variables -/
 
+/-- The finite support of a `Q`-almost surely positive and finite function has full measure under
+`Q`. -/
+theorem measure_fsupport_eq_measure_univ (hX_top : ∀ᵐ ω ∂Q, X ω ≠ ∞)
+    (hX₀ : ∀ᵐ ω ∂Q, X ω ≠ 0) : Q X.fsupport = Q univ :=
+  measure_congr <| ae_eq_univ.mpr <| mem_ae_iff.mp <| by
+    filter_upwards [hX_top, hX₀] with ω h_top h_zero using ⟨h_top, h_zero⟩
+
 /-- The measure `Q.withDensity X⁻¹` is in the effective null exactly when every e-variable `Y`
 has `∫⁻ Y / X ∂Q ≤ 1`: under `Q.withDensity X⁻¹`, `Y` has expectation `∫⁻ Y / X ∂Q`. -/
 theorem withDensity_inv_mem_effectiveSet_iff (hX : Measurable X) :
@@ -157,11 +166,8 @@ theorem isNumeraire_of_withDensity_inv_mem_effectiveSet [IsProbabilityMeasure Q]
       ne_top_of_le_ne_top ENNReal.one_ne_top (by simpa using h_div 1 (isEVar_one S))
     filter_upwards [ae_lt_top hX.measurable.inv h_inv] with ω hω
     simpa using hω.ne
-  have h_supp : Q X.fsupport = 1 := by
-    rw [← measure_univ (μ := Q)]
-    refine (ae_iff_measure_eq hX.measurable_fsupport.nullMeasurableSet).mp ?_
-    filter_upwards [hX_top, hX_zero] with ω h_top h_zero
-    exact ⟨h_top, h_zero⟩
+  have h_supp : Q X.fsupport = 1 :=
+    (measure_fsupport_eq_measure_univ hX_top hX_zero).trans measure_univ
   exact isNumeraire_of_lintegral_div_le hX (by simp [h_supp]) fun Y hY ↦ h_supp ▸ h_div Y hY
 
 /-- **[LRR25, Theorem 4.1].** A `Q`-almost surely finite e-variable `X` for `S` is the numeraire
@@ -177,15 +183,6 @@ theorem isNumeraire_iff_withDensity_inv_mem_effectiveSet [IsProbabilityMeasure Q
 
 /-! ### Alternatives absolutely continuous with respect to the null -/
 
-/-- If `Q` is absolutely continuous with respect to `S`, the finite support of a `Q`-almost surely
-positive e-variable for `S` has full measure under `Q`. -/
-theorem IsEVar.measure_fsupport_eq_measure_univ [IsFiniteMeasure Q] (hX : IsEVar X S)
-    (hQS : Q.AbsolutelyContinuousSet S) (hX₀ : ∀ᵐ ω ∂Q, X ω ≠ 0) :
-    Q X.fsupport = Q univ := by
-  refine (ae_iff_measure_eq hX.measurable_fsupport.nullMeasurableSet).mp ?_
-  filter_upwards [hQS.ae_ne_top hX, hX₀] with ω h_top h_zero
-  exact ⟨h_top, h_zero⟩
-
 /-- The reverse information projection is the measure of density `X⁻¹` with respect to `Q`, for
 the numeraire `X` [LRR25, Theorem 4.1]. -/
 theorem IsNumeraire.ripr_eq [IsFiniteMeasure Q] (hS : ∀ P ∈ S, IsFiniteMeasure P)
@@ -216,7 +213,8 @@ theorem IsNumeraire.eq_withDensity_inv_of_le [IsProbabilityMeasure Q]
   have h_one : ∫⁻ ω, X ω ∂ν = 1 := by
     rw [lintegral_withDensity_inv_eq_lintegral_div hX_meas.aemeasurable hX_meas.aemeasurable,
       lintegral_div_self_eq_measure_fsupport hX_meas.aemeasurable,
-      hX.isEVar.measure_fsupport_eq_measure_univ hQS hX.ae_ne_zero, measure_univ]
+      measure_fsupport_eq_measure_univ (hQS.ae_ne_top hX.isEVar) hX.ae_ne_zero,
+      measure_univ]
   have h_add : ∫⁻ ω, X ω ∂(μ - ν) + 1 ≤ 1 := by
     have h_le := hμ X hX.isEVar
     rwa [← Measure.sub_add_cancel_of_le hle, lintegral_add_measure, h_one] at h_le