feat: identifying numeraires through the effective null

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

LMLExplore/EValues/EffectiveSet.lean

@@ -6,7 +6,9 @@ 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
 
 /-!
 # The effective null
@@ -40,6 +42,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
@@ -142,24 +147,23 @@ 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`. -/