feat: p-variables, exact e- and p-variables, and Markov's inequality for e-variables

LMLExplore/EValues/EVariable.lean

@@ -0,0 +1,220 @@
+/-
+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.Decomposition.RadonNikodym
+public import LMLExplore.Probability.Independence.Integration
+public import Statlib.EValues.EVariable
+
+/-!
+# Exact e-variables, Markov's inequality and products of independent e-variables
+
+An e-variable for a null hypothesis `S : Set (Measure Ω)` (Statlib's `ProbabilityTheory.IsEVar`)
+is a measurable `E : Ω → ℝ≥0∞` with `∫ᵉ ω, E ω - 1 ∂P ≠ ⊥` and `∫ᵉ ω, E ω - 1 ∂P ≤ 0` for every
+`P ∈ S`. For a null of finite measures this says `∫⁻ E ∂P ≤ P univ` for every `P ∈ S`
+(`ProbabilityTheory.IsEVar.of_lintegral_le_measure_univ`,
+`ProbabilityTheory.IsEVar.lintegral_le_measure_univ`), that is, `E` has expectation at most one
+under every probability measure of `S`. This file develops the first properties of e-variables
+that hypothesis testing uses:
+
+* the exact e-variables, with `∫⁻ E ∂P = P univ` for every `P ∈ 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.
+
+Following Statlib, the null is an arbitrary set of measures, with no dominating measure, and
+e-variables are `ℝ≥0∞`-valued.
+
+## Main definitions
+
+* `ProbabilityTheory.IsExactEVar E S`: `E` is an e-variable for `S` with `∫⁻ E ∂P = P univ` for
+  every `P ∈ S`, that is, with expectation exactly one under every probability measure of `S`.
+
+## Main statements
+
+* `ProbabilityTheory.IsEVar.lintegral_le_one`: an e-variable has expectation at most one under
+  every probability measure of the null.
+* `ProbabilityTheory.isEVar_iff_lintegral_le_one`, `ProbabilityTheory.isExactEVar_iff`: for a null
+  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.measure_inv_le_le`: **Markov's inequality** for e-variables,
+  `P {ω | α⁻¹ ≤ E ω} ≤ α`.
+* `ProbabilityTheory.IsEVar.lintegral_min_mul_le`: `∫⁻ ω, min (α * E ω) 1 ∂P ≤ α`.
+* `ProbabilityTheory.isEVar_finsetProd`, `ProbabilityTheory.isExactEVar_finsetProd`: a finite
+  product of (exact) e-variables, from a family that is independent under every member of the
+  null, is an (exact) e-variable. Statlib's `ProbabilityTheory.IsEVar.prod` treats the two
+  coordinates of a product space, where independence holds by construction.
+
+## References
+
+* 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
+  (2021).
+-/
+
+public section
+
+open MeasureTheory Set
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {Ω 𝓨 : Type*} {mΩ : MeasurableSpace Ω} {m𝓨 : MeasurableSpace 𝓨}
+  {S T : Set (Measure Ω)} {E F : Ω → ℝ≥0∞} {P : Measure Ω}
+
+/-- An e-variable has expectation at most one under every probability measure of the null. -/
+theorem IsEVar.lintegral_le_one (hE : IsEVar E S) (hP : P ∈ S) [IsProbabilityMeasure P] :
+    ∫⁻ ω, E ω ∂P ≤ 1 := by
+  simpa using hE.lintegral_le_measure_univ P hP
+
+/-- For a null of probability measures, `E` is an e-variable exactly when it is measurable and has
+expectation at most one under every member of the null. -/
+theorem isEVar_iff_lintegral_le_one (hS : ∀ P ∈ S, IsProbabilityMeasure P) :
+    IsEVar E S ↔ Measurable E ∧ ∀ P ∈ S, ∫⁻ ω, E ω ∂P ≤ 1 := by
+  refine ⟨fun hE ↦ ⟨hE.measurable, fun P hP ↦ ?_⟩,
+    fun h ↦ IsEVar.of_lintegral_le_one hS h.1 h.2⟩
+  have := hS P hP
+  exact hE.lintegral_le_one hP
+
+/-! ### Exact e-variables -/
+
+/-- An e-variable `E` for `S` is **exact** when `∫⁻ E ∂P = P univ` for every `P ∈ S`: for a null of
+probability measures, its expectation is exactly one under every member of the null. The
+normalization by `P univ` matches the one of Statlib's `IsEVar`, which asks
+`∫⁻ E ∂P ≤ P univ` for a finite measure `P`. -/
+structure IsExactEVar (E : Ω → ℝ≥0∞) (S : Set (Measure Ω)) : Prop extends IsEVar E S where
+  lintegral_eq_measure_univ : ∀ P ∈ S, ∫⁻ ω, E ω ∂P = P univ
+
+/-- An exact e-variable has expectation one under every probability measure of the null. -/
+theorem IsExactEVar.lintegral_eq_one (hE : IsExactEVar E S) (hP : P ∈ S)
+    [IsProbabilityMeasure P] :
+    ∫⁻ ω, E ω ∂P = 1 := by
+  simpa using hE.lintegral_eq_measure_univ P hP
+
+/-- For a null of probability measures, `E` is an exact e-variable exactly when it is measurable
+and has expectation one under every member of the null. -/
+theorem isExactEVar_iff (hS : ∀ P ∈ S, IsProbabilityMeasure P) :
+    IsExactEVar E S ↔ Measurable E ∧ ∀ P ∈ S, ∫⁻ ω, E ω ∂P = 1 := by
+  refine ⟨fun hE ↦ ⟨hE.measurable, fun P hP ↦ have := hS P hP; hE.lintegral_eq_one hP⟩,
+    fun h ↦ ⟨IsEVar.of_lintegral_le_one hS h.1 fun P hP ↦ (h.2 P hP).le, fun P hP ↦ ?_⟩⟩
+  have := hS P hP
+  simpa using h.2 P hP
+
+theorem IsExactEVar.of_lintegral_eq_one (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hE : Measurable E) (h : ∀ P ∈ S, ∫⁻ ω, E ω ∂P = 1) :
+    IsExactEVar E S :=
+  (isExactEVar_iff hS).2 ⟨hE, h⟩
+
+/-- The constant `1` is an exact e-variable for every null. -/
+theorem isExactEVar_one (S : Set (Measure Ω)) : IsExactEVar 1 S where
+  toIsEVar := isEVar_one S
+  lintegral_eq_measure_univ P _ := by simp
+
+theorem IsExactEVar.anti_set (hST : S ⊆ T) (hE : IsExactEVar E T) : IsExactEVar E S where
+  toIsEVar := hE.toIsEVar.anti_set hST
+  lintegral_eq_measure_univ P hP := hE.lintegral_eq_measure_univ P (hST hP)
+
+theorem IsExactEVar.congr (hE : IsExactEVar E S) (hF : Measurable F)
+    (hEF : ∀ P ∈ S, E =ᵐ[P] F) : IsExactEVar F S where
+  toIsEVar := hE.toIsEVar.congr hF hEF
+  lintegral_eq_measure_univ P hP := by
+    rw [← lintegral_congr_ae (hEF P hP), hE.lintegral_eq_measure_univ P hP]
+
+/-- The composition of an exact e-variable with a measurable map is an exact e-variable for the
+null of the measures whose image is in the original null. -/
+theorem IsExactEVar.comp {Y : 𝓨 → ℝ≥0∞} {φ : Ω → 𝓨} (hφ : Measurable φ)
+    (h : IsExactEVar Y {P.map φ | P ∈ S}) : IsExactEVar (Y ∘ φ) S where
+  toIsEVar := h.toIsEVar.comp hφ
+  lintegral_eq_measure_univ P hP := by
+    have h_eq := h.lintegral_eq_measure_univ (P.map φ) ⟨P, hP, rfl⟩
+    rwa [lintegral_map h.measurable hφ, Measure.map_apply hφ .univ, preimage_univ] at h_eq
+
+/-- A likelihood ratio `Q.rnDeriv P`, for `Q ≪ P` with the same finite total mass, is an exact
+e-variable for the simple null `{P}`. -/
+theorem isExactEVar_rnDeriv {Q : Measure Ω} [IsFiniteMeasure P] [Q.HaveLebesgueDecomposition P]
+    (hQP : Q ≪ P) (hQ : Q univ = P univ) :
+    IsExactEVar (Q.rnDeriv P) {P} where
+  toIsEVar := .of_lintegral_le_measure_univ (by simpa) (Measure.measurable_rnDeriv Q P)
+    (by simp [Measure.lintegral_rnDeriv hQP, hQ])
+  lintegral_eq_measure_univ := by simp [Measure.lintegral_rnDeriv hQP, hQ]
+
+/-! ### Markov's inequality -/
+
+/-- **Markov's inequality** for e-variables: for every probability measure `P` of the null and
+every level
+`α`, the e-variable reaches `α⁻¹` with probability at most `α`. -/
+theorem IsEVar.measure_inv_le_le (hE : IsEVar E S) (hP : P ∈ S) [IsProbabilityMeasure P]
+    (α : ℝ≥0∞) :
+    P {ω | α⁻¹ ≤ E ω} ≤ α := by
+  rcases eq_or_ne α 0 with rfl | hα₀
+  · -- at level `0`, the event is `{E = ∞}`, which is null since `E` is almost surely finite
+    refine (measure_eq_zero_iff_ae_notMem.2 ?_).le
+    filter_upwards [hE.ae_lt_top hP] with ω hω
+    simpa using hω.ne
+  rcases eq_or_ne α ∞ with rfl | hα_top
+  · exact le_top
+  calc P {ω | α⁻¹ ≤ E ω}
+  _ ≤ (∫⁻ ω, E ω ∂P) / α⁻¹ :=
+    meas_ge_le_lintegral_div hE.measurable.aemeasurable (by simpa) (by simpa)
+  _ ≤ 1 / α⁻¹ := by
+    gcongr
+    exact hE.lintegral_le_one hP
+  _ = α := by simp
+
+/-- The test that rejects when an e-variable reaches `α⁻¹` has level `α` under every probability
+measure of the null. -/
+theorem IsEVar.lintegral_indicator_le (hE : IsEVar E S) (hP : P ∈ S) [IsProbabilityMeasure P]
+    (α : ℝ≥0∞) :
+    ∫⁻ ω, {ω | α⁻¹ ≤ E ω}.indicator 1 ω ∂P ≤ α := by
+  rw [lintegral_indicator_one (measurableSet_le measurable_const hE.measurable)]
+  exact hE.measure_inv_le_le hP α
+
+/-- The randomized test `min (α * E) 1` of an e-variable `E` has expectation at most `α` under
+every probability measure of the null. -/
+theorem IsEVar.lintegral_min_mul_le (hE : IsEVar E S) (hP : P ∈ S) [IsProbabilityMeasure P]
+    (α : ℝ≥0∞) :
+    ∫⁻ ω, min (α * E ω) 1 ∂P ≤ α :=
+  calc ∫⁻ ω, min (α * E ω) 1 ∂P
+  _ ≤ ∫⁻ ω, α * E ω ∂P := lintegral_mono fun _ ↦ min_le_left _ _
+  _ = α * ∫⁻ ω, E ω ∂P := lintegral_const_mul α hE.measurable
+  _ ≤ α * 1 := by
+    gcongr
+    exact hE.lintegral_le_one hP
+  _ = α := mul_one α
+
+/-! ### Products of independent e-variables -/
+
+/-- A finite product `∏ i ∈ s, E i` of e-variables is an e-variable when the whole family `E` is
+independent under every member of the null, which makes the null a set of probability
+measures. -/
+theorem isEVar_finsetProd {ι : Type*} {E : ι → Ω → ℝ≥0∞} (s : Finset ι)
+    (hE : ∀ i ∈ s, IsEVar (E i) S) (hind : ∀ P ∈ S, iIndepFun E P) :
+    IsEVar (fun ω ↦ ∏ i ∈ s, E i ω) S := by
+  have hS : ∀ P ∈ S, IsProbabilityMeasure P := fun P hP ↦ (hind P hP).isProbabilityMeasure
+  refine .of_lintegral_le_one hS (Finset.measurable_fun_prod s fun i hi ↦ (hE i hi).measurable)
+    fun P hP ↦ ?_
+  have := hS P hP
+  rw [lintegral_prod_eq_prod_lintegral_of_indepFun' s (hind P hP)
+    fun i hi ↦ (hE i hi).measurable]
+  exact Finset.prod_le_one fun i hi ↦ (hE i hi).lintegral_le_one hP
+
+/-- A finite product `∏ i ∈ s, E i` of exact e-variables is an exact e-variable when the whole
+family `E` is independent under every member of the null, which makes the null a set of
+probability measures. -/
+theorem isExactEVar_finsetProd {ι : Type*} {E : ι → Ω → ℝ≥0∞} (s : Finset ι)
+    (hE : ∀ i ∈ s, IsExactEVar (E i) S) (hind : ∀ P ∈ S, iIndepFun E P) :
+    IsExactEVar (fun ω ↦ ∏ i ∈ s, E i ω) S := by
+  have hS : ∀ P ∈ S, IsProbabilityMeasure P := fun P hP ↦ (hind P hP).isProbabilityMeasure
+  refine .of_lintegral_eq_one hS (Finset.measurable_fun_prod s fun i hi ↦ (hE i hi).measurable)
+    fun P hP ↦ ?_
+  have := hS P hP
+  rw [lintegral_prod_eq_prod_lintegral_of_indepFun' s (hind P hP)
+    fun i hi ↦ (hE i hi).measurable]
+  exact Finset.prod_eq_one fun i hi ↦ (hE i hi).lintegral_eq_one hP
+
+end ProbabilityTheory

LMLExplore/EValues/PVariable.lean

@@ -0,0 +1,178 @@
+/-
+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.EVariable
+public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
+
+/-!
+# P-variables
+
+A p-variable for a null hypothesis `S : Set (Measure Ω)` is a measurable `p : Ω → ℝ≥0∞` with
+`P {ω | p ω ≤ α} ≤ α` for every member `P` of the null and every level `α`: rejecting when
+`p ≤ α` is a level-`α` test for every `α` at once. As for Statlib's e-variables, the null is an
+arbitrary set of measures and p-variables are `ℝ≥0∞`-valued; values above `1` carry no evidence.
+This file defines p-variables and exact p-variables, and proves that, for a null of probability
+measures, the inverse `E⁻¹` of an e-variable is a p-variable (the e-to-p calibration, with
+`0⁻¹ = ∞` and no truncation at `1`).
+
+## Main definitions
+
+* `ProbabilityTheory.IsPVar p S`: `p` is a p-variable for `S`.
+* `ProbabilityTheory.IsExactPVar p S`: `p` is a p-variable for `S` with `P {ω | p ω ≤ α} = α` for
+  every `P ∈ S` and every `α ≤ 1`.
+
+## Main statements
+
+* `ProbabilityTheory.IsEVar.isPVar_inv`: for a null of probability measures, the inverse of an
+  e-variable is a p-variable.
+* `ProbabilityTheory.isExactPVar_ofReal_volume`: the identity of `[0, 1]` under Lebesgue measure is
+  an exact p-variable, and `ProbabilityTheory.isExactPVar_ofReal_of_map_eq`: so is every random
+  variable uniformly distributed on `[0, 1]` under every member of the null.
+* `ProbabilityTheory.IsExactPVar.ae_le_one`: an exact p-variable is almost surely at most `1`
+  under every probability measure of the null.
+
+## References
+
+* A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in
+  Statistics 1 (2025), arXiv:2410.23614v6: Definition 1.2 and Proposition 2.1.
+-/
+
+public section
+
+open MeasureTheory Set
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {Ω 𝓨 : Type*} {mΩ : MeasurableSpace Ω} {m𝓨 : MeasurableSpace 𝓨}
+  {S T : Set (Measure Ω)} {p q : Ω → ℝ≥0∞} {E : Ω → ℝ≥0∞} {P : Measure Ω}
+
+/-- A measurable `p : Ω → ℝ≥0∞` is a **p-variable** for the null `S` when
+`P {ω | p ω ≤ α} ≤ α` for every `P ∈ S` and every level `α`. -/
+structure IsPVar (p : Ω → ℝ≥0∞) (S : Set (Measure Ω)) : Prop where
+  measurable : Measurable p := by fun_prop
+  measure_le_le : ∀ P ∈ S, ∀ α : ℝ≥0∞, P {ω | p ω ≤ α} ≤ α
+
+/-- For a simple null `{P}`, a p-variable is a measurable `p` with `P {p ≤ α} ≤ α` for every
+`α`. -/
+theorem isPVar_singleton_iff :
+    IsPVar p {P} ↔ Measurable p ∧ ∀ α : ℝ≥0∞, P {ω | p ω ≤ α} ≤ α :=
+  ⟨fun h ↦ ⟨h.measurable, h.measure_le_le P rfl⟩, fun h ↦ ⟨h.1, fun _ hQ ↦ hQ ▸ h.2⟩⟩
+
+theorem IsPVar.anti_set (hST : S ⊆ T) (hp : IsPVar p T) : IsPVar p S where
+  measurable := hp.measurable
+  measure_le_le P hP := hp.measure_le_le P (hST hP)
+
+theorem IsPVar.union (hS : IsPVar p S) (hT : IsPVar p T) : IsPVar p (S ∪ T) where
+  measurable := hS.measurable
+  measure_le_le P hP := hP.elim (hS.measure_le_le P) (hT.measure_le_le P)
+
+theorem isPVar_union_iff : IsPVar p (S ∪ T) ↔ IsPVar p S ∧ IsPVar p T :=
+  ⟨fun h ↦ ⟨h.anti_set subset_union_left, h.anti_set subset_union_right⟩,
+    fun h ↦ h.1.union h.2⟩
+
+/-- A measurable function almost surely at least a p-variable, under every member of the null, is a
+p-variable. -/
+theorem IsPVar.mono (hp : IsPVar p S) (hq : Measurable q) (hpq : ∀ P ∈ S, p ≤ᵐ[P] q) :
+    IsPVar q S where
+  measurable := hq
+  measure_le_le P hP α := by
+    refine le_trans (measure_mono_ae ?_) (hp.measure_le_le P hP α)
+    filter_upwards [hpq P hP] with ω hω hqα using hω.trans hqα
+
+theorem IsPVar.congr (hp : IsPVar p S) (hq : Measurable q) (hpq : ∀ P ∈ S, p =ᵐ[P] q) :
+    IsPVar q S :=
+  hp.mono hq fun P hP ↦ (hpq P hP).le
+
+/-- The composition of a p-variable with a measurable map is a p-variable for the null of the
+measures whose image is in the original null. -/
+theorem IsPVar.comp {q : 𝓨 → ℝ≥0∞} {φ : Ω → 𝓨} (hφ : Measurable φ)
+    (h : IsPVar q {P.map φ | P ∈ S}) : IsPVar (q ∘ φ) S where
+  measurable := h.measurable.comp hφ
+  measure_le_le P hP α := by
+    have h_le := h.measure_le_le (P.map φ) ⟨P, hP, rfl⟩ α
+    rwa [Measure.map_apply hφ (measurableSet_le h.measurable measurable_const)] at h_le
+
+/-- **E-to-p calibration**: for a null of probability measures, the inverse `E⁻¹` of an
+e-variable `E` is a p-variable. -/
+theorem IsEVar.isPVar_inv (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hE : IsEVar E S) :
+    IsPVar (fun ω ↦ (E ω)⁻¹) S where
+  measurable := hE.measurable.inv
+  measure_le_le P hP α := by
+    have := hS P hP
+    have h_set : {ω | (E ω)⁻¹ ≤ α} = {ω | α⁻¹ ≤ E ω} :=
+      Set.ext fun _ ↦ ENNReal.inv_le_iff_inv_le
+    rw [h_set]
+    exact hE.measure_inv_le_le hP α
+
+/-! ### Exact p-variables -/
+
+/-- A p-variable `p` for `S` is **exact** when `P {ω | p ω ≤ α} = α` for every `P ∈ S` and every
+`α ≤ 1`: under a probability measure of the null, `p` is then almost surely at most `1`
+(`IsExactPVar.ae_le_one`) and uniformly distributed on `[0, 1]`. -/
+structure IsExactPVar (p : Ω → ℝ≥0∞) (S : Set (Measure Ω)) : Prop extends IsPVar p S where
+  measure_le_eq : ∀ P ∈ S, ∀ α ≤ 1, P {ω | p ω ≤ α} = α
+
+theorem IsExactPVar.anti_set (hST : S ⊆ T) (hp : IsExactPVar p T) : IsExactPVar p S where
+  toIsPVar := hp.toIsPVar.anti_set hST
+  measure_le_eq P hP := hp.measure_le_eq P (hST hP)
+
+theorem IsExactPVar.congr (hp : IsExactPVar p S) (hq : Measurable q)
+    (hpq : ∀ P ∈ S, p =ᵐ[P] q) : IsExactPVar q S where
+  toIsPVar := hp.toIsPVar.congr hq hpq
+  measure_le_eq P hP α hα := by
+    refine (measure_congr ?_).trans (hp.measure_le_eq P hP α hα)
+    filter_upwards [hpq P hP] with ω hω
+    simp [hω]
+
+/-- The composition of an exact p-variable with a measurable map is an exact p-variable for the
+null of the measures whose image is in the original null. -/
+theorem IsExactPVar.comp {q : 𝓨 → ℝ≥0∞} {φ : Ω → 𝓨} (hφ : Measurable φ)
+    (h : IsExactPVar q {P.map φ | P ∈ S}) : IsExactPVar (q ∘ φ) S where
+  toIsPVar := h.toIsPVar.comp hφ
+  measure_le_eq P hP α hα := by
+    have h_eq := h.measure_le_eq (P.map φ) ⟨P, hP, rfl⟩ α hα
+    rwa [Measure.map_apply hφ (measurableSet_le h.measurable measurable_const)] at h_eq
+
+/-- An exact p-variable is almost surely at most `1` under every probability measure of the
+null. -/
+theorem IsExactPVar.ae_le_one (hp : IsExactPVar p S) (hP : P ∈ S) [IsProbabilityMeasure P] :
+    ∀ᵐ ω ∂P, p ω ≤ 1 := by
+  rw [ae_iff_measure_eq (measurableSet_le hp.measurable measurable_const).nullMeasurableSet,
+    hp.measure_le_eq P hP 1 le_rfl, measure_univ]
+
+/-- 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
+  -- the distribution function of the uniform law: `{x ∈ [0, 1] | x ≤ α}` has measure `min α 1`
+  have h_eq (α : ℝ≥0∞) :
+      volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x ≤ α} = min α 1 := by
+    rcases eq_or_ne α ∞ with rfl | hα
+    · simp
+    have h_set : {x : ℝ | ENNReal.ofReal x ≤ α} ∩ Icc 0 1 = Icc 0 (min α.toReal 1) := by
+      ext x
+      simp only [mem_inter_iff, mem_ofPred_eq, mem_Icc, le_min_iff,
+        ENNReal.ofReal_le_iff_le_toReal hα]
+      tauto
+    rw [Measure.restrict_apply (measurableSet_le ENNReal.measurable_ofReal measurable_const), h_set]
+    simp [ENNReal.ofReal_min, hα]
+  refine ⟨⟨ENNReal.measurable_ofReal, fun P hP α ↦ ?_⟩, fun P hP α hα ↦ ?_⟩
+  · rw [mem_singleton_iff.1 hP, h_eq]
+    exact min_le_left α 1
+  · rw [mem_singleton_iff.1 hP, h_eq, min_eq_left hα]
+
+/-- A real random variable `U` uniformly distributed on `[0, 1]` under every member of the null
+`S` is an exact p-variable for `S`. -/
+theorem isExactPVar_ofReal_of_map_eq {U : Ω → ℝ} (hU : Measurable U)
+    (hU_law : ∀ P ∈ S, P.map U = volume.restrict (Icc 0 1)) :
+    IsExactPVar (fun ω ↦ ENNReal.ofReal (U ω)) S := by
+  refine IsExactPVar.comp (q := fun x : ℝ ↦ ENNReal.ofReal x) hU
+    (isExactPVar_ofReal_volume.anti_set ?_)
+  rintro _ ⟨P, hP, rfl⟩
+  exact hU_law P hP
+
+end ProbabilityTheory