feat: two mixture nulls separating one observation, the bipolar rate and the relative entropy

LMLExplore/EValues/BipolarRate/FiniteSupport.lean

@@ -0,0 +1,238 @@
+/-
+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.BipolarRate.Basic
+import LMLExplore.EValues.EffectiveSet
+import LMLExplore.InformationTheory.KullbackLeibler.Mixture
+import LMLExplore.MeasureTheory.Constructions.Pi
+import Mathlib.Analysis.SpecialFunctions.Choose
+import Statlib.ForMathlib.MeasureTheory.Constructions.Pi
+
+/-!
+# A null against which no sample size carries evidence, at positive relative entropy
+
+Let `Q` be a probability measure on a measurable space with measurable singletons, and `ε ≤ 1`.
+Against the i.i.d. null generated by the mixtures `(1 - ε) F + ε Q`, with `F` a probability
+measure carried by a finite set, no `n`-sample e-variable has a positive expected logarithm under
+`Q ^ n`, for any `n`: `maxLogGrowth Q S n = 0`, so the bipolar rate is `0`. If moreover `Q` has no
+atoms, every such `F` is singular to `Q`, and the relative entropy from `Q` to each member of the
+null is `log (1 / ε)`. The bipolar rate is at most the smallest relative entropy to the null
+(`ProbabilityTheory.bipolarRate_le_iInf_klDiv`), and the inequality can be strict
+[RR26, Proposition 5.4]; here the bipolar rate is `0` while the smallest relative entropy is
+positive for `ε < 1`.
+
+For Lebesgue measure on the circle, this null has the same smallest relative entropy as the null
+of `LMLExplore.EValues.BipolarRate.Circle`, which it contains, but bipolar rate `0` instead of
+`log (1 / ε)`.
+
+## Main statements
+
+* `ProbabilityTheory.maxLogGrowth_finitelySupported_mixtures_eq_zero`: for every `n`, the maximal
+  expected logarithm of an `n`-sample e-variable is `0`.
+* `ProbabilityTheory.bipolarRate_finitelySupported_mixtures_eq_zero`: the bipolar rate is `0`.
+* `ProbabilityTheory.iInf_klDiv_finitelySupported_mixtures`: for `Q` without atoms, the smallest
+  relative entropy from `Q` to the null is `log (1 / ε)`.
+
+## Implementation notes
+
+Write `G z = (1 - ε) δ_z + ε Q`, so that `Q` is the average of the `G z` under `Q`. For
+`y : Fin m → 𝓧`, the uniform mixture of the `G (y k)` is the member `(1 - ε) F_y + ε Q` of the
+null, with `F_y` uniform on the points `y k`. Its `n`-fold product expands along the maps
+`σ : Fin n → Fin m` (`MeasureTheory.Measure.pi_sum_smul`), and for an injective `σ` the average,
+over `m` independent points `y` of law `Q`, of the product of the `G (y (σ i))` is `Q ^ n`
+(Statlib's `MeasureTheory.Measure.pi_map_comp_of_injective` and
+`MeasureTheory.Measure.pi_bind_pi`). So `Q ^ n`, scaled by the fraction
+`m (m - 1) ⋯ (m - n + 1) / m ^ n` of the injective maps, is below an average of members of the
+`n`-sample null, and that fraction tends to `1` as `m → ∞`: `Q ^ n` is in the effective null of
+the `n`-sample null (`ProbabilityTheory.maxUtility_eq_zero_of_mem_effectiveSet`).
+
+The instance is [EVR26, Note 19]. Its statements and proofs are adapted from
+`EValuesResearch/Results/RateVersusKL.lean` (commit `dd4072f`) in the paper project
+`RemyDegenne/evalues_research` (same author), which states them on the circle only, with `F`
+carried by a `Finset`.
+
+## References
+
+* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, notes 01 to 34 and
+  the Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026.
+* [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1.
+-/
+
+public section
+
+open MeasureTheory InformationTheory Filter
+open scoped ENNReal Topology
+
+namespace ProbabilityTheory
+
+variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {Q : Measure 𝓧} {ε : ℝ≥0∞}
+
+/-- The law `(1 - ε) δ_z + ε Q`: keep the point `z` with probability `1 - ε`, and resample it
+from `Q` otherwise. -/
+private noncomputable def resample (Q : Measure 𝓧) (ε : ℝ≥0∞) (z : 𝓧) : Measure 𝓧 :=
+  (1 - ε) • Measure.dirac z + ε • Q
+
+/-- For `ε ≤ 1`, the law `(1 - ε) δ_z + ε Q` is a probability measure. -/
+private lemma isProbabilityMeasure_resample [IsProbabilityMeasure Q] (hε : ε ≤ 1) (z : 𝓧) :
+    IsProbabilityMeasure (resample Q ε z) :=
+  ⟨by simp [resample, tsub_add_cancel_of_le hε]⟩
+
+/-- The law `(1 - ε) δ_z + ε Q` depends measurably on `z`. -/
+private lemma measurable_resample (Q : Measure 𝓧) (ε : ℝ≥0∞) : Measurable (resample Q ε) := by
+  refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_
+  simp only [resample, add_apply, smul_apply, Measure.dirac_apply' _ hs, smul_eq_mul]
+  exact ((measurable_one.indicator hs).const_mul _).add measurable_const
+
+/-- `Q` is the average of the laws `(1 - ε) δ_z + ε Q` under `Q`. -/
+private lemma bind_resample [IsProbabilityMeasure Q] (hε : ε ≤ 1) :
+    Q.bind (resample Q ε) = Q := by
+  ext s hs
+  rw [Measure.bind_apply hs (measurable_resample Q ε).aemeasurable]
+  simp only [resample, add_apply, smul_apply, Measure.dirac_apply' _ hs, smul_eq_mul]
+  simp [lintegral_add_right _ measurable_const, lintegral_const_mul _ (measurable_one.indicator hs),
+    lintegral_indicator_one hs, ← add_mul, tsub_add_cancel_of_le hε]
+
+/-- Reading `m` independent points of law `Q` along an injective `σ : Fin n → Fin m`, and
+resampling each of them from `Q` with probability `ε`, gives `n` independent points of law
+`Q`. -/
+private lemma lintegral_lintegral_pi_resample [IsProbabilityMeasure Q] (hε : ε ≤ 1) {n m : ℕ}
+    {σ : Fin n → Fin m} (hσ : σ.Injective) {E : (Fin n → 𝓧) → ℝ≥0∞} (hE : Measurable E) :
+    ∫⁻ y, ∫⁻ x, E x ∂(Measure.pi fun i ↦ resample Q ε (y (σ i))) ∂(Measure.pi fun _ ↦ Q) =
+      ∫⁻ x, E x ∂(Measure.pi fun _ ↦ Q) := by
+  have := isProbabilityMeasure_resample (Q := Q) hε
+  have : SigmaFinite (Q.bind (resample Q ε)) := by rw [bind_resample hε]; infer_instance
+  have hG := Measure.measurable_pi_comp (G := fun _ : Fin n ↦ resample Q ε)
+    fun _ ↦ measurable_resample Q ε
+  set F : (Fin n → 𝓧) → ℝ≥0∞ := fun x ↦ ∫⁻ x', E x' ∂(Measure.pi fun i ↦ resample Q ε (x i))
+  have hF : Measurable F := (Measure.measurable_lintegral hE).comp hG
+  calc ∫⁻ y, ∫⁻ x, E x ∂(Measure.pi fun i ↦ resample Q ε (y (σ i))) ∂(Measure.pi fun _ ↦ Q)
+  _ = ∫⁻ x, F x ∂((Measure.pi fun _ ↦ Q).map fun y i ↦ y (σ i)) :=
+    (lintegral_map hF (by fun_prop)).symm
+  _ = ∫⁻ x, F x ∂(Measure.pi fun _ ↦ Q) := by rw [Measure.pi_map_comp_of_injective _ hσ]
+  _ = ∫⁻ x, E x ∂((Measure.pi fun _ ↦ Q).bind fun x ↦ Measure.pi fun i ↦ resample Q ε (x i)) :=
+    (Measure.lintegral_bind hG.aemeasurable hE.aemeasurable).symm
+  _ = ∫⁻ x, E x ∂(Measure.pi fun _ ↦ Q) := by
+    rw [Measure.pi_bind_pi fun _ ↦ measurable_resample Q ε, bind_resample hε]
+
+/-- The averaging bound: if the null `S` contains the uniform mixtures of `m` laws
+`(1 - ε) δ_z + ε Q`, an `n`-sample e-variable for `S` has expectation under `Q ^ n` at most
+`m ^ n / (m (m - 1) ⋯ (m - n + 1))`. -/
+private lemma descFactorial_mul_lintegral_le [IsProbabilityMeasure Q] (hε : ε ≤ 1)
+    {S : Set (Measure 𝓧)} {n m : ℕ} (hm : m ≠ 0)
+    (hS : ∀ y : Fin m → 𝓧, ∑ k, (m : ℝ≥0∞)⁻¹ • resample Q ε (y k) ∈ S)
+    {E : (Fin n → 𝓧) → ℝ≥0∞} (hE : IsEVar E ((fun P ↦ Measure.pi fun _ : Fin n ↦ P) '' S)) :
+    (m.descFactorial n : ℝ≥0∞) * (m : ℝ≥0∞)⁻¹ ^ n * ∫⁻ x, E x ∂(Measure.pi fun _ ↦ Q) ≤ 1 := by
+  classical
+  have := isProbabilityMeasure_resample (Q := Q) hε
+  have hm0 : (m : ℝ≥0∞) ≠ 0 := Nat.cast_ne_zero.2 hm
+  set c := (m : ℝ≥0∞)⁻¹ ^ n
+  set I : (Fin n → Fin m) → (Fin m → 𝓧) → ℝ≥0∞ :=
+    fun σ y ↦ ∫⁻ x, E x ∂(Measure.pi fun i ↦ resample Q ε (y (σ i)))
+  have hI (σ : Fin n → Fin m) : Measurable (I σ) :=
+    (Measure.measurable_lintegral hE.measurable).comp ((Measure.measurable_pi_comp
+      (G := fun _ : Fin n ↦ resample Q ε) fun _ ↦ measurable_resample Q ε).comp (by fun_prop))
+  have hP (y : Fin m → 𝓧) : IsProbabilityMeasure (∑ k, (m : ℝ≥0∞)⁻¹ • resample Q ε (y k)) :=
+    ⟨by simp [ENNReal.mul_inv_cancel hm0 (ENNReal.natCast_ne_top m)]⟩
+  -- the `n`-fold product of a uniform mixture of `m` laws expands along the maps `Fin n → Fin m`
+  have hexp (y : Fin m → 𝓧) :
+      ∫⁻ x, E x ∂(Measure.pi fun _ : Fin n ↦ ∑ k, (m : ℝ≥0∞)⁻¹ • resample Q ε (y k)) =
+        ∑ σ, c * I σ y := by
+    have := hP y
+    rw [Measure.pi_sum_smul (fun _ _ ↦ (m : ℝ≥0∞)⁻¹) (fun _ k ↦ resample Q ε (y k)),
+      lintegral_finsetSum_measure]
+    simp [I, c, lintegral_smul_measure]
+  -- the injective maps contribute `Q ^ n` each
+  calc (m.descFactorial n : ℝ≥0∞) * c * ∫⁻ x, E x ∂(Measure.pi fun _ ↦ Q)
+  _ = ∑ e : Fin n ↪ Fin m, c * ∫⁻ y, I e y ∂(Measure.pi fun _ ↦ Q) := by
+    have h (e : Fin n ↪ Fin m) :
+        ∫⁻ y, I e y ∂(Measure.pi fun _ ↦ Q) = ∫⁻ x, E x ∂(Measure.pi fun _ ↦ Q) :=
+      lintegral_lintegral_pi_resample hε e.injective hE.measurable
+    simp_rw [h, Finset.sum_const, Finset.card_univ, Fintype.card_embedding_eq, Fintype.card_fin,
+      nsmul_eq_mul, mul_assoc]
+  _ ≤ ∑ σ, c * ∫⁻ y, I σ y ∂(Measure.pi fun _ ↦ Q) :=
+    (Finset.sum_map Finset.univ ⟨_, DFunLike.coe_injective⟩
+      fun σ ↦ c * ∫⁻ y, I σ y ∂(Measure.pi fun _ ↦ Q)).symm.trans_le
+      (Finset.sum_le_sum_of_subset (Finset.subset_univ _))
+  _ = ∫⁻ y, ∫⁻ x, E x ∂(Measure.pi fun _ : Fin n ↦ ∑ k, (m : ℝ≥0∞)⁻¹ • resample Q ε (y k))
+      ∂(Measure.pi fun _ ↦ Q) := by
+    rw [lintegral_congr hexp, lintegral_finsetSum _ fun σ _ ↦ (hI σ).const_mul c]
+    exact Finset.sum_congr rfl fun σ _ ↦ (lintegral_const_mul c (hI σ)).symm
+  _ ≤ ∫⁻ _, 1 ∂(Measure.pi fun _ : Fin m ↦ Q) := by
+    refine lintegral_mono fun y ↦ ?_
+    have := hP y
+    exact (hE.lintegral_le_measure_univ _ ⟨_, hS y, rfl⟩).trans_eq measure_univ
+  _ = 1 := by simp
+
+variable [MeasurableSingletonClass 𝓧]
+
+/-- The uniform mixture of the laws `(1 - ε) δ_{y k} + ε Q` is `(1 - ε) F + ε Q` with `F` the
+uniform law on the points `y k`, a probability measure carried by a finite set. -/
+private lemma sum_resample_mem {m : ℕ} (hm : m ≠ 0) (y : Fin m → 𝓧) :
+    ∑ k, (m : ℝ≥0∞)⁻¹ • resample Q ε (y k) ∈ {(1 - ε) • F + ε • Q | (F : Measure 𝓧)
+      (_ : IsProbabilityMeasure F) (_ : ∃ s : Set 𝓧, s.Finite ∧ F sᶜ = 0)} := by
+  have hm0 : (m : ℝ≥0∞) ≠ 0 := Nat.cast_ne_zero.2 hm
+  have hs := (Set.finite_range y).measurableSet.compl
+  refine ⟨(m : ℝ≥0∞)⁻¹ • ∑ k, Measure.dirac (y k),
+    ⟨by simp [ENNReal.inv_mul_cancel hm0 (ENNReal.natCast_ne_top m)]⟩,
+    ⟨Set.range y, Set.finite_range y, by simp [Measure.dirac_apply' _ hs]⟩, ?_⟩
+  ext s hs
+  simp only [resample, _root_.sum_apply, smul_apply, add_apply, smul_eq_mul]
+  simp [← Finset.mul_sum, Finset.sum_add_distrib, mul_add,
+    ENNReal.mul_inv_cancel_left hm0 (ENNReal.natCast_ne_top m)]
+  ring
+
+/-- **No sample size carries evidence.** For the i.i.d. null generated by the mixtures
+`(1 - ε) F + ε Q` of the probability measures `F` carried by a finite set with `Q`, the maximal
+expected logarithm under `Q ^ n` of an `n`-sample e-variable is `0`, for every `n`. -/
+theorem maxLogGrowth_finitelySupported_mixtures_eq_zero (Q : Measure 𝓧) [IsProbabilityMeasure Q]
+    (hε : ε ≤ 1) (n : ℕ) :
+    maxLogGrowth Q {(1 - ε) • F + ε • Q | (F : Measure 𝓧) (_ : IsProbabilityMeasure F)
+      (_ : ∃ s : Set 𝓧, s.Finite ∧ F sᶜ = 0)} n = 0 := by
+  -- the fraction of the injective maps among the maps `Fin n → Fin m` tends to `1`
+  have hlim : Tendsto (fun m : ℕ ↦ (m.descFactorial n : ℝ≥0∞) * (m : ℝ≥0∞)⁻¹ ^ n) atTop
+      (𝓝 1) := by
+    have h := (Asymptotics.isEquivalent_iff_tendsto_one
+      ((eventually_ne_atTop 0).mono fun m hm ↦ pow_ne_zero n (Nat.cast_ne_zero.2 hm))).1
+      (isEquivalent_descFactorial n)
+    refine (by simpa using ENNReal.tendsto_ofReal h :
+      Tendsto (fun m : ℕ ↦ ENNReal.ofReal ((m.descFactorial n : ℝ) / (m : ℝ) ^ n)) atTop
+        (𝓝 1)).congr' ?_
+    filter_upwards [eventually_ne_atTop 0] with m hm
+    simp [div_eq_mul_inv, ENNReal.ofReal_mul, ENNReal.ofReal_inv_of_pos, ENNReal.ofReal_pow,
+      Nat.pos_of_ne_zero hm, ENNReal.inv_pow]
+  rw [maxLogGrowth_def]
+  refine maxUtility_eq_zero_of_mem_effectiveSet fun E hE ↦
+    ENNReal.le_of_forall_lt_one_mul_le fun a ha ↦ ?_
+  obtain ⟨m, ham, hm⟩ := ((hlim.eventually (lt_mem_nhds ha)).and (eventually_ne_atTop 0)).exists
+  exact (mul_le_mul_left ham.le _).trans
+    (descFactorial_mul_lintegral_le hε hm (sum_resample_mem hm) hE)
+
+/-- For the i.i.d. null generated by the mixtures `(1 - ε) F + ε Q` of the probability measures
+`F` carried by a finite set with `Q`, the bipolar rate of `Q` is `0`. -/
+theorem bipolarRate_finitelySupported_mixtures_eq_zero (Q : Measure 𝓧) [IsProbabilityMeasure Q]
+    (hε : ε ≤ 1) :
+    bipolarRate Q {(1 - ε) • F + ε • Q | (F : Measure 𝓧) (_ : IsProbabilityMeasure F)
+      (_ : ∃ s : Set 𝓧, s.Finite ∧ F sᶜ = 0)} = 0 :=
+  le_antisymm (bipolarRate_le_iff.2 fun n _ ↦ by
+    rw [maxLogGrowth_finitelySupported_mixtures_eq_zero Q hε n, mul_zero]) (bipolarRate_nonneg _ _)
+
+/-- For a probability measure `Q` without atoms, the smallest relative entropy from `Q` to the
+mixtures `(1 - ε) F + ε Q` of the probability measures `F` carried by a finite set with `Q` is
+`log (1 / ε)`: each `F` is singular to `Q`. -/
+theorem iInf_klDiv_finitelySupported_mixtures (Q : Measure 𝓧) [IsProbabilityMeasure Q]
+    [NullSingletonClass Q] (hε : ε ≤ 1) :
+    ((⨅ P ∈ {(1 - ε) • F + ε • Q | (F : Measure 𝓧) (_ : IsProbabilityMeasure F)
+      (_ : ∃ s : Set 𝓧, s.Finite ∧ F sᶜ = 0)}, klDiv Q P : ℝ≥0∞) : EReal) =
+        ENNReal.log ε⁻¹ := by
+  obtain ⟨x⟩ := nonempty_of_isProbabilityMeasure Q
+  refine iInf_klDiv_mixture_of_mutuallySingular
+    ⟨_, Measure.dirac x, inferInstance, ⟨{x}, Set.finite_singleton x, by simp⟩, rfl⟩ ?_ hε
+  rintro _ ⟨F, hF, ⟨s, hs, hFs⟩, rfl⟩
+  exact ⟨F, hF, ⟨sᶜ, hs.measurableSet.compl, hFs, by rw [compl_compl]; exact hs.measure_zero Q⟩,
+    rfl⟩
+
+end ProbabilityTheory

LMLExplore/EValues/EffectiveSet.lean

@@ -52,6 +52,8 @@ measures `S`.
 * `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].
+* `ProbabilityTheory.maxUtility_eq_zero_of_mem_effectiveSet`: no e-variable for `S` has a
+  positive expected logarithm under a probability measure of the effective null of `S`.
 
 ## References
 
@@ -269,4 +271,17 @@ theorem exists_powered_test_iff (hS : ∀ P ∈ S, IsProbabilityMeasure P) (Q :
             ENNReal.mul_lt_mul_right (ENNReal.inv_ne_zero.mpr hNtop) (ENNReal.inv_ne_top.mpr hN0)
               hYQ
 
+/-- Under a probability measure `P` of the effective null of `S`, no e-variable for `S` has a
+positive expected logarithm, by Jensen's inequality: the maximal expected logarithm is `0`.
+Statlib's `maxUtility_eq_zero_of_mem` is the analogue for the members of `S`. Adapted from the
+helper `maxUtility_log_nonpos_of_forall_lintegral_le_one` of
+`EValuesResearch/Results/RateVersusKL.lean` (commit `dd4072f`) in the paper project
+`RemyDegenne/evalues_research` (same author). -/
+theorem maxUtility_eq_zero_of_mem_effectiveSet {P : Measure Ω} [IsProbabilityMeasure P]
+    (hP : P ∈ effectiveSet S) : maxUtility P S logUtility = 0 := by
+  refine le_antisymm (iSup₂_le fun X hX ↦ ?_) (maxUtility_nonneg P)
+  calc ∫ᵉ ω, (logUtility ∘ X) ω ∂P
+  _ ≤ logUtility (∫⁻ ω, X ω ∂P) := Utility.eintegral_le_map logUtility hX.measurable.aemeasurable
+  _ ≤ 0 := by rw [logUtility_apply, ENNReal.log_le_zero_iff]; exact hP X hX
+
 end ProbabilityTheory

LMLExplore/EValues/Utility/Basic.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 Statlib.EValues.Utility.Basic
+
+/-!
+# Expected utility of a constant multiple of an indicator
+
+Under a probability measure `μ` carried by a set `A`, the e-variable `c` times the indicator of
+`A` is almost surely `c`, so its expected utility is `U c`, for every utility function `U`
+(Statlib's `ProbabilityTheory.Utility`). With the logarithmic utility, this is the expected
+logarithm `log c` of the e-variables that bound relative entropies and growth rates from below.
+
+## Main statements
+
+* `ProbabilityTheory.Utility.eintegral_comp_indicator_const`:
+  `∫ᵉ x, (U ∘ A.indicator fun _ ↦ c) x ∂μ = U c` for `μ Aᶜ = 0`.
+-/
+
+public section
+
+open MeasureTheory
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
+
+/-- Under a probability measure `μ` carried by a set `A`, the expected utility of `c` times the
+indicator of `A` is `U c`. -/
+lemma Utility.eintegral_comp_indicator_const (U : Utility) {μ : Measure Ω}
+    [IsProbabilityMeasure μ] {A : Set Ω} (hA : μ Aᶜ = 0) (c : ℝ≥0∞) :
+    ∫ᵉ x, (U ∘ A.indicator fun _ ↦ c) x ∂μ = U c := by
+  rw [eintegral_congr_ae (g := fun _ ↦ U c), eintegral_const, measure_univ,
+    EReal.coe_ennreal_one, mul_one]
+  filter_upwards [mem_ae_iff.2 hA] with x hx
+  simp [hx]
+
+end ProbabilityTheory