From 2a3137dadc216a6a018d235db70ec3189ac907ba Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 16:31:19 +0100 Subject: [PATCH 1/5] feat: p-variables, exact e- and p-variables, and Markov's inequality for e-variables MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define `ProbabilityTheory.IsPVar`, `IsExactPVar` and `IsExactEVar` for arbitrary nulls with ℝ≥0∞ values, prove Markov's inequality for e-variables, the e-to-p calibration `E ↦ E⁻¹`, the level-α tests `𝟙{α⁻¹ ≤ E}` and `min (α * E) 1`, and that finite products of e-variables that are independent under every member of the null are (exact) e-variables. Co-Authored-By: Claude Code --- LMLExplore/EValues/EVariable.lean | 213 ++++++++++++++++++++++++++++++ LMLExplore/EValues/PVariable.lean | 174 ++++++++++++++++++++++++ 2 files changed, 387 insertions(+) create mode 100644 LMLExplore/EValues/EVariable.lean create mode 100644 LMLExplore/EValues/PVariable.lean diff --git a/LMLExplore/EValues/EVariable.lean b/LMLExplore/EValues/EVariable.lean new file mode 100644 index 00000000..6d3c31be --- /dev/null +++ b/LMLExplore/EValues/EVariable.lean @@ -0,0 +1,213 @@ +/- +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 Mathlib.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 Ω)` is a measurable `E : Ω → ℝ≥0∞` with +expectation at most one under every member of `S` (Statlib's `ProbabilityTheory.IsEVar`). This +file develops the first properties of e-variables that hypothesis testing uses: + +* the e-variables whose expectation is exactly one under every member of the null; +* Markov's inequality, which makes `{α⁻¹ ≤ E}` the rejection region of a level-`α` test, and its + smoothed form `min (α * E) 1`; +* products of e-variables that are 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_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`: 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 that are 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 Ω} + +/-- 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 + simpa using hE.lintegral_le_measure_univ P 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 member `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 + simpa using hE.lintegral_le_measure_univ P hP + _ = α := by simp + +/-- The test that rejects when an e-variable reaches `α⁻¹` has level `α` under every member 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 member 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 + simpa using hE.lintegral_le_measure_univ P hP + _ = α := mul_one α + +/-! ### Products of independent e-variables -/ + +/-- The expectation of a finite product of e-variables that are independent under `P` is the +product of their expectations. -/ +private theorem lintegral_finsetProd_eq {ι : Type*} {E : ι → Ω → ℝ≥0∞} (s : Finset ι) + (hE : ∀ i ∈ s, IsEVar (E i) S) (hind : iIndepFun E P) : + ∫⁻ ω, ∏ i ∈ s, E i ω ∂P = ∏ i ∈ s, ∫⁻ ω, E i ω ∂P := by + simp_rw [← Finset.prod_coe_sort s] + exact lintegral_prod_eq_prod_lintegral_of_indepFun _ (fun i : s ↦ E i) + (hind.precomp Subtype.val_injective) fun i ↦ (hE i i.2).measurable + +/-- A finite product of e-variables that are independent under every member of the null is an +e-variable. -/ +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_finsetProd_eq s hE (hind P hP)] + exact Finset.prod_le_one fun i hi ↦ by simpa using (hE i hi).lintegral_le_measure_univ P hP + +/-- A finite product of exact e-variables that are independent under every member of the null is +an exact e-variable. -/ +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_finsetProd_eq s (fun i hi ↦ (hE i hi).toIsEVar) (hind P hP)] + exact Finset.prod_eq_one fun i hi ↦ (hE i hi).lintegral_eq_one hP + +end ProbabilityTheory diff --git a/LMLExplore/EValues/PVariable.lean b/LMLExplore/EValues/PVariable.lean new file mode 100644 index 00000000..e39db48f --- /dev/null +++ b/LMLExplore/EValues/PVariable.lean @@ -0,0 +1,174 @@ +/- +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 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`: 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]`. +* `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**: the inverse `E⁻¹` of an e-variable `E` is a p-variable, by Markov's +inequality. -/ +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 + simpa only [ENNReal.inv_le_iff_inv_le] using 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, Real.volume_Icc, sub_zero, ENNReal.ofReal_min, ENNReal.ofReal_toReal hα, + ENNReal.ofReal_one] + 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 `P` is an exact p-variable +for `{P}`. -/ +theorem isExactPVar_ofReal_of_map_eq {U : Ω → ℝ} (hU : Measurable U) + (hU_law : P.map U = volume.restrict (Icc 0 1)) : + IsExactPVar (fun ω ↦ ENNReal.ofReal (U ω)) {P} := by + have h_set : {Q.map U | Q ∈ ({P} : Set (Measure Ω))} = {volume.restrict (Icc (0 : ℝ) 1)} := by + ext Q + simp [hU_law, eq_comm] + exact IsExactPVar.comp (q := fun x : ℝ ↦ ENNReal.ofReal x) hU (h_set ▸ isExactPVar_ofReal_volume) + +end ProbabilityTheory From 18fa9c47e6c4100255f37204a85dd54ff79be9ab Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 17:28:15 +0100 Subject: [PATCH 2/5] refactor: address review of e- and p-variables Make the finite-product independence identity a public Mathlib-style lemma lintegral_prod_eq_prod_lintegral_of_indepFun' requiring measurability only on s, add IsEVar.lintegral_le_one, generalize isExactPVar_ofReal_of_map_eq to an arbitrary null, shorten the uniform-law rewrite chain and make docstrings precise about probability measures and family-wide independence. Co-Authored-By: Claude Code --- LMLExplore/EValues/EVariable.lean | 66 ++++++++++--------- LMLExplore/EValues/PVariable.lean | 23 ++++--- .../Probability/Independence/Integration.lean | 43 ++++++++++++ 3 files changed, 89 insertions(+), 43 deletions(-) create mode 100644 LMLExplore/Probability/Independence/Integration.lean diff --git a/LMLExplore/EValues/EVariable.lean b/LMLExplore/EValues/EVariable.lean index 6d3c31be..c29d5786 100644 --- a/LMLExplore/EValues/EVariable.lean +++ b/LMLExplore/EValues/EVariable.lean @@ -6,20 +6,21 @@ Authors: LMLExplore contributors module public import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym -public import Mathlib.Probability.Independence.Integration +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 Ω)` is a measurable `E : Ω → ℝ≥0∞` with -expectation at most one under every member of `S` (Statlib's `ProbabilityTheory.IsEVar`). This -file develops the first properties of e-variables that hypothesis testing uses: +`∫⁻ E ∂P ≤ P univ` for every `P ∈ S` (Statlib's `ProbabilityTheory.IsEVar`), that is, with +expectation at most one under every probability measure of `S`. This file develops the first +properties of e-variables that hypothesis testing uses: -* the e-variables whose expectation is exactly one under every member of the null; +* 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 that are independent under every member of the null. +* 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. @@ -31,6 +32,8 @@ e-variables are `ℝ≥0∞`-valued. ## 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`: a likelihood ratio `Q.rnDeriv P` with `Q ≪ P` and @@ -39,9 +42,9 @@ e-variables are `ℝ≥0∞`-valued. `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 that are 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. + 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 @@ -61,6 +64,11 @@ 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) : @@ -68,7 +76,7 @@ theorem isEVar_iff_lintegral_le_one (hS : ∀ P ∈ S, IsProbabilityMeasure P) : refine ⟨fun hE ↦ ⟨hE.measurable, fun P hP ↦ ?_⟩, fun h ↦ IsEVar.of_lintegral_le_one hS h.1 h.2⟩ have := hS P hP - simpa using hE.lintegral_le_measure_univ P hP + exact hE.lintegral_le_one hP /-! ### Exact e-variables -/ @@ -134,7 +142,8 @@ theorem isExactEVar_rnDeriv {Q : Measure Ω} [IsFiniteMeasure P] [Q.HaveLebesgue /-! ### Markov's inequality -/ -/-- **Markov's inequality** for e-variables: for every member `P` of the null and every level +/-- **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∞) : @@ -151,11 +160,11 @@ theorem IsEVar.measure_inv_le_le (hE : IsEVar E S) (hP : P ∈ S) [IsProbability meas_ge_le_lintegral_div hE.measurable.aemeasurable (by simpa) (by simpa) _ ≤ 1 / α⁻¹ := by gcongr - simpa using hE.lintegral_le_measure_univ P hP + exact hE.lintegral_le_one hP _ = α := by simp -/-- The test that rejects when an e-variable reaches `α⁻¹` has level `α` under every member of -the null. -/ +/-- 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 @@ -163,7 +172,7 @@ theorem IsEVar.lintegral_indicator_le (hE : IsEVar E S) (hP : P ∈ S) [IsProbab exact hE.measure_inv_le_le hP α /-- The randomized test `min (α * E) 1` of an e-variable `E` has expectation at most `α` under -every member of the null. -/ +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 ≤ α := @@ -172,22 +181,14 @@ theorem IsEVar.lintegral_min_mul_le (hE : IsEVar E S) (hP : P ∈ S) [IsProbabil _ = α * ∫⁻ ω, E ω ∂P := lintegral_const_mul α hE.measurable _ ≤ α * 1 := by gcongr - simpa using hE.lintegral_le_measure_univ P hP + exact hE.lintegral_le_one hP _ = α := mul_one α /-! ### Products of independent e-variables -/ -/-- The expectation of a finite product of e-variables that are independent under `P` is the -product of their expectations. -/ -private theorem lintegral_finsetProd_eq {ι : Type*} {E : ι → Ω → ℝ≥0∞} (s : Finset ι) - (hE : ∀ i ∈ s, IsEVar (E i) S) (hind : iIndepFun E P) : - ∫⁻ ω, ∏ i ∈ s, E i ω ∂P = ∏ i ∈ s, ∫⁻ ω, E i ω ∂P := by - simp_rw [← Finset.prod_coe_sort s] - exact lintegral_prod_eq_prod_lintegral_of_indepFun _ (fun i : s ↦ E i) - (hind.precomp Subtype.val_injective) fun i ↦ (hE i i.2).measurable - -/-- A finite product of e-variables that are independent under every member of the null is an -e-variable. -/ +/-- 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 @@ -195,11 +196,13 @@ theorem isEVar_finsetProd {ι : Type*} {E : ι → Ω → ℝ≥0∞} (s : Finse 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_finsetProd_eq s hE (hind P hP)] - exact Finset.prod_le_one fun i hi ↦ by simpa using (hE i hi).lintegral_le_measure_univ 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 of exact e-variables that are independent under every member of the null is -an exact e-variable. -/ +/-- 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 @@ -207,7 +210,8 @@ theorem isExactEVar_finsetProd {ι : Type*} {E : ι → Ω → ℝ≥0∞} (s : 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_finsetProd_eq s (fun i hi ↦ (hE i hi).toIsEVar) (hind 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 diff --git a/LMLExplore/EValues/PVariable.lean b/LMLExplore/EValues/PVariable.lean index e39db48f..d4ea7b14 100644 --- a/LMLExplore/EValues/PVariable.lean +++ b/LMLExplore/EValues/PVariable.lean @@ -29,7 +29,7 @@ e-variable is a p-variable (the e-to-p calibration, with `0⁻¹ = ∞` and no t * `ProbabilityTheory.IsEVar.isPVar_inv`: 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]`. + 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. @@ -153,22 +153,21 @@ theorem isExactPVar_ofReal_volume : 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, Real.volume_Icc, sub_zero, ENNReal.ofReal_min, ENNReal.ofReal_toReal hα, - ENNReal.ofReal_one] + 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 `P` is an exact p-variable -for `{P}`. -/ +/-- 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.map U = volume.restrict (Icc 0 1)) : - IsExactPVar (fun ω ↦ ENNReal.ofReal (U ω)) {P} := by - have h_set : {Q.map U | Q ∈ ({P} : Set (Measure Ω))} = {volume.restrict (Icc (0 : ℝ) 1)} := by - ext Q - simp [hU_law, eq_comm] - exact IsExactPVar.comp (q := fun x : ℝ ↦ ENNReal.ofReal x) hU (h_set ▸ isExactPVar_ofReal_volume) + (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 diff --git a/LMLExplore/Probability/Independence/Integration.lean b/LMLExplore/Probability/Independence/Integration.lean new file mode 100644 index 00000000..5fe87a3c --- /dev/null +++ b/LMLExplore/Probability/Independence/Integration.lean @@ -0,0 +1,43 @@ +/- +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.Integration + +/-! +# Expectation of a finite product of independent random variables + +Mathlib's `ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFun` computes the +expectation of `∏ i ∈ s, X i` for an independent family `X`, assuming every `X i` measurable. +This file proves the same identity assuming measurability only of the factors `X i` with +`i ∈ s`. + +## Main statements + +* `ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFun'`: for an independent family + `X` whose factors in `s` are measurable, `∫⁻ ∏ i ∈ s, X i = ∏ i ∈ s, ∫⁻ X i`. +-/ + +public section + +open MeasureTheory +open scoped ENNReal + +namespace ProbabilityTheory + +variable {Ω ι : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} + +/-- The expectation of a finite product of independent `ℝ≥0∞`-valued random variables is the +product of their expectations. Unlike `lintegral_prod_eq_prod_lintegral_of_indepFun`, only the +factors indexed by `s` need to be measurable. -/ +theorem lintegral_prod_eq_prod_lintegral_of_indepFun' (s : Finset ι) {X : ι → Ω → ℝ≥0∞} + (hX : iIndepFun X μ) (x_mea : ∀ i ∈ s, Measurable (X i)) : + ∫⁻ ω, ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ ω, X i ω ∂μ := by + simp_rw [← Finset.prod_coe_sort s] + exact lintegral_prod_eq_prod_lintegral_of_indepFun _ (fun i : s ↦ X i) + (hX.precomp Subtype.val_injective) fun i ↦ x_mea i i.2 + +end ProbabilityTheory From 4a062febdf65974cff0a8b121ed43c8c6fe6e5d2 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 17:49:05 +0100 Subject: [PATCH 3/5] doc: state the probability-measure hypothesis of the e-to-p calibration Co-Authored-By: Claude Code --- LMLExplore/EValues/PVariable.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/LMLExplore/EValues/PVariable.lean b/LMLExplore/EValues/PVariable.lean index d4ea7b14..8b4b99a0 100644 --- a/LMLExplore/EValues/PVariable.lean +++ b/LMLExplore/EValues/PVariable.lean @@ -15,8 +15,9 @@ A p-variable for a null hypothesis `S : Set (Measure Ω)` is a measurable `p : `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 the inverse `E⁻¹` of an -e-variable is a p-variable (the e-to-p calibration, with `0⁻¹ = ∞` and no truncation at `1`). +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 @@ -26,7 +27,8 @@ e-variable is a p-variable (the e-to-p calibration, with `0⁻¹ = ∞` and no t ## Main statements -* `ProbabilityTheory.IsEVar.isPVar_inv`: the inverse of an e-variable is a p-variable. +* `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. @@ -95,8 +97,8 @@ theorem IsPVar.comp {q : 𝓨 → ℝ≥0∞} {φ : Ω → 𝓨} (hφ : Measurab 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**: the inverse `E⁻¹` of an e-variable `E` is a p-variable, by Markov's -inequality. -/ +/-- **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 From 1fb2af55f597692386c38db4339bb2128193684f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 18:09:26 +0100 Subject: [PATCH 4/5] doc: state IsEVar via the extended integral in the e-variable module docstring MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Statlib's IsEVar asks ∫ᵉ (E - 1) ∂P ≠ ⊥ and ≤ 0; the ∫⁻ E ∂P ≤ P univ form is equivalent only for finite measures, so say so and cite the two Statlib bridge lemmas. Also record the finiteness hypothesis of isExactEVar_rnDeriv in the module summary. Co-Authored-By: Claude Code --- LMLExplore/EValues/EVariable.lean | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/LMLExplore/EValues/EVariable.lean b/LMLExplore/EValues/EVariable.lean index c29d5786..30450c1a 100644 --- a/LMLExplore/EValues/EVariable.lean +++ b/LMLExplore/EValues/EVariable.lean @@ -12,10 +12,13 @@ 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 Ω)` is a measurable `E : Ω → ℝ≥0∞` with -`∫⁻ E ∂P ≤ P univ` for every `P ∈ S` (Statlib's `ProbabilityTheory.IsEVar`), that is, with -expectation at most one under every probability measure of `S`. This file develops the first -properties of e-variables that hypothesis testing uses: +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 @@ -36,8 +39,8 @@ e-variables are `ℝ≥0∞`-valued. 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`: a likelihood ratio `Q.rnDeriv P` with `Q ≪ P` and - `Q univ = P univ` is an exact e-variable for `{P}`. +* `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 ≤ α`. From 54c7ed4fc9b743d819ec47d9fdb5f72f129f8785 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 18:33:48 +0100 Subject: [PATCH 5/5] refactor: state the inverse-level set equality in the e-to-p calibration Co-Authored-By: Claude Code --- LMLExplore/EValues/PVariable.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/LMLExplore/EValues/PVariable.lean b/LMLExplore/EValues/PVariable.lean index 8b4b99a0..2f3b8059 100644 --- a/LMLExplore/EValues/PVariable.lean +++ b/LMLExplore/EValues/PVariable.lean @@ -104,7 +104,10 @@ theorem IsEVar.isPVar_inv (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hE : IsEVa measurable := hE.measurable.inv measure_le_le P hP α := by have := hS P hP - simpa only [ENNReal.inv_le_iff_inv_le] using hE.measure_inv_le_le 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 -/