diff --git a/LMLExplore/EValues/BipolarRate/Circle.lean b/LMLExplore/EValues/BipolarRate/Circle.lean
new file mode 100644
index 00000000..a5418c01
--- /dev/null
+++ b/LMLExplore/EValues/BipolarRate/Circle.lean
@@ -0,0 +1,349 @@
+/-
+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
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
+public import Mathlib.Probability.UniformOn
+import LMLExplore.EValues.EffectiveSet
+import LMLExplore.EValues.Utility.Basic
+import LMLExplore.InformationTheory.KullbackLeibler.Mixture
+import LMLExplore.MeasureTheory.Integral.IntervalIntegral.Periodic
+import Statlib.ForMathlib.MeasureTheory.Constructions.Pi
+import TauCeti.MeasureTheory.Measure.Haar.UnitAddTorus
+
+/-!
+# One observation without evidence, at a positive bipolar rate, on the circle
+
+On the circle `UnitAddCircle = ℝ / ℤ` with Lebesgue measure `volume`, and for `ε ≤ 1`, consider
+the i.i.d. null generated by the mixtures `(1 - ε) U + ε volume`, with `U` the uniform law
+`uniformOn` on a finite coset `x₀ + (1 / N) ℤ` of the circle, written
+`{x | x - x₀ ∈ AddSubgroup.zmultiples (1 / N)}` (for `N = 0` it is the point `x₀`, as for
+`N = 1`, since `0⁻¹ = 0`). Then:
+
+* one observation carries no evidence against the null: `maxLogGrowth volume S 1 = 0`, since
+  Lebesgue measure is the average over `x₀` of the members `(1 - ε) δ_{x₀} + ε volume`;
+* the bipolar rate and the smallest relative entropy from `volume` to the null are both
+  `log (1 / ε)` (infinite for `ε = 0`).
+
+So the bipolar rate equals the smallest relative entropy to the null, although, for `ε < 1`, the
+smallest relative entropy, as a function of the law, is not lower semicontinuous at `volume` for
+the topology of the integrals of bounded measurable functions, which
+`ProbabilityTheory.bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le` [RR26, Theorem 4.1]
+assumes: the laws `(1 - ε) U + ε volume` approach `volume` in that topology (this is not proved
+here), and one observation cannot tell them from `volume`. The larger null of the mixtures
+`(1 - ε) F + ε volume` with `F` any finitely supported law has the same smallest relative entropy
+but bipolar rate `0` (`ProbabilityTheory.bipolarRate_finitelySupported_mixtures_eq_zero`).
+
+## Main statements
+
+* `ProbabilityTheory.maxLogGrowth_one_coset_mixtures_eq_zero`: one observation carries no
+  evidence.
+* `ProbabilityTheory.bipolarRate_coset_mixtures`: the bipolar rate is `log (1 / ε)`.
+* `ProbabilityTheory.iInf_klDiv_coset_mixtures`: the smallest relative entropy from `volume` to
+  the null is `log (1 / ε)`.
+
+## Implementation notes
+
+The lower bound on the bipolar rate tests the tuples whose pairwise differences are irrational,
+which have probability `1` under `volume ^ n`. Under the `n`-fold product of a member of the null,
+two coordinates drawn from the coset part differ by a rational, so such a tuple has at most one
+coordinate in the coset: its probability is at most `n ε ^ (n - 1)`. The indicator of these
+tuples divided by `n ε ^ (n - 1)` is an `n`-sample e-variable with expected logarithm
+`(n - 1) log (1 / ε) - log n`.
+
+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 defines the coset law and the null instead
+of writing them in the statements.
+
+## 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 {ε : ℝ≥0∞}
+
+/-! ### Rational differences -/
+
+/-- The image of the rationals in the circle. -/
+private def ratCircle : Set UnitAddCircle := Set.range fun q : ℚ ↦ ((q : ℝ) : UnitAddCircle)
+
+/-- The tuples of points of the circle whose pairwise differences are irrational. -/
+private def pairwiseIrrational (n : ℕ) : Set (Fin n → UnitAddCircle) :=
+  {x | ∀ i j, i ≠ j → x i - x j ∉ ratCircle}
+
+/-- The tuples with pairwise irrational differences form a measurable set. -/
+private lemma measurableSet_pairwiseIrrational (n : ℕ) :
+    MeasurableSet (pairwiseIrrational n) := by
+  have h : pairwiseIrrational n =
+      ⋂ i, ⋂ j, ⋂ (_ : i ≠ j), (fun x : Fin n → UnitAddCircle ↦ x i - x j) ⁻¹' ratCircleᶜ := by
+    ext x
+    simp [pairwiseIrrational]
+  rw [h]
+  exact .iInter fun i ↦ .iInter fun j ↦ .iInter fun _ ↦
+    ((measurable_pi_apply i).sub (measurable_pi_apply j))
+      (Set.countable_range _).measurableSet.compl
+
+/-- An i.i.d. uniform sample on the circle has pairwise irrational differences almost surely. -/
+private lemma volume_pi_compl_pairwiseIrrational (n : ℕ) :
+    (Measure.pi fun _ : Fin n ↦ (volume : Measure UnitAddCircle)) (pairwiseIrrational n)ᶜ = 0 := by
+  have h : (pairwiseIrrational n)ᶜ =
+      ⋃ i, ⋃ j, ⋃ (_ : i ≠ j), {x : Fin n → UnitAddCircle | x i - x j ∈ ratCircle} := by
+    ext x
+    simp [pairwiseIrrational]
+  rw [h]
+  refine measure_iUnion_null fun i ↦ measure_iUnion_null fun j ↦ measure_iUnion_null fun hij ↦ ?_
+  -- the pair of coordinates `(x i, x j)` has law `volume ⊗ volume`
+  have hσ : Function.Injective ![i, j] := by
+    intro a b hab
+    fin_cases a <;> fin_cases b <;> simp_all [eq_comm]
+  have hmp := (measurePreserving_finTwoArrow (volume : Measure UnitAddCircle)).comp
+    (⟨by fun_prop, Measure.pi_map_comp_of_injective _ hσ⟩ :
+      MeasurePreserving (fun x : Fin n → UnitAddCircle ↦ fun k ↦ x (![i, j] k))
+        (Measure.pi fun _ ↦ volume) (Measure.pi fun _ ↦ volume))
+  have hs : MeasurableSet {p : UnitAddCircle × UnitAddCircle | p.1 - p.2 ∈ ratCircle} :=
+    (measurable_fst.sub measurable_snd) (Set.countable_range _).measurableSet
+  have h := hmp.measure_preimage hs.nullMeasurableSet
+  simp only [Set.preimage_ofPred_eq, Function.comp_apply, MeasurableEquiv.finTwoArrow_apply,
+    Matrix.cons_val_zero, Matrix.cons_val_one] at h
+  rw [h, Measure.prod_apply_symm hs]
+  refine lintegral_eq_zero_of_ae_eq_zero (.of_forall fun y ↦ ?_)
+  -- for fixed `y`, the points `x` with `x - y` rational form a countable set
+  exact ((Set.countable_range _).preimage (sub_left_injective (b := y))).measure_zero _
+
+/-- Under the `n`-fold product of a law that gives mass at least `1 - ε` to a set `C` whose
+points differ by rationals, the tuples with pairwise irrational differences have at most one
+coordinate in `C`, hence probability at most `n ε ^ (n - 1)`. -/
+private lemma measure_pi_pairwiseIrrational_le {P : Measure UnitAddCircle}
+    [IsProbabilityMeasure P] {C : Set UnitAddCircle} (hPC : P Cᶜ ≤ ε)
+    (hC : ∀ a ∈ C, ∀ b ∈ C, a - b ∈ ratCircle) {n : ℕ} (hn : n ≠ 0) :
+    (Measure.pi fun _ : Fin n ↦ P) (pairwiseIrrational n) ≤ n * ε ^ (n - 1) := by
+  classical
+  have hsub : pairwiseIrrational n ⊆
+      ⋃ k, Set.univ.pi (Function.update (fun _ : Fin n ↦ Cᶜ) k Set.univ) := by
+    intro x hx
+    -- `k` is the coordinate in `C`, if there is one
+    obtain ⟨k, hk⟩ : ∃ k, ∀ i ≠ k, x i ∉ C := by
+      by_cases h : ∃ k, x k ∈ C
+      · obtain ⟨k, hk⟩ := h
+        exact ⟨k, fun i hik hi ↦ hx i k hik (hC _ hi _ hk)⟩
+      · push Not at h
+        exact ⟨⟨0, Nat.pos_of_ne_zero hn⟩, fun i _ ↦ h i⟩
+    refine Set.mem_iUnion.2 ⟨k, fun i _ ↦ ?_⟩
+    by_cases hik : i = k
+    · subst hik
+      simp
+    · rw [Function.update_of_ne hik]
+      exact hk i hik
+  calc (Measure.pi fun _ : Fin n ↦ P) (pairwiseIrrational n)
+  _ ≤ ∑ k, (Measure.pi fun _ : Fin n ↦ P)
+      (Set.univ.pi (Function.update (fun _ : Fin n ↦ Cᶜ) k Set.univ)) :=
+    (measure_mono hsub).trans (measure_iUnion_fintype_le _ _)
+  _ ≤ ∑ _k : Fin n, ε ^ (n - 1) := by
+    refine Finset.sum_le_sum fun k _ ↦ ?_
+    rw [Measure.pi_pi]
+    simp_rw [Function.apply_update (fun _ s ↦ P s)]
+    have hcard : (Finset.univ \ {k}).card = n - 1 := by simp [Finset.card_sdiff]
+    rw [Finset.prod_update_of_mem (Finset.mem_univ k), measure_univ, one_mul, Finset.prod_const,
+      hcard]
+    gcongr
+  _ = n * ε ^ (n - 1) := by simp
+
+/-- For a null whose members give mass at least `1 - ε` to sets whose points differ by
+rationals, the indicator of the tuples with pairwise irrational differences, divided by
+`n ε ^ (n - 1)`, gives the lower bound `log (1 / (n ε ^ (n - 1)))` on the growth of `n`
+observations. -/
+private lemma log_le_maxLogGrowth {S : Set (Measure UnitAddCircle)}
+    (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hSC : ∀ P ∈ S, ∃ C, P Cᶜ ≤ ε ∧ ∀ a ∈ C, ∀ b ∈ C, a - b ∈ ratCircle) {n : ℕ} (hn : n ≠ 0) :
+    ENNReal.log ((n * ε ^ (n - 1))⁻¹) ≤ maxLogGrowth volume S n := by
+  set c := ((n : ℝ≥0∞) * ε ^ (n - 1))⁻¹
+  have hA := measurableSet_pairwiseIrrational n
+  have hX : IsEVar ((pairwiseIrrational n).indicator fun _ ↦ c)
+      ((fun P ↦ Measure.pi fun _ : Fin n ↦ P) '' S) := by
+    refine IsEVar.of_lintegral_le_one ?_ (measurable_const.indicator hA) ?_
+    · rintro _ ⟨P, hP, rfl⟩
+      have := hS P hP
+      infer_instance
+    · rintro _ ⟨P, hP, rfl⟩
+      have := hS P hP
+      obtain ⟨C, hPC, hC⟩ := hSC P hP
+      rw [lintegral_indicator_const hA]
+      calc c * (Measure.pi fun _ : Fin n ↦ P) (pairwiseIrrational n)
+      _ ≤ c * (n * ε ^ (n - 1)) := by gcongr; exact measure_pi_pairwiseIrrational_le hPC hC hn
+      _ ≤ 1 := ENNReal.inv_mul_le_one _
+  rw [maxLogGrowth_def]
+  exact (logUtility.eintegral_comp_indicator_const (volume_pi_compl_pairwiseIrrational n)
+    c).symm.trans_le (hX.eintegral_le_maxUtility _ logUtility)
+
+/-- If the growth of `n` observations is at least `log (1 / (n ε ^ (n - 1)))` for every `n ≠ 0`,
+the bipolar rate is at least `log (1 / ε)`: the term `log n` is negligible against `n`. For
+`ε = 0`, two observations already give infinite growth. -/
+private lemma log_inv_le_bipolarRate {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {Q : Measure 𝓧}
+    {S : Set (Measure 𝓧)} (hε : ε ≤ 1)
+    (h : ∀ n : ℕ, n ≠ 0 → ENNReal.log (((n : ℝ≥0∞) * ε ^ (n - 1))⁻¹) ≤ maxLogGrowth Q S n) :
+    ENNReal.log ε⁻¹ ≤ bipolarRate Q S := by
+  rcases eq_or_ne ε 0 with rfl | hε0
+  · have h2 := h 2 two_ne_zero
+    simp only [Nat.add_one_sub_one, pow_one, mul_zero, ENNReal.inv_zero, ENNReal.log_top,
+      top_le_iff] at h2
+    refine le_trans ?_ (maxLogGrowth_div_le_bipolarRate _ _ two_ne_zero)
+    rw [h2, ENNReal.inv_zero, ENNReal.log_top,
+      EReal.top_div_of_pos_ne_top (by norm_num) (EReal.natCast_ne_top 2)]
+  -- for `ε > 0`, the growth of `n + 1` observations is at least `n log (1 / ε) - log (n + 1)`
+  set e := ε.toReal
+  have hε_top : ε ≠ ⊤ := ne_top_of_le_ne_top ENNReal.one_ne_top hε
+  have he0 : 0 < e := ENNReal.toReal_pos hε0 hε_top
+  have hεe : ε = ENNReal.ofReal e := (ENNReal.ofReal_toReal hε_top).symm
+  have hlog : ENNReal.log ε⁻¹ = (Real.log e⁻¹ : EReal) := by
+    rw [hεe, ← ENNReal.ofReal_inv_of_pos he0, ENNReal.log_ofReal_of_pos (inv_pos.2 he0)]
+  rw [hlog]
+  refine le_bipolarRate_of_tendsto (r := fun n ↦ n * Real.log e⁻¹ - Real.log (n + 1))
+    (fun n ↦ le_trans (le_of_eq ?_) (h (n + 1) n.succ_ne_zero)) ?_
+  · -- move to `ℝ`, where the identity is `Real.log` of a product
+    have hpos : 0 < ((n : ℝ) + 1) * e ^ n := by positivity
+    have hcast : ((n + 1 : ℕ) : ℝ≥0∞) * ε ^ (n + 1 - 1) =
+        ENNReal.ofReal (((n : ℝ) + 1) * e ^ n) := by
+      rw [ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_pow he0.le, ← hεe]
+      norm_cast
+    rw [hcast, ← ENNReal.ofReal_inv_of_pos hpos, ENNReal.log_ofReal_of_pos (inv_pos.2 hpos),
+      EReal.coe_eq_coe_iff]
+    simp only [Real.log_inv]
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_pow]
+    ring
+  · have h1 : Tendsto (fun n : ℕ ↦ (n : ℝ) / (n + 1)) atTop (𝓝 1) :=
+      tendsto_natCast_div_add_atTop 1
+    have h2 : Tendsto (fun n : ℕ ↦ Real.log ((n : ℝ) + 1) / ((n : ℝ) + 1)) atTop (𝓝 0) := by
+      have := (Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 one_ne_zero).comp
+        (tendsto_atTop_add_const_right atTop (1 : ℝ) tendsto_natCast_atTop_atTop)
+      simpa [Function.comp_def] using this
+    convert (h1.const_mul (Real.log e⁻¹)).sub h2 using 2 with n
+    · field_simp
+    · simp
+
+/-! ### The cosets -/
+
+/-- The subgroup `(1 / N) ℤ` of the circle is contained in the image of the rationals. -/
+private lemma zmultiples_subset_ratCircle (N : ℕ) :
+    (AddSubgroup.zmultiples (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle) : Set UnitAddCircle) ⊆
+      ratCircle := by
+  rintro _ ⟨k, rfl⟩
+  refine ⟨(k : ℚ) / N, ?_⟩
+  beta_reduce
+  rw [← AddCircle.coe_zsmul, zsmul_eq_mul]
+  congr 1
+  push_cast
+  ring
+
+/-- The coset `x₀ + (1 / N) ℤ` of the circle is finite. -/
+private lemma finite_coset (x₀ : UnitAddCircle) (N : ℕ) :
+    {x | x - x₀ ∈ AddSubgroup.zmultiples (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)}.Finite := by
+  have h : IsOfFinAddOrder (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle) := by
+    rcases eq_or_ne N 0 with rfl | hN
+    · simp
+    refine isOfFinAddOrder_iff_nsmul_eq_zero.2 ⟨N, Nat.pos_of_ne_zero hN, ?_⟩
+    rw [← AddCircle.coe_nsmul, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.2 hN)]
+    exact AddCircle.coe_period 1
+  have := h.finite_zmultiples
+  exact (Set.toFinite _).preimage (sub_left_injective.injOn)
+
+/-- The members of the coset null are probability measures. -/
+private lemma isProbabilityMeasure_coset_mixture (hε : ε ≤ 1) (x₀ : UnitAddCircle) (N : ℕ) :
+    IsProbabilityMeasure ((1 - ε) • uniformOn {x | x - x₀ ∈ AddSubgroup.zmultiples
+      (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)} + ε • volume) := by
+  have := isProbabilityMeasure_uniformOn (finite_coset x₀ N) ⟨x₀, by simp⟩
+  exact ⟨by simp [tsub_add_cancel_of_le hε]⟩
+
+/-- For `N = 1`, the coset `x₀ + ℤ` of the circle is the point `x₀`. -/
+private lemma uniformOn_coset_one (x₀ : UnitAddCircle) :
+    uniformOn {x | x - x₀ ∈ AddSubgroup.zmultiples ((((1 : ℕ) : ℝ)⁻¹ : ℝ) : UnitAddCircle)} =
+      Measure.dirac x₀ := by
+  classical
+  have h1 : ((1 : ℝ) : UnitAddCircle) = 0 := AddCircle.coe_period 1
+  have h : {x | x - x₀ ∈ AddSubgroup.zmultiples ((((1 : ℕ) : ℝ)⁻¹ : ℝ) : UnitAddCircle)} =
+      {x₀} := by
+    ext x
+    simp [h1, sub_eq_zero]
+  ext t ht
+  rw [h, uniformOn_singleton, Measure.dirac_apply' _ ht]
+  by_cases hx : x₀ ∈ t <;> simp [hx]
+
+/-! ### The coset null -/
+
+/-- **One observation carries no evidence** against the null generated by the mixtures
+`(1 - ε) U + ε volume` on the circle, with `U` uniform on a coset `x₀ + (1 / N) ℤ`: the maximal
+expected logarithm of an e-variable under Lebesgue measure is `0`. -/
+theorem maxLogGrowth_one_coset_mixtures_eq_zero (hε : ε ≤ 1) :
+    maxLogGrowth volume {(1 - ε) • uniformOn {x | x - x₀ ∈ AddSubgroup.zmultiples
+      (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)} + ε • volume |
+      (x₀ : UnitAddCircle) (N : ℕ)} 1 = 0 := by
+  rw [maxLogGrowth_one]
+  refine maxUtility_eq_zero_of_mem_effectiveSet fun X hX ↦ ?_
+  set c := ∫⁻ x, X x ∂(volume : Measure UnitAddCircle)
+  -- Lebesgue measure is the average over `x` of the members `(1 - ε) δ_x + ε volume`
+  have hx (x : UnitAddCircle) : (1 - ε) * X x + ε * c ≤ 1 := by
+    have := isProbabilityMeasure_coset_mixture hε x 1
+    have h := hX.lintegral_le_measure_univ _ ⟨x, 1, rfl⟩
+    rw [uniformOn_coset_one] at h
+    simpa [c, lintegral_add_measure, tsub_add_cancel_of_le hε] using h
+  calc c
+  _ = ((1 - ε) + ε) * c := by rw [tsub_add_cancel_of_le hε, one_mul]
+  _ = ∫⁻ x, ((1 - ε) * X x + ε * c) ∂(volume : Measure UnitAddCircle) := by
+    simp [c, lintegral_add_right _ measurable_const, lintegral_const_mul _ hX.measurable, add_mul]
+  _ ≤ ∫⁻ _, 1 ∂(volume : Measure UnitAddCircle) := lintegral_mono hx
+  _ = 1 := by simp
+
+/-- The smallest relative entropy from Lebesgue measure on the circle to the mixtures
+`(1 - ε) U + ε volume`, with `U` uniform on a coset `x₀ + (1 / N) ℤ`, is `log (1 / ε)`: each `U`
+is singular to Lebesgue measure. -/
+theorem iInf_klDiv_coset_mixtures (hε : ε ≤ 1) :
+    ((⨅ P ∈ {(1 - ε) • uniformOn {x | x - x₀ ∈ AddSubgroup.zmultiples
+      (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)} + ε • volume |
+      (x₀ : UnitAddCircle) (N : ℕ)}, klDiv volume P : ℝ≥0∞) : EReal) = ENNReal.log ε⁻¹ := by
+  refine iInf_klDiv_mixture_of_mutuallySingular ⟨_, 0, 0, rfl⟩ ?_ hε
+  rintro _ ⟨x₀, N, rfl⟩
+  have hfin := finite_coset x₀ N
+  refine ⟨_, isProbabilityMeasure_uniformOn hfin ⟨x₀, by simp⟩,
+    ⟨_, hfin.measurableSet.compl, ?_, ?_⟩, rfl⟩
+  · exact (uniformOn_eq_zero_iff hfin).2 (Set.inter_compl_self _)
+  · rw [compl_compl]
+    exact hfin.measure_zero _
+
+/-- The bipolar rate of Lebesgue measure on the circle against the mixtures `(1 - ε) U + ε volume`,
+with `U` uniform on a coset `x₀ + (1 / N) ℤ`, is `log (1 / ε)`, the smallest relative entropy to
+the null (`ProbabilityTheory.iInf_klDiv_coset_mixtures`). -/
+theorem bipolarRate_coset_mixtures (hε : ε ≤ 1) :
+    bipolarRate volume {(1 - ε) • uniformOn {x | x - x₀ ∈ AddSubgroup.zmultiples
+      (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)} + ε • volume |
+      (x₀ : UnitAddCircle) (N : ℕ)} = ENNReal.log ε⁻¹ := by
+  set S := {(1 - ε) • uniformOn {x | x - x₀ ∈ AddSubgroup.zmultiples
+      (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)} + ε • volume | (x₀ : UnitAddCircle) (N : ℕ)}
+  have hS : ∀ P ∈ S, IsProbabilityMeasure P := by
+    rintro _ ⟨x₀, N, rfl⟩
+    exact isProbabilityMeasure_coset_mixture hε x₀ N
+  have hSC : ∀ P ∈ S, ∃ C, P Cᶜ ≤ ε ∧ ∀ a ∈ C, ∀ b ∈ C, a - b ∈ ratCircle := by
+    rintro _ ⟨x₀, N, rfl⟩
+    refine ⟨{x | x - x₀ ∈ AddSubgroup.zmultiples (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)}, ?_,
+      fun a ha b hb ↦ zmultiples_subset_ratCircle N
+        (by simpa using sub_mem (Set.mem_ofPred.1 ha) (Set.mem_ofPred.1 hb))⟩
+    simp only [add_apply, smul_apply, smul_eq_mul,
+      (uniformOn_eq_zero_iff (finite_coset x₀ N)).2 (Set.inter_compl_self _), mul_zero, zero_add]
+    exact mul_le_of_le_one_right' prob_le_one
+  exact le_antisymm ((bipolarRate_le_iInf_klDiv volume hS).trans_eq
+    (iInf_klDiv_coset_mixtures hε)) (log_inv_le_bipolarRate hε fun n hn ↦
+      log_le_maxLogGrowth hS hSC hn)
+
+end ProbabilityTheory
diff --git a/LMLExplore/EValues/BipolarRate/FiniteSupport.lean b/LMLExplore/EValues/BipolarRate/FiniteSupport.lean
new file mode 100644
index 00000000..7e47754c
--- /dev/null
+++ b/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
diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean
index cc55fcc8..047628bf 100644
--- a/LMLExplore/EValues/EffectiveSet.lean
+++ b/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
diff --git a/LMLExplore/EValues/Utility/Basic.lean b/LMLExplore/EValues/Utility/Basic.lean
new file mode 100644
index 00000000..6238e5d2
--- /dev/null
+++ b/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
diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Mixture.lean b/LMLExplore/InformationTheory/KullbackLeibler/Mixture.lean
new file mode 100644
index 00000000..2c23ae09
--- /dev/null
+++ b/LMLExplore/InformationTheory/KullbackLeibler/Mixture.lean
@@ -0,0 +1,103 @@
+/-
+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.InformationTheory.KullbackLeibler.Basic
+public import Statlib.EValues.RIPr
+import LMLExplore.EValues.Utility.Basic
+
+/-!
+# The relative entropy to a mixture with a singular law
+
+For probability measures `μ` and `ν` with `ν` singular to `μ`, and `ε ≤ 1`, the relative entropy
+from `μ` to the mixture `(1 - ε) ν + ε μ` is `log (1 / ε)`: the density of `μ` with respect to the
+mixture is `1 / ε` on a set that carries `μ` and that `ν` does not charge. The proof uses
+Statlib's variational form of the relative entropy, the maximal expected logarithm of an
+e-variable for the singleton null (`maxUtility_singleton_eq_klDiv`): an e-variable for the mixture
+has integral at most `1 / ε` under `μ`, and `1 / ε` times the indicator of that set is an
+e-variable for the mixture.
+
+## Main statements
+
+* `InformationTheory.klDiv_mixture_of_mutuallySingular`:
+  `klDiv μ ((1 - ε) • ν + ε • μ) = log (1 / ε)` for `ν ⟂ₘ μ`.
+* `InformationTheory.iInf_klDiv_mixture_of_mutuallySingular`: the smallest relative entropy
+  from `μ` to a nonempty set of such mixtures is `log (1 / ε)`.
+
+## Implementation notes
+
+The statement and its proof are adapted from the helper `klDiv_mixture_eq_log_inv` of
+`EValuesResearch/Results/RateVersusKL.lean` (commit `dd4072f`) in the paper project
+`RemyDegenne/evalues_research` (same author), with its separating set replaced by the
+hypothesis `ν ⟂ₘ μ`.
+-/
+
+public section
+
+open MeasureTheory ProbabilityTheory
+open scoped ENNReal
+
+namespace InformationTheory
+
+variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧}
+
+/-- The relative entropy from a probability measure `μ` to its mixture `(1 - ε) ν + ε μ` with a
+probability measure `ν` singular to `μ` is `log (1 / ε)`, for `ε ≤ 1`. It is infinite for
+`ε = 0`. -/
+theorem klDiv_mixture_of_mutuallySingular {μ ν : Measure 𝓧} [IsProbabilityMeasure μ]
+    [IsProbabilityMeasure ν] (hνμ : ν ⟂ₘ μ) {ε : ℝ≥0∞} (hε : ε ≤ 1) :
+    ((klDiv μ ((1 - ε) • ν + ε • μ) : ℝ≥0∞) : EReal) = ENNReal.log ε⁻¹ := by
+  set P := (1 - ε) • ν + ε • μ with hP_def
+  have hP : IsProbabilityMeasure P := ⟨by simp [P, tsub_add_cancel_of_le hε]⟩
+  set t := hνμ.nullSet
+  have ht : MeasurableSet t := hνμ.measurableSet_nullSet
+  rw [← maxUtility_singleton_eq_klDiv]
+  refine le_antisymm (iSup₂_le fun X hX ↦ ?_) ?_
+  · -- an e-variable for the mixture has integral at most `1 / ε` under `μ`
+    rcases eq_or_ne ε 0 with rfl | hε0
+    · simp
+    have hle : ∫⁻ x, X x ∂μ ≤ ε⁻¹ := by
+      rw [ENNReal.le_inv_iff_mul_le, mul_comm]
+      calc ε * ∫⁻ x, X x ∂μ
+      _ ≤ (1 - ε) * ∫⁻ x, X x ∂ν + ε * ∫⁻ x, X x ∂μ := le_add_self
+      _ = ∫⁻ x, X x ∂P := by simp [P, lintegral_add_measure]
+      _ ≤ P .univ := hX.lintegral_le_measure_univ P rfl
+      _ = 1 := measure_univ
+    calc ∫ᵉ x, (logUtility ∘ X) x ∂μ
+    _ ≤ logUtility (∫⁻ x, X x ∂μ) :=
+      Utility.eintegral_le_map logUtility hX.measurable.aemeasurable
+    _ ≤ ENNReal.log ε⁻¹ := ENNReal.log_monotone hle
+  · -- `1 / ε` times the indicator of the set `t` charged by `μ` alone is an e-variable
+    have hX : IsEVar (t.indicator fun _ ↦ ε⁻¹) {P} := by
+      refine IsEVar.of_lintegral_le_one (by simpa using hP)
+        (measurable_const.indicator ht) fun P' hP' ↦ ?_
+      rw [Set.mem_singleton_iff.1 hP', lintegral_indicator_const ht]
+      calc ε⁻¹ * P t
+      _ = ε⁻¹ * (ε * μ t) := by simp [P, t, hνμ.measure_nullSet]
+      _ ≤ ε⁻¹ * ε := by gcongr; exact mul_le_of_le_one_right' prob_le_one
+      _ ≤ 1 := ENNReal.inv_mul_le_one ε
+    exact (logUtility.eintegral_comp_indicator_const hνμ.measure_compl_nullSet ε⁻¹).symm.trans_le
+      (hX.eintegral_le_maxUtility μ logUtility)
+
+/-- The smallest relative entropy from a probability measure `μ` to a nonempty set of mixtures
+`(1 - ε) ν + ε μ`, each with a probability measure `ν` singular to `μ`, is `log (1 / ε)`, for
+`ε ≤ 1`: every member is at relative entropy `log (1 / ε)`
+(`InformationTheory.klDiv_mixture_of_mutuallySingular`). -/
+theorem iInf_klDiv_mixture_of_mutuallySingular {μ : Measure 𝓧} [IsProbabilityMeasure μ]
+    {ε : ℝ≥0∞} {S : Set (Measure 𝓧)} (hS : S.Nonempty)
+    (h : ∀ P ∈ S, ∃ ν : Measure 𝓧, IsProbabilityMeasure ν ∧ ν ⟂ₘ μ ∧ P = (1 - ε) • ν + ε • μ)
+    (hε : ε ≤ 1) :
+    ((⨅ P ∈ S, klDiv μ P : ℝ≥0∞) : EReal) = ENNReal.log ε⁻¹ := by
+  have hkl (P : Measure 𝓧) (hP : P ∈ S) : ((klDiv μ P : ℝ≥0∞) : EReal) = ENNReal.log ε⁻¹ := by
+    obtain ⟨ν, hν, hνμ, rfl⟩ := h P hP
+    exact klDiv_mixture_of_mutuallySingular hνμ hε
+  obtain ⟨P₀, hP₀⟩ := hS
+  rw [← hkl P₀ hP₀]
+  congr 1
+  exact (biInf_congr fun P hP ↦ EReal.coe_ennreal_injective ((hkl P hP).trans
+    (hkl P₀ hP₀).symm)).trans (biInf_const ⟨P₀, hP₀⟩)
+
+end InformationTheory
diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean
index cb2f1807..d4781064 100644
--- a/LMLExplore/MeasureTheory/Constructions/Pi.lean
+++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean
@@ -6,12 +6,14 @@ Authors: LMLExplore contributors
 module
 
 public import Mathlib.MeasureTheory.Constructions.Pi
+public import Mathlib.MeasureTheory.Measure.GiryMonad
 public import Mathlib.Probability.ConditionalProbability
 import TauCeti.MeasureTheory.Constructions.Pi
+import TauCeti.MeasureTheory.Integral.Pi
 
 /-!
-# Measures on products: laws of coordinatewise images, restricted factors, bounds by lines and
-fixed prefixes
+# Measures on products: coordinatewise images, restricted factors, bounds by lines, mixtures,
+binds and fixed prefixes
 
 Under the product measure `Measure.pi μ`, the law of a function `f` of the coordinatewise images
 `X i (y i)` is the law of `f` under the product of the laws of the `X i`. For example, the law of
@@ -25,6 +27,16 @@ Under a product of probability measures, a measurable set whose lines along one
 all have `μ i`-measure at most `c` has product measure at most `c`, by resampling the coordinate
 `i` and integrating the measures of the lines.
 
+The product of finite mixtures of measures is the mixture, over the choices of one component for
+each coordinate, of the products of the components. For measurable maps `G i` to finite
+measures, the product `Measure.pi fun i ↦ G i (x i)` depends measurably on `x`, and binding a
+product measure along it gives the product of the binds: an independent sample from `μ i` followed
+by independent draws from the `G i (x i)` is an independent sample from the mixtures. These three
+lemmas are adapted from the helpers `pi_sum_ennreal_smul`, `measurable_pi_comp` and
+`lintegral_lintegral_pi_comp` of `EValuesResearch/Results/RateVersusKL.lean` (commit `dd4072f`)
+in the paper project `RemyDegenne/evalues_research` (same author), where all the coordinates
+share one mixture or one kernel.
+
 Under a measure on `ℕ → β` that agrees almost surely with a path `ω` on the first `k` coordinates,
 a set that only depends on these coordinates is almost surely full or empty according to whether
 it contains `ω`.
@@ -40,6 +52,11 @@ it contains `ω`.
 * `MeasureTheory.Measure.pi_le_of_forall_measure_update_preimage_le`: under a product of
   probability measures, a measurable set whose lines `{t | update x i t ∈ E}` along one coordinate
   `i` all have `μ i`-measure at most `c` has product measure at most `c`.
+* `MeasureTheory.Measure.pi_sum_smul`: the product of the finite mixtures `∑ k, w i k • μ i k` is
+  `∑ σ, (∏ i, w i (σ i)) • Measure.pi fun i ↦ μ i (σ i)`.
+* `MeasureTheory.Measure.measurable_pi_comp`: `x ↦ Measure.pi fun i ↦ G i (x i)` is measurable.
+* `MeasureTheory.Measure.pi_bind_pi`: binding `Measure.pi μ` along
+  `x ↦ Measure.pi fun i ↦ G i (x i)` gives `Measure.pi fun i ↦ (μ i).bind (G i)`.
 * `MeasureTheory.setLIntegral_eq_ite_of_ae_prefix`, `MeasureTheory.measure_eq_ite_of_ae_prefix`:
   under a measure that agrees almost surely with `ω` on the first `k` coordinates, the integral
   over, and the measure of, a set that only depends on these coordinates.
@@ -104,6 +121,51 @@ lemma pi_le_of_forall_measure_update_preimage_le [DecidableEq ι] {μ : ∀ i, M
     Measure.prod_apply (measurable_update' hE)]
   exact (lintegral_mono fun x ↦ h x).trans_eq (by simp)
 
+/-! ### Products of mixtures -/
+
+/-- **Products of finite mixtures.** The product of the finite mixtures `∑ k, w i k • μ i k` is the
+mixture of the products `Measure.pi fun i ↦ μ i (σ i)` over the choices `σ` of a component for
+each coordinate, with weights `∏ i, w i (σ i)`. -/
+lemma pi_sum_smul [DecidableEq ι] {κ : ι → Type*} [∀ i, Fintype (κ i)] (w : ∀ i, κ i → ℝ≥0∞)
+    (μ : ∀ i, κ i → Measure (Ω i)) [∀ i, SigmaFinite (∑ k, w i k • μ i k)]
+    [∀ i k, SigmaFinite (μ i k)] :
+    Measure.pi (fun i ↦ ∑ k, w i k • μ i k) =
+      ∑ σ : ∀ i, κ i, (∏ i, w i (σ i)) • Measure.pi fun i ↦ μ i (σ i) := by
+  refine Measure.pi_eq fun s _ ↦ ?_
+  simp only [_root_.sum_apply, smul_apply, smul_eq_mul, Measure.pi_pi, Fintype.prod_sum,
+    ← Finset.prod_mul_distrib]
+
+/-- The product of the finite measures `G i (x i)` depends measurably on `x` when each `G i` is
+measurable. -/
+lemma measurable_pi_comp {G : ∀ i, Ω i → Measure (𝓨 i)} [∀ i x, IsFiniteMeasure (G i x)]
+    (hG : ∀ i, Measurable (G i)) :
+    Measurable fun x : ∀ i, Ω i ↦ Measure.pi fun i ↦ G i (x i) := by
+  have h_box (s : ∀ i, Set (𝓨 i)) (hs : ∀ i, MeasurableSet (s i)) :
+      Measurable fun x : ∀ i, Ω i ↦ Measure.pi (fun i ↦ G i (x i)) (Set.univ.pi s) := by
+    simp_rw [Measure.pi_pi]
+    exact Finset.measurable_prod _ fun i _ ↦
+      ((measurable_coe (hs i)).comp (hG i)).comp (measurable_pi_apply i)
+  refine Measurable.measure_of_isPiSystem generateFrom_pi.symm isPiSystem_pi ?_ ?_
+  · rintro _ ⟨s, hs, rfl⟩
+    exact h_box s fun i ↦ hs i (Set.mem_univ i)
+  · simpa using h_box (fun _ ↦ Set.univ) fun _ ↦ .univ
+
+/-- **Binding a product measure coordinatewise.** Binding `Measure.pi μ` along the products of
+the finite measures `G i (x i)` gives the product of the binds `(μ i).bind (G i)`: for probability
+measures, an independent sample of the `μ i`, followed by independent draws from the
+`G i (x i)`, is an independent sample of the mixtures. -/
+lemma pi_bind_pi {μ : ∀ i, Measure (Ω i)} [∀ i, SigmaFinite (μ i)]
+    {G : ∀ i, Ω i → Measure (𝓨 i)} [∀ i x, IsFiniteMeasure (G i x)]
+    [∀ i, SigmaFinite ((μ i).bind (G i))] (hG : ∀ i, Measurable (G i)) :
+    (Measure.pi μ).bind (fun x ↦ Measure.pi fun i ↦ G i (x i)) =
+      Measure.pi fun i ↦ (μ i).bind (G i) := by
+  refine (Measure.pi_eq fun s hs ↦ ?_).symm
+  rw [bind_apply (.univ_pi hs) (measurable_pi_comp hG).aemeasurable]
+  simp_rw [Measure.pi_pi]
+  rw [TauCeti.lintegral_fintype_prod_eq_prod μ (f := fun i x ↦ G i x (s i))
+    fun i ↦ (measurable_coe (hs i)).comp (hG i)]
+  exact Finset.prod_congr rfl fun i _ ↦ (bind_apply (hs i) (hG i).aemeasurable).symm
+
 end MeasureTheory.Measure
 
 namespace MeasureTheory
diff --git a/LMLExplore/MeasureTheory/Integral/IntervalIntegral/Periodic.lean b/LMLExplore/MeasureTheory/Integral/IntervalIntegral/Periodic.lean
new file mode 100644
index 00000000..dfa49613
--- /dev/null
+++ b/LMLExplore/MeasureTheory/Integral/IntervalIntegral/Periodic.lean
@@ -0,0 +1,34 @@
+/-
+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.Integral.IntervalIntegral.Periodic
+
+/-!
+# Lebesgue measure on the circle has no atoms
+
+Lebesgue measure on the circle `AddCircle T` gives measure `0` to every point, since the closed
+ball of radius `0` around a point has measure `min T 0`. So countable sets are null
+(`Set.Countable.measure_zero`).
+
+## Main statements
+
+* An instance `NullSingletonClass (volume : Measure (AddCircle T))`.
+-/
+
+public section
+
+open MeasureTheory
+
+namespace AddCircle
+
+variable {T : ℝ} [Fact (0 < T)]
+
+/-- Lebesgue measure on the circle `AddCircle T` has no atoms. -/
+instance : NullSingletonClass (volume : Measure (AddCircle T)) :=
+  ⟨fun x ↦ by rw [← Metric.closedBall_zero, AddCircle.volume_closedBall]; simp⟩
+
+end AddCircle