feat: the randomized Markov inequality and randomized e-to-p calibration

LMLExplore/EValues/PVariable.lean

@@ -38,7 +38,8 @@ uniform law on `[0, 1]`.
   `ProbabilityTheory.volume_restrict_Icc_ofReal_lt`: the distribution function of the uniform law
   on `[0, 1]`.
 * `ProbabilityTheory.IsExactPVar.ae_le_one`: an exact p-variable is almost surely at most `1`
-  under every probability measure of the null.
+  under every probability measure of the null, and
+  `ProbabilityTheory.IsExactPVar.measure_le_eq_min`: its distribution function is `α ↦ min α 1`.
 * `ProbabilityTheory.IsPVar.lintegral_comp_le`: under a measure of mass at most `1`, the integral
   of an antitone function of a p-variable is at most its integral against the uniform law on
   `[0, 1]`: a p-variable is stochastically larger than the uniform law.
@@ -154,6 +155,18 @@ theorem IsExactPVar.ae_le_one (hp : IsExactPVar p S) (hP : P ∈ S) [IsProbabili
   rw [ae_iff_measure_eq (measurableSet_le hp.measurable measurable_const).nullMeasurableSet,
     hp.measure_le_eq P hP 1 le_rfl, measure_univ]
 
+/-- The distribution function of an exact p-variable under a probability measure of the null is
+that of the uniform law on `[0, 1]`: it gives mass `min α 1` to `{ω | p ω ≤ α}`. -/
+theorem IsExactPVar.measure_le_eq_min (hp : IsExactPVar p S) (hP : P ∈ S)
+    [IsProbabilityMeasure P] (α : ℝ≥0∞) :
+    P {ω | p ω ≤ α} = min α 1 := by
+  rcases le_total α 1 with hα | hα
+  · rw [hp.measure_le_eq P hP α hα, min_eq_left hα]
+  · rw [min_eq_right hα]
+    refine le_antisymm prob_le_one ?_
+    rw [← hp.measure_le_eq P hP 1 le_rfl]
+    exact measure_mono fun ω (hω : p ω ≤ 1) ↦ hω.trans hα
+
 /-! ### The uniform law on `[0, 1]` -/
 
 /-- The distribution function of the uniform law on `[0, 1]`: it gives mass `min α 1` to
@@ -190,6 +203,13 @@ theorem volume_restrict_Icc_ofReal_lt (a : ℝ≥0∞) :
       inter_eq_right.2 fun x hx ↦ (ENNReal.ofReal_le_one.2 hx.2).trans_lt ha
     simp [h_set, min_eq_right ha.le]
 
+/-- A measure under which a real random variable has the uniform law on `[0, 1]` is a probability
+measure. -/
+theorem isProbabilityMeasure_of_map_eq_volume_restrict_Icc {U : Ω → ℝ} (hU : AEMeasurable U P)
+    (hU_law : P.map U = volume.restrict (Icc 0 1)) : IsProbabilityMeasure P := by
+  have : IsProbabilityMeasure (P.map U) := ⟨by simp [hU_law]⟩
+  exact Measure.isProbabilityMeasure_of_map hU
+
 /-- The identity of `[0, 1]`, under the Lebesgue measure on `[0, 1]`, is an exact p-variable. -/
 theorem isExactPVar_ofReal_volume :
     IsExactPVar (fun x : ℝ ↦ ENNReal.ofReal x) {volume.restrict (Icc 0 1)} := by

LMLExplore/EValues/RandomizedMarkov.lean

@@ -0,0 +1,165 @@
+/-
+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.PVariable
+public import LMLExplore.Probability.Independence.Basic
+
+/-!
+# The randomized Markov inequality
+
+Markov's inequality for e-variables rejects the null at level `α` when `α⁻¹ ≤ E`
+(`ProbabilityTheory.IsEVar.measure_inv_le_le`). Randomizing the threshold makes the test
+uniformly more powerful at no cost in validity: with `U` uniform on `[0, 1]` and independent of
+`E`, rejecting when `U ≤ α * E` still has level `α`: the threshold `1` of the test `1 ≤ α * E`
+is lowered to the random threshold `U`. The exact statement is the identity
+`P {U ≤ α * Y} = ∫⁻ min (α * Y) 1 ∂P ≤ α * ∫⁻ Y ∂P` for any `ℝ≥0∞`-valued `Y` independent of `U`,
+the uniformly randomized Markov inequality [RM26, Theorem 1.2; RW, Theorem 2.9].
+
+The proof freezes `Y` (`ProbabilityTheory.IndepFun.measure_prodMk_mem_eq_lintegral`): the event
+`{U ≤ Z}`, for `Z` independent of `U`, has probability `∫⁻ ω, P {U ≤ Z ω} ∂P`, and the
+distribution function of `U` is `t ↦ min t 1`. The same argument with a p-variable `p` in place
+of `U` gives the inequality `P {p ≤ Z} ≤ ∫⁻ min Z 1 ∂P`, since a p-variable has
+`P {p ≤ t} ≤ min t 1`; for an exact p-variable it is an equality. In particular, for a
+p-variable `p` and an e-variable `E` independent under every member of the null, `p / E` is a
+p-variable, and so is `U / E` for `U` uniform on `[0, 1]` [RW, Corollary 2.10]: the e-to-p
+calibration `E ↦ E⁻¹` (`ProbabilityTheory.IsEVar.isPVar_inv`) can be sharpened by an independent
+p-variable.
+
+As everywhere in `LMLExplore.EValues`, the null is an arbitrary set of measures, and values are
+in `ℝ≥0∞`, with `p / 0 = ∞` for `p ≠ 0` and `p / ∞ = 0`.
+
+## Main statements
+
+* `ProbabilityTheory.IsPVar.measure_le_le_lintegral_min`,
+  `ProbabilityTheory.IsExactPVar.measure_le_eq_lintegral_min`: for `Z` independent of a
+  p-variable `p`, `P {p ≤ Z} ≤ ∫⁻ min Z 1 ∂P`, with equality when `p` is exact.
+* `ProbabilityTheory.measure_ofReal_le_mul_eq_lintegral_min`: for `U` uniform on `[0, 1]` and
+  independent of `Y`, `P {U ≤ α * Y} = ∫⁻ min (α * Y) 1 ∂P` [RW, Theorem 2.9].
+* `ProbabilityTheory.IsPVar.measure_le_mul_le_mul_lintegral`: **the randomized Markov
+  inequality**, `P {p ≤ α * Y} ≤ α * ∫⁻ Y ∂P` for `Y` independent of a p-variable `p`, in
+  particular of a uniform variable [RM26, Theorem 1.2].
+* `ProbabilityTheory.IsEVar.measure_le_mul_le`: the randomized e-test `{p ≤ α * E}` has level `α`.
+* `ProbabilityTheory.IsEVar.isPVar_div`, `ProbabilityTheory.IsEVar.isPVar_ofReal_div`: `p / E`
+  and `U / E` are p-variables [RW, Corollary 2.10].
+
+## References
+
+* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in
+  Statistics 1 (2025), arXiv:2410.23614v6: Theorem 2.9 and Corollary 2.10.
+* [RM26] A. Ramdas and T. Manole, *Randomized and exchangeable improvements of Markov's,
+  Chebyshev's and Chernoff's inequalities*, Statist. Sci. 41 (2026),
+  arXiv:2304.02611v3: Theorem 1.2.
+-/
+
+public section
+
+open MeasureTheory Set
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S : Set (Measure Ω)} {P : Measure Ω}
+  {p E Y Z : Ω → ℝ≥0∞}
+
+/-- The event `{p ≤ Z}` of independent `ℝ≥0∞`-valued variables, by freezing `Z`. -/
+private theorem measure_le_eq_lintegral_of_indepFun [IsFiniteMeasure P] (hp : Measurable p)
+    (hZ : Measurable Z) (hpZ : IndepFun p Z P) :
+    P {ω | p ω ≤ Z ω} = ∫⁻ ω, P {ω' | p ω' ≤ Z ω} ∂P :=
+  hpZ.measure_prodMk_mem_eq_lintegral hp.aemeasurable hZ.aemeasurable (s := {x | x.1 ≤ x.2})
+    (measurableSet_le measurable_fst measurable_snd)
+
+/-- A p-variable `p` is at most an independent threshold `Z` with probability at most
+`∫⁻ min Z 1 ∂P`: the randomized test that rejects when `p ≤ Z` has the size of the
+`[0, 1]`-valued test `min Z 1`. -/
+theorem IsPVar.measure_le_le_lintegral_min (hp : IsPVar p S) (hP : P ∈ S)
+    [IsProbabilityMeasure P] (hZ : Measurable Z) (hpZ : IndepFun p Z P) :
+    P {ω | p ω ≤ Z ω} ≤ ∫⁻ ω, min (Z ω) 1 ∂P := by
+  rw [measure_le_eq_lintegral_of_indepFun hp.measurable hZ hpZ]
+  exact lintegral_mono fun ω ↦ le_min (hp.measure_le_le P hP _) prob_le_one
+
+/-- An exact p-variable `p` is below an independent threshold `Z` with probability exactly
+`∫⁻ min Z 1 ∂P`. -/
+theorem IsExactPVar.measure_le_eq_lintegral_min (hp : IsExactPVar p S) (hP : P ∈ S)
+    [IsProbabilityMeasure P] (hZ : Measurable Z) (hpZ : IndepFun p Z P) :
+    P {ω | p ω ≤ Z ω} = ∫⁻ ω, min (Z ω) 1 ∂P := by
+  simp_rw [measure_le_eq_lintegral_of_indepFun hp.measurable hZ hpZ, hp.measure_le_eq_min hP]
+
+/-- **The randomized Markov identity** [RW, Theorem 2.9]: for `U` uniform on `[0, 1]` and
+independent of a measurable `Y : Ω → ℝ≥0∞`, the randomized test that rejects when `U ≤ α * Y` has
+rejection probability `∫⁻ min (α * Y) 1 ∂P`, the expectation of the `[0, 1]`-valued test
+`min (α * Y) 1`. -/
+theorem measure_ofReal_le_mul_eq_lintegral_min (hY : Measurable Y) {U : Ω → ℝ} (hU : Measurable U)
+    (hU_law : P.map U = volume.restrict (Icc 0 1)) (hUY : IndepFun U Y P) (α : ℝ≥0∞) :
+    P {ω | ENNReal.ofReal (U ω) ≤ α * Y ω} = ∫⁻ ω, min (α * Y ω) 1 ∂P := by
+  have := isProbabilityMeasure_of_map_eq_volume_restrict_Icc hU.aemeasurable hU_law
+  refine (isExactPVar_ofReal_of_map_eq (S := {P}) hU fun Q hQ ↦ ?_).measure_le_eq_lintegral_min
+    (mem_singleton P) (hY.const_mul α)
+    (hUY.comp ENNReal.measurable_ofReal (measurable_const_mul α))
+  rwa [mem_singleton_iff.1 hQ]
+
+/-- **The randomized Markov inequality** [RW, Theorem 2.9; RM26, Theorem 1.2]: for a p-variable
+`p` and an independent measurable `Y : Ω → ℝ≥0∞`, `P {p ≤ α * Y} ≤ α * ∫⁻ Y ∂P`. For `p` uniform
+on `[0, 1]` (`ProbabilityTheory.isExactPVar_ofReal_of_map_eq`), this is the uniformly randomized
+Markov inequality `P {U ≤ α * Y} ≤ α * ∫⁻ Y ∂P`, whose event contains that of Markov's inequality
+`P {1 ≤ α * Y} ≤ α * ∫⁻ Y ∂P` as soon as `U ≤ 1`. -/
+theorem IsPVar.measure_le_mul_le_mul_lintegral (hp : IsPVar p S) (hP : P ∈ S)
+    [IsProbabilityMeasure P] (hY : Measurable Y) (hpY : IndepFun p Y P) (α : ℝ≥0∞) :
+    P {ω | p ω ≤ α * Y ω} ≤ α * ∫⁻ ω, Y ω ∂P :=
+  calc P {ω | p ω ≤ α * Y ω}
+  _ ≤ ∫⁻ ω, min (α * Y ω) 1 ∂P :=
+    hp.measure_le_le_lintegral_min hP (hY.const_mul α)
+      (hpY.comp measurable_id (measurable_const_mul α))
+  _ ≤ ∫⁻ ω, α * Y ω ∂P := lintegral_mono fun _ ↦ min_le_left _ _
+  _ = α * ∫⁻ ω, Y ω ∂P := lintegral_const_mul α hY
+
+/-- **The randomized e-test** [RW, Theorem 2.9]: for an e-variable `E` and a p-variable `p`
+independent of `E` under a probability measure `P` of the null, rejecting when `p ≤ α * E` has
+level `α`. For `p` uniform on `[0, 1]`, this lowers the rejection threshold of the test
+`1 ≤ α * E` of Markov's inequality (`ProbabilityTheory.IsEVar.measure_inv_le_le`) to `U`. -/
+theorem IsEVar.measure_le_mul_le (hE : IsEVar E S) (hp : IsPVar p S) (hP : P ∈ S)
+    [IsProbabilityMeasure P] (hpE : IndepFun p E P) (α : ℝ≥0∞) :
+    P {ω | p ω ≤ α * E ω} ≤ α :=
+  (hp.measure_le_le_lintegral_min hP (hE.measurable.const_mul α)
+    (hpE.comp measurable_id (measurable_const_mul α))).trans (hE.lintegral_min_mul_le hP α)
+
+/-- **Randomized e-to-p calibration** [RW, Corollary 2.10]: for a null of probability measures,
+an e-variable `E` and a p-variable `p` that are independent under every member of the null,
+`p / E` is a p-variable. -/
+theorem IsEVar.isPVar_div (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hE : IsEVar E S)
+    (hp : IsPVar p S) (hpE : ∀ P ∈ S, IndepFun p E P) :
+    IsPVar (fun ω ↦ p ω / E ω) S where
+  measurable := hp.measurable.div hE.measurable
+  measure_le_le P hP α := by
+    have := hS P hP
+    rcases eq_or_ne α ∞ with rfl | hα
+    · exact le_top
+    -- off the `P`-null set where `E` is infinite, `p / E ≤ α` means `p ≤ α * E`
+    have h_top : P {ω | E ω = ∞} = 0 := by
+      simpa [lt_top_iff_ne_top] using ae_iff.1 (hE.ae_lt_top hP)
+    calc P {ω | p ω / E ω ≤ α}
+    _ ≤ P ({ω | p ω ≤ α * E ω} ∪ {ω | E ω = ∞}) := by
+      refine measure_mono fun ω (hω : p ω / E ω ≤ α) ↦ ?_
+      rcases eq_or_ne (E ω) ∞ with hω_top | hω_top
+      · exact Or.inr hω_top
+      exact Or.inl ((ENNReal.div_le_iff_le_mul (.inr hα) (.inl hω_top)).1 hω)
+    _ ≤ P {ω | p ω ≤ α * E ω} + P {ω | E ω = ∞} := measure_union_le _ _
+    _ ≤ α := by
+      rw [h_top, add_zero]
+      exact hE.measure_le_mul_le hp hP (hpE P hP) α
+
+/-- **Randomized e-to-p calibration with a uniform variable** [RW, Corollary 2.10]: for an
+e-variable `E` and a variable `U` uniform on `[0, 1]` and independent of `E` under every member of
+the null, `U / E` is a p-variable. -/
+theorem IsEVar.isPVar_ofReal_div (hE : IsEVar E S) {U : Ω → ℝ} (hU : Measurable U)
+    (hU_law : ∀ P ∈ S, P.map U = volume.restrict (Icc 0 1)) (hUE : ∀ P ∈ S, IndepFun U E P) :
+    IsPVar (fun ω ↦ ENNReal.ofReal (U ω) / E ω) S :=
+  hE.isPVar_div (fun P hP ↦ isProbabilityMeasure_of_map_eq_volume_restrict_Icc hU.aemeasurable
+      (hU_law P hP))
+    (isExactPVar_ofReal_of_map_eq hU hU_law).toIsPVar
+    fun P hP ↦ (hUE P hP).comp ENNReal.measurable_ofReal measurable_id
+
+end ProbabilityTheory

LMLExplore/Probability/Independence/Basic.lean

@@ -0,0 +1,51 @@
+/-
+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.Probability.Independence.Basic
+
+/-!
+# Events of a pair of independent random variables
+
+For random variables `X` and `Y` that are independent under a finite measure `μ`, the joint law of
+`(X, Y)` is the product of the laws (`ProbabilityTheory.IndepFun.map_prod_eq_prod_map_map`). By
+Tonelli's theorem, the probability of an event `{(X, Y) ∈ s}` is then obtained by freezing the
+value of `Y` and integrating the probability of the resulting event of `X` against the law of
+`Y`. This computes the probability of the events of a randomized test, which compare a test
+statistic with an independent source of randomness.
+
+## Main statements
+
+* `ProbabilityTheory.IndepFun.measure_prodMk_mem_eq_lintegral`: for independent `X` and `Y`,
+  `μ {ω | (X ω, Y ω) ∈ s} = ∫⁻ ω, μ {ω' | (X ω', Y ω) ∈ s} ∂μ`.
+-/
+
+public section
+
+open MeasureTheory
+
+namespace ProbabilityTheory
+
+variable {Ω α β : Type*} {mΩ : MeasurableSpace Ω} {mα : MeasurableSpace α}
+  {mβ : MeasurableSpace β} {μ : Measure Ω} {X : Ω → α} {Y : Ω → β}
+
+/-- **Freezing an independent variable**: for random variables `X` and `Y` that are independent
+under a finite measure `μ`, the probability of an event `{(X, Y) ∈ s}` is the integral over the
+values of `Y` of the probability of the event of `X` obtained by fixing `Y`. -/
+theorem IndepFun.measure_prodMk_mem_eq_lintegral [IsFiniteMeasure μ] (hXY : IndepFun X Y μ)
+    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) {s : Set (α × β)} (hs : MeasurableSet s) :
+    μ {ω | (X ω, Y ω) ∈ s} = ∫⁻ ω, μ {ω' | (X ω', Y ω) ∈ s} ∂μ := by
+  have h_map : μ {ω | (X ω, Y ω) ∈ s} = (μ.map X).prod (μ.map Y) s := by
+    rw [← hXY.map_prod_eq_prod_map_map hX hY,
+      Measure.map_apply₀ (hX.prodMk hY) hs.nullMeasurableSet]
+    rfl
+  rw [h_map, Measure.prod_apply_symm hs,
+    lintegral_map' (measurable_measure_prodMk_right hs).aemeasurable hY]
+  refine lintegral_congr fun ω ↦ ?_
+  rw [Measure.map_apply₀ hX (measurable_prodMk_right hs).nullMeasurableSet]
+  rfl
+
+end ProbabilityTheory