From b7491973617fbfe19e8eef8b5480d4783263e914 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 18:03:00 +0100 Subject: [PATCH 1/5] feat: the effective null: mixtures, convexity, solidity, setwise closure and tests Co-Authored-By: Claude Code --- LMLExplore/EValues/EffectiveSet.lean | 222 ++++++++++++++++++ .../MeasureTheory/Integral/Lebesgue/Add.lean | 46 +++- 2 files changed, 266 insertions(+), 2 deletions(-) create mode 100644 LMLExplore/EValues/EffectiveSet.lean diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean new file mode 100644 index 00000000..5d130c9a --- /dev/null +++ b/LMLExplore/EValues/EffectiveSet.lean @@ -0,0 +1,222 @@ +/- +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 Statlib.EValues.RIPr +public import LMLExplore.MeasureTheory.Integral.Lebesgue.Add + +/-! +# The effective null + +The effective null of a null hypothesis `S : Set (Measure Ω)` is Statlib's `effectiveSet S`: the +measures `μ` under which every e-variable `X` for `S` has `∫⁻ X ∂μ ≤ 1`. It is the set over which +Statlib's duality `maxUtility_eq_iInf_klIntegral_effectiveSet` minimizes, and it describes the +alternatives that a null can be tested against: e-variables cannot distinguish `S` from its +effective null, and every probability measure outside of it is detected by a level-`α` test. + +This file proves the structural properties of the effective null, for any set of measures `S` on +any measurable space, with no dominating measure and no convexity. + +## Main statements + +* `ProbabilityTheory.subset_effectiveSet_iff`: `S ⊆ effectiveSet S` exactly when every member of + `S` has mass at most `1`. +* `ProbabilityTheory.comp_mem_effectiveSet`: the effective null contains every mixture `κ ∘ₘ π` of + members of the effective null over a measure `π` of mass at most `1`, in particular every mixture + of members of `S` over a probability measure. +* `ProbabilityTheory.convex_effectiveSet`, `ProbabilityTheory.convexHull_subset_effectiveSet`: the + effective null is convex, and contains the convex hull of `S`. +* `ProbabilityTheory.isLowerSet_effectiveSet`: the effective null is solid. +* `ProbabilityTheory.mem_effectiveSet_of_tendsto`: the effective null is closed under setwise + convergence, along any filter. +* `ProbabilityTheory.isEVar_effectiveSet_inter_iff`: `S` and the probability measures of its + effective null have the same e-variables, so that + `ProbabilityTheory.effectiveSet_effectiveSet_inter` they have the same effective null. +* `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_test_iff_notMem_effectiveSet`: a measure `Q` admits, for some + `α ∈ (0, 1)`, a level-`α` test for `S` with power larger than `α` under `Q` exactly when `Q` is + not in the effective null of `S` [RW, Theorem 6.10]. + +## References + +* [LRR25] M. Larsson, A. Ramdas and J. Ruf, *The numeraire e-variable and reverse information + projection*, Ann. Statist. 53 (2025), arXiv:2402.18810, Definition 3.1 and Lemma 4.5. +* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in + Statistics 1 (2025), arXiv:2410.23614v6, §6.3.1 and Theorem 6.10. +-/ + +public section + +open MeasureTheory Filter Set + +open scoped ENNReal Topology + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S T : Set (Measure Ω)} {μ ν Q : Measure Ω} + +/-- The effective null is monotone in the null. -/ +theorem effectiveSet_mono (hST : S ⊆ T) : effectiveSet S ⊆ effectiveSet T := + fun _ hμ X hX ↦ hμ X (hX.anti_set hST) + +/-- A null is contained in its effective null exactly when each of its members has mass at +most `1`; in particular a null of probability measures is contained in its effective null. -/ +theorem subset_effectiveSet_iff : S ⊆ effectiveSet S ↔ ∀ P ∈ S, P univ ≤ 1 := + ⟨fun h _ hP ↦ measure_univ_le_one_of_mem_effectiveSet (h hP), + fun hS P hP _ hX ↦ (hX.lintegral_le_measure_univ P hP).trans (hS P hP)⟩ + +/-- A null of measures of mass at most `1` is contained in its effective null. -/ +theorem subset_effectiveSet (hS : ∀ P ∈ S, P univ ≤ 1) : S ⊆ effectiveSet S := + subset_effectiveSet_iff.mpr hS + +/-- The effective null contains every mixture `κ ∘ₘ π` over a measure `π` of mass at most `1` of +a kernel `κ` whose values are `π`-almost surely in the effective null. With +`subset_effectiveSet`, this contains every mixture over a probability measure of a kernel with +values in a null of probability measures [LRR25, Definition 3.1]. -/ +theorem comp_mem_effectiveSet {Θ : Type*} {mΘ : MeasurableSpace Θ} {π : Measure Θ} + {κ : Kernel Θ Ω} (hπ : π univ ≤ 1) (hκ : ∀ᵐ θ ∂π, κ θ ∈ effectiveSet S) : + κ ∘ₘ π ∈ effectiveSet S := by + intro X hX + rw [Measure.lintegral_bind κ.aemeasurable hX.measurable.aemeasurable] + calc ∫⁻ θ, ∫⁻ ω, X ω ∂κ θ ∂π + _ ≤ ∫⁻ _, 1 ∂π := lintegral_mono_ae (hκ.mono fun θ hθ ↦ hθ X hX) + _ ≤ 1 := by simpa using hπ + +/-- The effective null is convex. -/ +theorem convex_effectiveSet : Convex ℝ≥0∞ (effectiveSet S) := by + intro μ hμ ν hν a b _ _ hab + -- A convex combination is a mixture over the two-point space `Bool`. + have h_eq : Kernel.boolKernel μ ν ∘ₘ (a • Measure.dirac false + b • Measure.dirac true) = + a • μ + b • ν := by + simp [Measure.comp_add, Measure.comp_smul, Measure.dirac_bind (Kernel.measurable _)] + rw [← h_eq] + refine comp_mem_effectiveSet (by simp [hab]) (.of_forall fun x ↦ ?_) + cases x <;> simpa + +/-- The effective null of a null of measures of mass at most `1` contains its convex hull. -/ +theorem convexHull_subset_effectiveSet (hS : ∀ P ∈ S, P univ ≤ 1) : + convexHull ℝ≥0∞ S ⊆ effectiveSet S := + convexHull_min (subset_effectiveSet hS) convex_effectiveSet + +/-- The effective null is solid: a measure below a member of the effective null is a member. -/ +theorem isLowerSet_effectiveSet : IsLowerSet (effectiveSet S) := + fun _ _ hμν hν X hX ↦ (lintegral_mono' hμν le_rfl).trans (hν X hX) + +/-- A measure below a member of the effective null is a member of the effective null. -/ +theorem mem_effectiveSet_of_le (hν : ν ∈ effectiveSet S) (hμν : μ ≤ ν) : μ ∈ effectiveSet S := + isLowerSet_effectiveSet hμν hν + +/-- The effective null is closed under setwise convergence: if `μs i s` tends to `μ s` along a +filter for every measurable set `s`, and `μs i` is eventually in the effective null, then so is +`μ`. The filter is arbitrary, so that the effective null is closed for the topology of setwise +convergence and not only sequentially closed. -/ +theorem mem_effectiveSet_of_tendsto {ι : Type*} {l : Filter ι} [l.NeBot] {μs : ι → Measure Ω} + (hμs : ∀ᶠ i in l, μs i ∈ effectiveSet S) + (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : + μ ∈ effectiveSet S := fun X hX ↦ + (lintegral_le_liminf_lintegral_of_tendsto_measure hX.measurable h).trans + (liminf_le_of_frequently_le (hμs.mono fun _ hi ↦ hi X hX).frequently) + +/-- 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) + by_cases hω : ω ∈ s <;> simp [hω] + by_contra h_ne + simp [ENNReal.top_mul h_ne] at 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 + +/-- The e-variables for the probability measures of the effective null of `S` are e-variables +for `S`. -/ +theorem IsEVar.effectiveSet_inter {X : Ω → ℝ≥0∞} (hX : IsEVar X S) : + IsEVar X (effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) := + .of_lintegral_le_one (S := effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) (fun _ hμ ↦ hμ.2) + hX.measurable fun _ hμ ↦ hμ.1 X hX + +/-- A null of probability measures and the probability measures of its effective null have the +same e-variables. -/ +theorem isEVar_effectiveSet_inter_iff (hS : ∀ P ∈ S, IsProbabilityMeasure P) {X : Ω → ℝ≥0∞} : + IsEVar X (effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) ↔ IsEVar X S := by + refine ⟨fun hX ↦ hX.anti_set fun P hP ↦ ?_, IsEVar.effectiveSet_inter⟩ + exact ⟨subset_effectiveSet (fun P hP ↦ (hS P hP).measure_univ.le) hP, hS P hP⟩ + +/-- A null of probability measures and the probability measures of its effective null have the +same effective null. -/ +theorem effectiveSet_effectiveSet_inter (hS : ∀ P ∈ S, IsProbabilityMeasure P) : + effectiveSet (effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) = effectiveSet S := by + ext μ + simp only [mem_effectiveSet_iff, isEVar_effectiveSet_inter_iff hS] + +/-- A measure `Q` is outside the effective null of a null `S` of probability measures exactly +when, for some level `α ∈ (0, 1)`, some level-`α` test `φ` for `S` (a measurable function with +values in `[0, 1]` and expectation at most `α` under every member of `S`) has expectation larger +than `α` under `Q` [RW, Theorem 6.10]. -/ +theorem exists_test_iff_notMem_effectiveSet (hS : ∀ P ∈ S, IsProbabilityMeasure P) : + (∃ α : ℝ≥0∞, 0 < α ∧ α < 1 ∧ ∃ φ : Ω → ℝ≥0∞, Measurable φ ∧ φ ≤ 1 ∧ + (∀ P ∈ S, ∫⁻ ω, φ ω ∂P ≤ α) ∧ α < ∫⁻ ω, φ ω ∂Q) ↔ Q ∉ effectiveSet S := by + constructor + · rintro ⟨α, hα0, hα1, φ, hφ, -, hφS, hφQ⟩ hQ + -- `α⁻¹ * φ` is an e-variable for `S`, so its expectation under `Q` is at most `1`. + have hX : IsEVar (fun ω ↦ α⁻¹ * φ ω) S := by + refine .of_lintegral_le_one hS (measurable_const.mul hφ) fun P hP ↦ ?_ + rw [lintegral_const_mul _ hφ] + exact ENNReal.inv_mul_le_iff hα0.ne' (hα1.trans ENNReal.one_lt_top).ne |>.mpr <| + by simpa using hφS P hP + have h := hQ _ hX + rw [lintegral_const_mul _ hφ, + ENNReal.inv_mul_le_iff hα0.ne' (hα1.trans ENNReal.one_lt_top).ne, mul_one] at h + exact (h.trans_lt hφQ).false + · -- An e-variable with expectation larger than `1` under `Q`, truncated at a large level `N` + -- and divided by `N`, is a level-`N⁻¹` test with power larger than `N⁻¹` under `Q`. + intro hQ + obtain ⟨X, hX, hXQ⟩ : ∃ X, IsEVar X S ∧ 1 < ∫⁻ ω, X ω ∂Q := by + simpa [mem_effectiveSet_iff] using hQ + -- By monotone convergence, the truncations `min X N` have expectation larger than `1` under + -- `Q` from some level `N ≥ 2` on. + have hXm := hX.measurable + have h_tendsto : Tendsto (fun N : ℕ ↦ ∫⁻ ω, min (X ω) N ∂Q) atTop (𝓝 (∫⁻ ω, X ω ∂Q)) := by + refine lintegral_tendsto_of_tendsto_of_monotone (fun N ↦ by fun_prop) (.of_forall + fun ω N M hNM ↦ min_le_min_left _ (by exact_mod_cast hNM)) (.of_forall fun ω ↦ ?_) + simpa using (tendsto_const_nhds (x := X ω)).min ENNReal.tendsto_nat_nhds_top + obtain ⟨N, hNQ, hN2⟩ := ((h_tendsto.eventually (lt_mem_nhds hXQ)).and + (eventually_ge_atTop 2)).exists + have hN0 : (N : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : N ≠ 0) + have hNtop : (N : ℝ≥0∞) ≠ ∞ := ENNReal.natCast_ne_top N + refine ⟨(N : ℝ≥0∞)⁻¹, ENNReal.inv_pos.mpr hNtop, ENNReal.inv_lt_one.mpr + (by exact_mod_cast (by omega : 1 < N)), fun ω ↦ (N : ℝ≥0∞)⁻¹ * min (X ω) N, by fun_prop, + fun ω ↦ ?_, fun P hP ↦ ?_, ?_⟩ + · calc (N : ℝ≥0∞)⁻¹ * min (X ω) N ≤ (N : ℝ≥0∞)⁻¹ * N := by gcongr; exact min_le_right _ _ + _ = 1 := ENNReal.inv_mul_cancel hN0 hNtop + · have := hS P hP + rw [lintegral_const_mul _ (by fun_prop)] + calc (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, min (X ω) N ∂P ≤ (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, X ω ∂P := by + gcongr with ω; exact min_le_left _ _ + _ ≤ (N : ℝ≥0∞)⁻¹ * 1 := by + gcongr; simpa using hX.lintegral_le_measure_univ P hP + _ = (N : ℝ≥0∞)⁻¹ := mul_one _ + · rw [lintegral_const_mul _ (by fun_prop)] + calc (N : ℝ≥0∞)⁻¹ = (N : ℝ≥0∞)⁻¹ * 1 := (mul_one _).symm + _ < (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, min (X ω) N ∂Q := + ENNReal.mul_lt_mul_right (ENNReal.inv_ne_zero.mpr hNtop) (ENNReal.inv_ne_top.mpr hN0) + hNQ + +end ProbabilityTheory diff --git a/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean b/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean index 24bcbe51..10640367 100644 --- a/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean +++ b/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean @@ -6,20 +6,29 @@ Authors: LMLExplore contributors module public import Mathlib.MeasureTheory.Integral.Lebesgue.Add +public import Mathlib.Topology.Instances.ENNReal.Lemmas /-! -# Lebesgue integral of a finite sum of indicators +# Lebesgue integral of finite sums and lower semicontinuity under setwise convergence ## Main statements * `MeasureTheory.lintegral_finsetSum_indicator_one`: the Lebesgue integral of a finite sum of indicators of measurable sets is the sum of their measures, and `MeasureTheory.lintegral_finsetSum_indicator_one₀`, its version for null measurable sets. +* `MeasureTheory.SimpleFunc.tendsto_lintegral_of_tendsto_measure`: the integral of a simple function + with finite values is continuous for the setwise convergence of measures. +* `MeasureTheory.lintegral_le_liminf_lintegral_of_tendsto_measure`: the Lebesgue integral of a + measurable function is lower semicontinuous for the setwise convergence of measures, along any + filter. This is the setwise counterpart of the portmanteau inequality + `MeasureTheory.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure`. -/ public section -open scoped ENNReal +open Filter + +open scoped ENNReal Topology namespace MeasureTheory @@ -39,4 +48,37 @@ lemma lintegral_finsetSum_indicator_one (hS : ∀ i ∈ s, MeasurableSet (S i)) ∫⁻ a, ∑ i ∈ s, (S i).indicator 1 a ∂μ = ∑ i ∈ s, μ (S i) := lintegral_finsetSum_indicator_one₀ fun i hi ↦ (hS i hi).nullMeasurableSet +section Setwise + +variable {ι : Type*} {l : Filter ι} {μs : ι → Measure α} + +/-- The integral of a simple function with finite values is continuous for the setwise convergence +of measures. -/ +theorem SimpleFunc.tendsto_lintegral_of_tendsto_measure (f : SimpleFunc α ℝ≥0∞) + (hf : ∀ y ∈ f.range, y ≠ ∞) + (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : + Tendsto (fun i ↦ f.lintegral (μs i)) l (𝓝 (f.lintegral μ)) := + tendsto_finsetSum _ fun y hy ↦ + ENNReal.Tendsto.const_mul (h _ (f.measurableSet_preimage _)) (.inr (hf y hy)) + +/-- **Lower semicontinuity of the Lebesgue integral under setwise convergence.** If `μs i s` +tends to `μ s` along a filter for every measurable set `s`, then +`∫⁻ f ∂μ ≤ liminf (∫⁻ f ∂μs i)` for every measurable `f`. The filter is arbitrary, so this holds +for nets of measures and not only for sequences. -/ +theorem lintegral_le_liminf_lintegral_of_tendsto_measure [l.NeBot] {f : α → ℝ≥0∞} + (hf : Measurable f) (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : + ∫⁻ x, f x ∂μ ≤ liminf (fun i ↦ ∫⁻ x, f x ∂μs i) l := by + rw [lintegral_eq_iSup_eapprox_lintegral hf] + refine iSup_le fun n ↦ ?_ + have h_tendsto := (SimpleFunc.eapprox f n).tendsto_lintegral_of_tendsto_measure + (fun y hy ↦ by + obtain ⟨x, rfl⟩ := SimpleFunc.mem_range.mp hy + exact (SimpleFunc.eapprox_lt_top f n x).ne) h + rw [← h_tendsto.liminf_eq] + refine liminf_le_liminf (.of_forall fun i ↦ ?_) + rw [lintegral_eq_iSup_eapprox_lintegral hf] + exact le_iSup (fun n ↦ (SimpleFunc.eapprox f n).lintegral (μs i)) n + +end Setwise + end MeasureTheory From 1dbe5ff01da2904675e711e8a1e4fbf8ea807032 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 19:19:54 +0100 Subject: [PATCH 2/5] fix: address review of the effective null MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Generalise the lower semicontinuity of `∫⁻` to the hypothesis `μ s ≤ liminf (μs i s)`, as `lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure`, through the new `SimpleFunc.lintegral_le_liminf_lintegral` and TauCeti's `ENNReal.sum_liminf_le_liminf_sum`. - Factor the truncation step out as `exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet`, and cite [RW, Fact 3.6]. - Tag `effectiveSet_mono` with `@[gcongr]`. - Fix the docstring of `IsEVar.effectiveSet_inter` and the module's main-statements list. - Unfold `SimpleFunc.lintegral` explicitly. Co-Authored-By: Claude Code --- LMLExplore/EValues/EffectiveSet.lean | 89 +++++++++++-------- .../MeasureTheory/Integral/Lebesgue/Add.lean | 57 +++++++----- 2 files changed, 90 insertions(+), 56 deletions(-) diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean index 5d130c9a..61949411 100644 --- a/LMLExplore/EValues/EffectiveSet.lean +++ b/LMLExplore/EValues/EffectiveSet.lean @@ -17,8 +17,9 @@ Statlib's duality `maxUtility_eq_iInf_klIntegral_effectiveSet` minimizes, and it alternatives that a null can be tested against: e-variables cannot distinguish `S` from its effective null, and every probability measure outside of it is detected by a level-`α` test. -This file proves the structural properties of the effective null, for any set of measures `S` on -any measurable space, with no dominating measure and no convexity. +This file proves the structural properties of the effective null on any measurable space, with no +dominating measure and no convexity. Unless stated otherwise below, the results hold for any set of +measures `S`. ## Main statements @@ -32,21 +33,23 @@ any measurable space, with no dominating measure and no convexity. * `ProbabilityTheory.isLowerSet_effectiveSet`: the effective null is solid. * `ProbabilityTheory.mem_effectiveSet_of_tendsto`: the effective null is closed under setwise convergence, along any filter. -* `ProbabilityTheory.isEVar_effectiveSet_inter_iff`: `S` and the probability measures of its - effective null have the same e-variables, so that - `ProbabilityTheory.effectiveSet_effectiveSet_inter` they have the same effective null. +* `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.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_test_iff_notMem_effectiveSet`: a measure `Q` admits, for some - `α ∈ (0, 1)`, a level-`α` test for `S` with power larger than `α` under `Q` exactly when `Q` is - not in the effective null of `S` [RW, Theorem 6.10]. +* `ProbabilityTheory.exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet`: for a null `S` of + finite measures, a measure outside the effective null of `S` is detected by a bounded e-variable. +* `ProbabilityTheory.exists_test_iff_notMem_effectiveSet`: for a null `S` of probability measures, + a measure `Q` admits, for some `α ∈ (0, 1)`, a level-`α` test for `S` with power larger than `α` + under `Q` exactly when `Q` is not in the effective null of `S` [RW, Theorem 6.10]. ## References * [LRR25] M. Larsson, A. Ramdas and J. Ruf, *The numeraire e-variable and reverse information projection*, Ann. Statist. 53 (2025), arXiv:2402.18810, Definition 3.1 and Lemma 4.5. * [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in - Statistics 1 (2025), arXiv:2410.23614v6, §6.3.1 and Theorem 6.10. + Statistics 1 (2025), arXiv:2410.23614v6, Fact 3.6, §6.3.1 and Theorem 6.10. -/ public section @@ -60,6 +63,7 @@ namespace ProbabilityTheory variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S T : Set (Measure Ω)} {μ ν Q : Measure Ω} /-- The effective null is monotone in the null. -/ +@[gcongr] theorem effectiveSet_mono (hST : S ⊆ T) : effectiveSet S ⊆ effectiveSet T := fun _ hμ X hX ↦ hμ X (hX.anti_set hST) @@ -118,7 +122,8 @@ theorem mem_effectiveSet_of_tendsto {ι : Type*} {l : Filter ι} [l.NeBot] {μs (hμs : ∀ᶠ i in l, μs i ∈ effectiveSet S) (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : μ ∈ effectiveSet S := fun X hX ↦ - (lintegral_le_liminf_lintegral_of_tendsto_measure hX.measurable h).trans + (lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure hX.measurable + fun s hs ↦ (h s hs).liminf_eq.ge).trans (liminf_le_of_frequently_le (hμs.mono fun _ hi ↦ hi X hX).frequently) /-- A measurable set that is null for every member of `S` is null for every member of the @@ -145,8 +150,8 @@ theorem absolutelyContinuous_of_mem_effectiveSet (hμ : μ ∈ effectiveSet S) 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 -/-- The e-variables for the probability measures of the effective null of `S` are e-variables -for `S`. -/ +/-- An e-variable for `S` is an e-variable for the probability measures of the effective null of +`S`. -/ theorem IsEVar.effectiveSet_inter {X : Ω → ℝ≥0∞} (hX : IsEVar X S) : IsEVar X (effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) := .of_lintegral_le_one (S := effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) (fun _ hμ ↦ hμ.2) @@ -166,10 +171,32 @@ theorem effectiveSet_effectiveSet_inter (hS : ∀ P ∈ S, IsProbabilityMeasure ext μ simp only [mem_effectiveSet_iff, isEVar_effectiveSet_inter_iff hS] +/-- A measure `Q` outside the effective null of a null `S` of finite measures is detected by a +bounded e-variable: some e-variable for `S` bounded by an integer `N ≥ 2` has expectation larger +than `1` under `Q`. It is the truncation `min X N` of an e-variable `X` with expectation larger +than `1` under `Q`, for `N` large enough. -/ +theorem exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet + (hS : ∀ P ∈ S, IsFiniteMeasure P) (hQ : Q ∉ effectiveSet S) : + ∃ Y : Ω → ℝ≥0∞, ∃ N : ℕ, 2 ≤ N ∧ IsEVar Y S ∧ (∀ ω, Y ω ≤ N) ∧ 1 < ∫⁻ ω, Y ω ∂Q := by + obtain ⟨X, hX, hXQ⟩ : ∃ X, IsEVar X S ∧ 1 < ∫⁻ ω, X ω ∂Q := by + simpa [mem_effectiveSet_iff] using hQ + -- By monotone convergence, the truncations `min X N` have expectation larger than `1` under + -- `Q` from some level `N ≥ 2` on. + have hXm := hX.measurable + have h_tendsto : Tendsto (fun N : ℕ ↦ ∫⁻ ω, min (X ω) N ∂Q) atTop (𝓝 (∫⁻ ω, X ω ∂Q)) := by + refine lintegral_tendsto_of_tendsto_of_monotone (fun N ↦ by fun_prop) (.of_forall + fun ω N M hNM ↦ min_le_min_left _ (by exact_mod_cast hNM)) (.of_forall fun ω ↦ ?_) + simpa using (tendsto_const_nhds (x := X ω)).min ENNReal.tendsto_nat_nhds_top + obtain ⟨N, hNQ, hN2⟩ := ((h_tendsto.eventually (lt_mem_nhds hXQ)).and + (eventually_ge_atTop 2)).exists + exact ⟨fun ω ↦ min (X ω) N, N, hN2, hX.mono hS (by fun_prop) fun ω ↦ min_le_left _ _, + fun ω ↦ min_le_right _ _, hNQ⟩ + /-- A measure `Q` is outside the effective null of a null `S` of probability measures exactly when, for some level `α ∈ (0, 1)`, some level-`α` test `φ` for `S` (a measurable function with values in `[0, 1]` and expectation at most `α` under every member of `S`) has expectation larger -than `α` under `Q` [RW, Theorem 6.10]. -/ +than `α` under `Q` [RW, Theorem 6.10]. Both directions pass between a level-`α` test `φ` and the +`[0, α⁻¹]`-valued e-variable `α⁻¹ * φ` [RW, Fact 3.6]. -/ theorem exists_test_iff_notMem_effectiveSet (hS : ∀ P ∈ S, IsProbabilityMeasure P) : (∃ α : ℝ≥0∞, 0 < α ∧ α < 1 ∧ ∃ φ : Ω → ℝ≥0∞, Measurable φ ∧ φ ≤ 1 ∧ (∀ P ∈ S, ∫⁻ ω, φ ω ∂P ≤ α) ∧ α < ∫⁻ ω, φ ω ∂Q) ↔ Q ∉ effectiveSet S := by @@ -185,38 +212,28 @@ theorem exists_test_iff_notMem_effectiveSet (hS : ∀ P ∈ S, IsProbabilityMeas rw [lintegral_const_mul _ hφ, ENNReal.inv_mul_le_iff hα0.ne' (hα1.trans ENNReal.one_lt_top).ne, mul_one] at h exact (h.trans_lt hφQ).false - · -- An e-variable with expectation larger than `1` under `Q`, truncated at a large level `N` - -- and divided by `N`, is a level-`N⁻¹` test with power larger than `N⁻¹` under `Q`. + · -- A bounded e-variable with expectation larger than `1` under `Q`, divided by its bound `N`, + -- is a level-`N⁻¹` test with power larger than `N⁻¹` under `Q`. intro hQ - obtain ⟨X, hX, hXQ⟩ : ∃ X, IsEVar X S ∧ 1 < ∫⁻ ω, X ω ∂Q := by - simpa [mem_effectiveSet_iff] using hQ - -- By monotone convergence, the truncations `min X N` have expectation larger than `1` under - -- `Q` from some level `N ≥ 2` on. - have hXm := hX.measurable - have h_tendsto : Tendsto (fun N : ℕ ↦ ∫⁻ ω, min (X ω) N ∂Q) atTop (𝓝 (∫⁻ ω, X ω ∂Q)) := by - refine lintegral_tendsto_of_tendsto_of_monotone (fun N ↦ by fun_prop) (.of_forall - fun ω N M hNM ↦ min_le_min_left _ (by exact_mod_cast hNM)) (.of_forall fun ω ↦ ?_) - simpa using (tendsto_const_nhds (x := X ω)).min ENNReal.tendsto_nat_nhds_top - obtain ⟨N, hNQ, hN2⟩ := ((h_tendsto.eventually (lt_mem_nhds hXQ)).and - (eventually_ge_atTop 2)).exists + obtain ⟨Y, N, hN2, hY, hYN, hYQ⟩ := exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet + (fun P hP ↦ have := hS P hP; inferInstance) hQ + have hYm := hY.measurable have hN0 : (N : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : N ≠ 0) have hNtop : (N : ℝ≥0∞) ≠ ∞ := ENNReal.natCast_ne_top N refine ⟨(N : ℝ≥0∞)⁻¹, ENNReal.inv_pos.mpr hNtop, ENNReal.inv_lt_one.mpr - (by exact_mod_cast (by omega : 1 < N)), fun ω ↦ (N : ℝ≥0∞)⁻¹ * min (X ω) N, by fun_prop, + (by exact_mod_cast (by omega : 1 < N)), fun ω ↦ (N : ℝ≥0∞)⁻¹ * Y ω, by fun_prop, fun ω ↦ ?_, fun P hP ↦ ?_, ?_⟩ - · calc (N : ℝ≥0∞)⁻¹ * min (X ω) N ≤ (N : ℝ≥0∞)⁻¹ * N := by gcongr; exact min_le_right _ _ + · calc (N : ℝ≥0∞)⁻¹ * Y ω ≤ (N : ℝ≥0∞)⁻¹ * N := by gcongr; exact hYN ω _ = 1 := ENNReal.inv_mul_cancel hN0 hNtop · have := hS P hP - rw [lintegral_const_mul _ (by fun_prop)] - calc (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, min (X ω) N ∂P ≤ (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, X ω ∂P := by - gcongr with ω; exact min_le_left _ _ - _ ≤ (N : ℝ≥0∞)⁻¹ * 1 := by - gcongr; simpa using hX.lintegral_le_measure_univ P hP + rw [lintegral_const_mul _ hYm] + calc (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, Y ω ∂P ≤ (N : ℝ≥0∞)⁻¹ * 1 := by + gcongr; simpa using hY.lintegral_le_measure_univ P hP _ = (N : ℝ≥0∞)⁻¹ := mul_one _ - · rw [lintegral_const_mul _ (by fun_prop)] + · rw [lintegral_const_mul _ hYm] calc (N : ℝ≥0∞)⁻¹ = (N : ℝ≥0∞)⁻¹ * 1 := (mul_one _).symm - _ < (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, min (X ω) N ∂Q := + _ < (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, Y ω ∂Q := ENNReal.mul_lt_mul_right (ENNReal.inv_ne_zero.mpr hNtop) (ENNReal.inv_ne_top.mpr hN0) - hNQ + hYQ end ProbabilityTheory diff --git a/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean b/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean index 10640367..fec78f25 100644 --- a/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean +++ b/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean @@ -6,7 +6,8 @@ Authors: LMLExplore contributors module public import Mathlib.MeasureTheory.Integral.Lebesgue.Add -public import Mathlib.Topology.Instances.ENNReal.Lemmas +public import Mathlib.Order.Filter.ENNReal +public import TauCeti.Topology.Instances.ENNReal /-! # Lebesgue integral of finite sums and lower semicontinuity under setwise convergence @@ -18,9 +19,13 @@ public import Mathlib.Topology.Instances.ENNReal.Lemmas `MeasureTheory.lintegral_finsetSum_indicator_one₀`, its version for null measurable sets. * `MeasureTheory.SimpleFunc.tendsto_lintegral_of_tendsto_measure`: the integral of a simple function with finite values is continuous for the setwise convergence of measures. -* `MeasureTheory.lintegral_le_liminf_lintegral_of_tendsto_measure`: the Lebesgue integral of a - measurable function is lower semicontinuous for the setwise convergence of measures, along any - filter. This is the setwise counterpart of the portmanteau inequality +* `MeasureTheory.SimpleFunc.lintegral_le_liminf_lintegral`: the integral of a simple function with + finite values is lower semicontinuous when the measures of measurable sets are. +* `MeasureTheory.lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure`: + if `μ s ≤ liminf (μs i s)` along a filter for every measurable set `s`, then + `∫⁻ f ∂μ ≤ liminf (∫⁻ f ∂μs i)` for every measurable `f`; in particular the Lebesgue integral + is lower semicontinuous for the setwise convergence of measures. This is the measurable-set + counterpart of the portmanteau inequality `MeasureTheory.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure`. -/ @@ -57,27 +62,39 @@ of measures. -/ theorem SimpleFunc.tendsto_lintegral_of_tendsto_measure (f : SimpleFunc α ℝ≥0∞) (hf : ∀ y ∈ f.range, y ≠ ∞) (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : - Tendsto (fun i ↦ f.lintegral (μs i)) l (𝓝 (f.lintegral μ)) := - tendsto_finsetSum _ fun y hy ↦ + Tendsto (fun i ↦ f.lintegral (μs i)) l (𝓝 (f.lintegral μ)) := by + unfold SimpleFunc.lintegral + exact tendsto_finsetSum _ fun y hy ↦ ENNReal.Tendsto.const_mul (h _ (f.measurableSet_preimage _)) (.inr (hf y hy)) -/-- **Lower semicontinuity of the Lebesgue integral under setwise convergence.** If `μs i s` -tends to `μ s` along a filter for every measurable set `s`, then -`∫⁻ f ∂μ ≤ liminf (∫⁻ f ∂μs i)` for every measurable `f`. The filter is arbitrary, so this holds -for nets of measures and not only for sequences. -/ -theorem lintegral_le_liminf_lintegral_of_tendsto_measure [l.NeBot] {f : α → ℝ≥0∞} - (hf : Measurable f) (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : +/-- The integral of a simple function with finite values is lower semicontinuous along a filter +when the measures of measurable sets are: if `μ s ≤ liminf (μs i s)` for every measurable set +`s`, then `f.lintegral μ ≤ liminf (f.lintegral (μs i))`. -/ +theorem SimpleFunc.lintegral_le_liminf_lintegral [l.NeBot] (f : SimpleFunc α ℝ≥0∞) + (hf : ∀ y ∈ f.range, y ≠ ∞) (h : ∀ s, MeasurableSet s → μ s ≤ liminf (fun i ↦ μs i s) l) : + f.lintegral μ ≤ liminf (fun i ↦ f.lintegral (μs i)) l := by + unfold SimpleFunc.lintegral + refine (Finset.sum_le_sum fun y hy ↦ ?_).trans (ENNReal.sum_liminf_le_liminf_sum _ _) + rw [ENNReal.liminf_const_mul_of_ne_top (hf y hy)] + gcongr + exact h _ (f.measurableSet_preimage _) + +/-- **Lower semicontinuity of the Lebesgue integral.** If `μ s ≤ liminf (μs i s)` along a filter +for every measurable set `s`, then `∫⁻ f ∂μ ≤ liminf (∫⁻ f ∂μs i)` for every measurable `f`. This +covers the setwise convergence of measures along any filter, so it holds for nets of measures and +not only for sequences. -/ +theorem lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure [l.NeBot] + {f : α → ℝ≥0∞} (hf : Measurable f) + (h : ∀ s, MeasurableSet s → μ s ≤ liminf (fun i ↦ μs i s) l) : ∫⁻ x, f x ∂μ ≤ liminf (fun i ↦ ∫⁻ x, f x ∂μs i) l := by rw [lintegral_eq_iSup_eapprox_lintegral hf] refine iSup_le fun n ↦ ?_ - have h_tendsto := (SimpleFunc.eapprox f n).tendsto_lintegral_of_tendsto_measure - (fun y hy ↦ by - obtain ⟨x, rfl⟩ := SimpleFunc.mem_range.mp hy - exact (SimpleFunc.eapprox_lt_top f n x).ne) h - rw [← h_tendsto.liminf_eq] - refine liminf_le_liminf (.of_forall fun i ↦ ?_) - rw [lintegral_eq_iSup_eapprox_lintegral hf] - exact le_iSup (fun n ↦ (SimpleFunc.eapprox f n).lintegral (μs i)) n + refine ((SimpleFunc.eapprox f n).lintegral_le_liminf_lintegral (fun y hy ↦ ?_) h).trans + (liminf_le_liminf (.of_forall fun i ↦ ?_)) + · obtain ⟨x, rfl⟩ := SimpleFunc.mem_range.mp hy + exact (SimpleFunc.eapprox_lt_top f n x).ne + · rw [lintegral_eq_iSup_eapprox_lintegral hf] + exact le_iSup (fun n ↦ (SimpleFunc.eapprox f n).lintegral (μs i)) n end Setwise From ce4c807d16dbd47d33b26e10e7ec8cc55eeb56fe Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 19:39:29 +0100 Subject: [PATCH 3/5] fix: adopt the roadmap name for the test characterization of the effective null Rename `exists_test_iff_notMem_effectiveSet` to the roadmap's suggested `exists_powered_test_iff`, with its signature. Generalise the closure of the effective null to the liminf hypothesis (`mem_effectiveSet_of_measure_le_liminf`), keeping setwise convergence as a corollary. Make the module docstring state the hypotheses of its main statements, and move proof narration out of docstrings. Co-Authored-By: Claude Code --- LMLExplore/EValues/EffectiveSet.lean | 50 +++++++++++++++++----------- 1 file changed, 31 insertions(+), 19 deletions(-) diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean index 61949411..5292e643 100644 --- a/LMLExplore/EValues/EffectiveSet.lean +++ b/LMLExplore/EValues/EffectiveSet.lean @@ -15,7 +15,8 @@ The effective null of a null hypothesis `S : Set (Measure Ω)` is Statlib's `eff measures `μ` under which every e-variable `X` for `S` has `∫⁻ X ∂μ ≤ 1`. It is the set over which Statlib's duality `maxUtility_eq_iInf_klIntegral_effectiveSet` minimizes, and it describes the alternatives that a null can be tested against: e-variables cannot distinguish `S` from its -effective null, and every probability measure outside of it is detected by a level-`α` test. +effective null, and, when `S` consists of probability measures, every measure outside its +effective null is detected by a level-`α` test. This file proves the structural properties of the effective null on any measurable space, with no dominating measure and no convexity. Unless stated otherwise below, the results hold for any set of @@ -26,13 +27,16 @@ measures `S`. * `ProbabilityTheory.subset_effectiveSet_iff`: `S ⊆ effectiveSet S` exactly when every member of `S` has mass at most `1`. * `ProbabilityTheory.comp_mem_effectiveSet`: the effective null contains every mixture `κ ∘ₘ π` of - members of the effective null over a measure `π` of mass at most `1`, in particular every mixture - of members of `S` over a probability measure. + members of the effective null over a measure `π` of mass at most `1`, in particular, for a null + of measures of mass at most `1`, every mixture of members of `S` over a probability measure. * `ProbabilityTheory.convex_effectiveSet`, `ProbabilityTheory.convexHull_subset_effectiveSet`: the - effective null is convex, and contains the convex hull of `S`. + effective null is convex, and, for a null of measures of mass at most `1`, contains the convex + hull of `S`. * `ProbabilityTheory.isLowerSet_effectiveSet`: the effective null is solid. -* `ProbabilityTheory.mem_effectiveSet_of_tendsto`: the effective null is closed under setwise - convergence, along any filter. +* `ProbabilityTheory.mem_effectiveSet_of_measure_le_liminf`, + `ProbabilityTheory.mem_effectiveSet_of_tendsto`: the effective null is closed under setwise + convergence, along any filter, and more generally contains every measure `μ` with + `μ s ≤ liminf (μs · s)` for every measurable `s`, for a net `μs` eventually in it. * `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. @@ -40,7 +44,7 @@ measures `S`. absolutely continuous with respect to `μ`, so is every member of the effective null. * `ProbabilityTheory.exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet`: for a null `S` of finite measures, a measure outside the effective null of `S` is detected by a bounded e-variable. -* `ProbabilityTheory.exists_test_iff_notMem_effectiveSet`: for a null `S` of probability measures, +* `ProbabilityTheory.exists_powered_test_iff`: for a null `S` of probability measures, a measure `Q` admits, for some `α ∈ (0, 1)`, a level-`α` test for `S` with power larger than `α` under `Q` exactly when `Q` is not in the effective null of `S` [RW, Theorem 6.10]. @@ -114,6 +118,15 @@ theorem isLowerSet_effectiveSet : IsLowerSet (effectiveSet S) := theorem mem_effectiveSet_of_le (hν : ν ∈ effectiveSet S) (hμν : μ ≤ ν) : μ ∈ effectiveSet S := isLowerSet_effectiveSet hμν hν +/-- If `μs i` is eventually in the effective null along a filter, and `μ s` is at most the limit +inferior of `μs i s` for every measurable set `s`, then `μ` is in the effective null. -/ +theorem mem_effectiveSet_of_measure_le_liminf {ι : Type*} {l : Filter ι} [l.NeBot] + {μs : ι → Measure Ω} (hμs : ∀ᶠ i in l, μs i ∈ effectiveSet S) + (h : ∀ s, MeasurableSet s → μ s ≤ liminf (fun i ↦ μs i s) l) : + μ ∈ effectiveSet S := fun X hX ↦ + (lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure hX.measurable + h).trans (liminf_le_of_frequently_le (hμs.mono fun _ hi ↦ hi X hX).frequently) + /-- The effective null is closed under setwise convergence: if `μs i s` tends to `μ s` along a filter for every measurable set `s`, and `μs i` is eventually in the effective null, then so is `μ`. The filter is arbitrary, so that the effective null is closed for the topology of setwise @@ -121,10 +134,8 @@ convergence and not only sequentially closed. -/ theorem mem_effectiveSet_of_tendsto {ι : Type*} {l : Filter ι} [l.NeBot] {μs : ι → Measure Ω} (hμs : ∀ᶠ i in l, μs i ∈ effectiveSet S) (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : - μ ∈ effectiveSet S := fun X hX ↦ - (lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure hX.measurable - fun s hs ↦ (h s hs).liminf_eq.ge).trans - (liminf_le_of_frequently_le (hμs.mono fun _ hi ↦ hi X hX).frequently) + μ ∈ effectiveSet S := + mem_effectiveSet_of_measure_le_liminf hμs fun s hs ↦ (h s hs).liminf_eq.ge /-- A measurable set that is null for every member of `S` is null for every member of the effective null of `S`. -/ @@ -173,15 +184,15 @@ theorem effectiveSet_effectiveSet_inter (hS : ∀ P ∈ S, IsProbabilityMeasure /-- A measure `Q` outside the effective null of a null `S` of finite measures is detected by a bounded e-variable: some e-variable for `S` bounded by an integer `N ≥ 2` has expectation larger -than `1` under `Q`. It is the truncation `min X N` of an e-variable `X` with expectation larger -than `1` under `Q`, for `N` large enough. -/ +than `1` under `Q`. -/ theorem exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet (hS : ∀ P ∈ S, IsFiniteMeasure P) (hQ : Q ∉ effectiveSet S) : ∃ Y : Ω → ℝ≥0∞, ∃ N : ℕ, 2 ≤ N ∧ IsEVar Y S ∧ (∀ ω, Y ω ≤ N) ∧ 1 < ∫⁻ ω, Y ω ∂Q := by obtain ⟨X, hX, hXQ⟩ : ∃ X, IsEVar X S ∧ 1 < ∫⁻ ω, X ω ∂Q := by simpa [mem_effectiveSet_iff] using hQ - -- By monotone convergence, the truncations `min X N` have expectation larger than `1` under - -- `Q` from some level `N ≥ 2` on. + -- `Y` is the truncation `min X N` of an e-variable `X` with expectation larger than `1` under + -- `Q`, for `N` large enough. By monotone convergence, the truncations `min X N` have + -- expectation larger than `1` under `Q` from some level `N ≥ 2` on. have hXm := hX.measurable have h_tendsto : Tendsto (fun N : ℕ ↦ ∫⁻ ω, min (X ω) N ∂Q) atTop (𝓝 (∫⁻ ω, X ω ∂Q)) := by refine lintegral_tendsto_of_tendsto_of_monotone (fun N ↦ by fun_prop) (.of_forall @@ -195,11 +206,12 @@ theorem exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet /-- A measure `Q` is outside the effective null of a null `S` of probability measures exactly when, for some level `α ∈ (0, 1)`, some level-`α` test `φ` for `S` (a measurable function with values in `[0, 1]` and expectation at most `α` under every member of `S`) has expectation larger -than `α` under `Q` [RW, Theorem 6.10]. Both directions pass between a level-`α` test `φ` and the -`[0, α⁻¹]`-valued e-variable `α⁻¹ * φ` [RW, Fact 3.6]. -/ -theorem exists_test_iff_notMem_effectiveSet (hS : ∀ P ∈ S, IsProbabilityMeasure P) : - (∃ α : ℝ≥0∞, 0 < α ∧ α < 1 ∧ ∃ φ : Ω → ℝ≥0∞, Measurable φ ∧ φ ≤ 1 ∧ +than `α` under `Q` [RW, Theorem 6.10]. -/ +theorem exists_powered_test_iff (hS : ∀ P ∈ S, IsProbabilityMeasure P) (Q : Measure Ω) : + (∃ α : ℝ≥0∞, 0 < α ∧ α < 1 ∧ ∃ φ : Ω → ℝ≥0∞, Measurable φ ∧ (∀ ω, φ ω ≤ 1) ∧ (∀ P ∈ S, ∫⁻ ω, φ ω ∂P ≤ α) ∧ α < ∫⁻ ω, φ ω ∂Q) ↔ Q ∉ effectiveSet S := by + -- Both directions pass between a level-`α` test `φ` and the `[0, α⁻¹]`-valued e-variable + -- `α⁻¹ * φ` [RW, Fact 3.6]. constructor · rintro ⟨α, hα0, hα1, φ, hφ, -, hφS, hφQ⟩ hQ -- `α⁻¹ * φ` is an e-variable for `S`, so its expectation under `Q` is at most `1`. From 5fdb30e2574ea9ceda8b2c5e52b3b85da551ba97 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 20:02:26 +0100 Subject: [PATCH 4/5] fix: drop the finiteness hypothesis from the bounded e-variable detection lemma MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet` no longer assumes that the members of `S` are finite: for `N ≥ 1` the truncation `min X N - 1` has the same negative part as `X - 1`, so it is an e-variable for any null. Co-Authored-By: Claude Code --- LMLExplore/EValues/EffectiveSet.lean | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean index 5292e643..ad95f8b5 100644 --- a/LMLExplore/EValues/EffectiveSet.lean +++ b/LMLExplore/EValues/EffectiveSet.lean @@ -42,8 +42,8 @@ measures `S`. (`ProbabilityTheory.effectiveSet_effectiveSet_inter`) the same effective null. * `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`: for a null `S` of - finite measures, a measure outside the effective null of `S` is detected by a bounded e-variable. +* `ProbabilityTheory.exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet`: a measure outside the + effective null of `S` is detected by a bounded e-variable. * `ProbabilityTheory.exists_powered_test_iff`: for a null `S` of probability measures, a measure `Q` admits, for some `α ∈ (0, 1)`, a level-`α` test for `S` with power larger than `α` under `Q` exactly when `Q` is not in the effective null of `S` [RW, Theorem 6.10]. @@ -182,11 +182,10 @@ theorem effectiveSet_effectiveSet_inter (hS : ∀ P ∈ S, IsProbabilityMeasure ext μ simp only [mem_effectiveSet_iff, isEVar_effectiveSet_inter_iff hS] -/-- A measure `Q` outside the effective null of a null `S` of finite measures is detected by a +/-- A measure `Q` outside the effective null of a null `S` is detected by a bounded e-variable: some e-variable for `S` bounded by an integer `N ≥ 2` has expectation larger than `1` under `Q`. -/ -theorem exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet - (hS : ∀ P ∈ S, IsFiniteMeasure P) (hQ : Q ∉ effectiveSet S) : +theorem exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet (hQ : Q ∉ effectiveSet S) : ∃ Y : Ω → ℝ≥0∞, ∃ N : ℕ, 2 ≤ N ∧ IsEVar Y S ∧ (∀ ω, Y ω ≤ N) ∧ 1 < ∫⁻ ω, Y ω ∂Q := by obtain ⟨X, hX, hXQ⟩ : ∃ X, IsEVar X S ∧ 1 < ∫⁻ ω, X ω ∂Q := by simpa [mem_effectiveSet_iff] using hQ @@ -200,8 +199,20 @@ theorem exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet simpa using (tendsto_const_nhds (x := X ω)).min ENNReal.tendsto_nat_nhds_top obtain ⟨N, hNQ, hN2⟩ := ((h_tendsto.eventually (lt_mem_nhds hXQ)).and (eventually_ge_atTop 2)).exists - exact ⟨fun ω ↦ min (X ω) N, N, hN2, hX.mono hS (by fun_prop) fun ω ↦ min_le_left _ _, + -- Since `N ≥ 1`, the truncation `min X N - 1` has the same negative part as `X - 1`, and a + -- smaller positive part, so it is an e-variable whatever the members of `S`. + refine ⟨fun ω ↦ min (X ω) N, N, hN2, ⟨by fun_prop, fun P hP ↦ ?_, fun P hP ↦ ?_⟩, fun ω ↦ min_le_right _ _, hNQ⟩ + · refine eintegral_ne_bot_iff_lintegral_ne_top.mpr <| ne_top_of_le_ne_top + (eintegral_ne_bot_iff_lintegral_ne_top.mp (hX.eintegral_ne_bot P hP)) + (lintegral_mono fun ω ↦ ?_) + rcases le_total (X ω) N with h | h + · rw [min_eq_left h] + · rw [min_eq_right h, EReal.toENNReal_of_nonpos (EReal.neg_le_zero.mpr <| + (EReal.sub_nonneg (by simp) (by simp)).mpr (by exact_mod_cast (by omega : 1 ≤ N)))] + exact bot_le + · exact (eintegral_mono fun ω ↦ EReal.sub_le_sub (by exact_mod_cast min_le_left _ _) le_rfl).trans + (hX.eintegral_nonpos P hP) /-- A measure `Q` is outside the effective null of a null `S` of probability measures exactly when, for some level `α ∈ (0, 1)`, some level-`α` test `φ` for `S` (a measurable function with @@ -227,8 +238,7 @@ theorem exists_powered_test_iff (hS : ∀ P ∈ S, IsProbabilityMeasure P) (Q : · -- A bounded e-variable with expectation larger than `1` under `Q`, divided by its bound `N`, -- is a level-`N⁻¹` test with power larger than `N⁻¹` under `Q`. intro hQ - obtain ⟨Y, N, hN2, hY, hYN, hYQ⟩ := exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet - (fun P hP ↦ have := hS P hP; inferInstance) hQ + obtain ⟨Y, N, hN2, hY, hYN, hYQ⟩ := exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet hQ have hYm := hY.measurable have hN0 : (N : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : N ≠ 0) have hNtop : (N : ℝ≥0∞) ≠ ∞ := ENNReal.natCast_ne_top N From 2ff1ca4d184ebe63fbbf6de586e3ebe72460dcf6 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 20:34:15 +0100 Subject: [PATCH 5/5] refactor: factor out the truncation of an e-variable as IsEVar.min_const MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The proof that min X N is an e-variable for S when 1 ≤ N was inlined in exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet. It is now the lemma IsEVar.min_const, for any level c ≥ 1 in ℝ≥0∞, proved through the negative part identity (1 - y) rather than a chain of EReal rewrites. Co-Authored-By: Claude Code --- LMLExplore/EValues/EffectiveSet.lean | 33 +++++++++++++++++----------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean index ad95f8b5..039a2cbb 100644 --- a/LMLExplore/EValues/EffectiveSet.lean +++ b/LMLExplore/EValues/EffectiveSet.lean @@ -182,6 +182,25 @@ theorem effectiveSet_effectiveSet_inter (hS : ∀ P ∈ S, IsProbabilityMeasure ext μ simp only [mem_effectiveSet_iff, isEVar_effectiveSet_inter_iff hS] +/-- The truncation `min X c` of an e-variable `X` for `S` at a level `c ≥ 1` is an e-variable for +`S`. -/ +theorem IsEVar.min_const {X : Ω → ℝ≥0∞} (hX : IsEVar X S) {c : ℝ≥0∞} (hc : 1 ≤ c) : + IsEVar (fun ω ↦ min (X ω) c) S where + measurable := hX.measurable.min measurable_const + eintegral_ne_bot P hP := by + -- The negative part of `y - 1` is `1 - y`, and `1 - min y c = 1 - y` since `1 ≤ c`, so + -- `min X c - 1` has the same negative part as `X - 1`. + have h_neg (y : ℝ≥0∞) : (-((y : EReal) - 1)).toENNReal = 1 - y := by + simpa [EReal.toENNReal_sub, EReal.coe_ennreal_nonneg] using + congrArg EReal.toENNReal (EReal.neg_coe_ennreal_sub (u := y) (.inr ENNReal.one_ne_top)) + have h_min (y : ℝ≥0∞) : 1 - min y c = 1 - y := by + rcases le_total y c with h | h + · simp [h] + · simp [h, tsub_eq_zero_of_le hc, tsub_eq_zero_of_le (hc.trans h)] + simpa [eintegral_ne_bot_iff_lintegral_ne_top, h_neg, h_min] using hX.eintegral_ne_bot P hP + eintegral_nonpos P hP := (eintegral_mono fun ω ↦ + EReal.sub_le_sub (mod_cast min_le_left _ _) le_rfl).trans (hX.eintegral_nonpos P hP) + /-- A measure `Q` outside the effective null of a null `S` is detected by a bounded e-variable: some e-variable for `S` bounded by an integer `N ≥ 2` has expectation larger than `1` under `Q`. -/ @@ -199,20 +218,8 @@ theorem exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet (hQ : Q ∉ effecti simpa using (tendsto_const_nhds (x := X ω)).min ENNReal.tendsto_nat_nhds_top obtain ⟨N, hNQ, hN2⟩ := ((h_tendsto.eventually (lt_mem_nhds hXQ)).and (eventually_ge_atTop 2)).exists - -- Since `N ≥ 1`, the truncation `min X N - 1` has the same negative part as `X - 1`, and a - -- smaller positive part, so it is an e-variable whatever the members of `S`. - refine ⟨fun ω ↦ min (X ω) N, N, hN2, ⟨by fun_prop, fun P hP ↦ ?_, fun P hP ↦ ?_⟩, + exact ⟨fun ω ↦ min (X ω) N, N, hN2, hX.min_const (by exact_mod_cast (by omega : 1 ≤ N)), fun ω ↦ min_le_right _ _, hNQ⟩ - · refine eintegral_ne_bot_iff_lintegral_ne_top.mpr <| ne_top_of_le_ne_top - (eintegral_ne_bot_iff_lintegral_ne_top.mp (hX.eintegral_ne_bot P hP)) - (lintegral_mono fun ω ↦ ?_) - rcases le_total (X ω) N with h | h - · rw [min_eq_left h] - · rw [min_eq_right h, EReal.toENNReal_of_nonpos (EReal.neg_le_zero.mpr <| - (EReal.sub_nonneg (by simp) (by simp)).mpr (by exact_mod_cast (by omega : 1 ≤ N)))] - exact bot_le - · exact (eintegral_mono fun ω ↦ EReal.sub_le_sub (by exact_mod_cast min_le_left _ _) le_rfl).trans - (hX.eintegral_nonpos P hP) /-- A measure `Q` is outside the effective null of a null `S` of probability measures exactly when, for some level `α ∈ (0, 1)`, some level-`α` test `φ` for `S` (a measurable function with