diff --git a/LMLExplore/Basic/ENNReal/BigOperators.lean b/LMLExplore/Basic/ENNReal/BigOperators.lean
index e7690159..a4dfe67c 100644
--- a/LMLExplore/Basic/ENNReal/BigOperators.lean
+++ b/LMLExplore/Basic/ENNReal/BigOperators.lean
@@ -8,7 +8,7 @@ module
 public import Mathlib.Basic.ENNReal.BigOperators
 
 /-!
-# Weighted sums of finite extended nonnegative reals
+# Weighted sums and products of extended nonnegative reals
 
 ## Main statements
 
@@ -19,6 +19,9 @@ public import Mathlib.Basic.ENNReal.BigOperators
 * `ENNReal.ofReal_sum_mul_add`: an affine form `∑ x ∈ s, f x * g x + c` with nonnegative real
   coefficients, evaluated at a point with nonnegative real coordinates and mapped to `ℝ≥0∞`, is
   the same affine form of the images in `ℝ≥0∞`.
+* `ENNReal.one_sub_prod_le_sum_one_sub`: for numbers `m i ≤ 1`,
+  `1 - ∏ i ∈ s, m i ≤ ∑ i ∈ s, (1 - m i)`, the union bound for independent events of
+  probabilities `1 - m i`.
 -/
 
 public section
@@ -47,4 +50,27 @@ lemma ofReal_sum_mul_add {ι : Type*} {s : Finset ι} {f g : ι → ℝ} {c : 
   refine congrArg (· + _) (Finset.sum_congr rfl fun x hx ↦ ?_)
   rw [ofReal_mul (hf x hx)]
 
+/-- For numbers `m i ≤ 1`, one minus their product is at most the sum of the numbers `1 - m i`:
+the union bound for independent events of probabilities `1 - m i`. -/
+lemma one_sub_prod_le_sum_one_sub {ι : Type*} (s : Finset ι) {m : ι → ℝ≥0∞}
+    (hm : ∀ i ∈ s, m i ≤ 1) :
+    1 - ∏ i ∈ s, m i ≤ ∑ i ∈ s, (1 - m i) := by
+  classical
+  induction s using Finset.induction with
+  | empty => simp
+  | insert j s hj ih =>
+    have hmj : m j ≤ 1 := hm j (Finset.mem_insert_self j s)
+    have hms : ∀ i ∈ s, m i ≤ 1 := fun i hi ↦ hm i (Finset.mem_insert_of_mem hi)
+    have hprod : ∏ i ∈ s, m i ≤ 1 := Finset.prod_le_one hms
+    rw [Finset.prod_insert hj, Finset.sum_insert hj]
+    calc 1 - m j * ∏ i ∈ s, m i ≤ (1 - m j) + (1 - ∏ i ∈ s, m i) := by
+          refine tsub_le_iff_right.2 ?_
+          calc (1 : ℝ≥0∞) = (1 - m j) + m j * ((1 - ∏ i ∈ s, m i) + ∏ i ∈ s, m i) := by
+                rw [tsub_add_cancel_of_le hprod, mul_one, tsub_add_cancel_of_le hmj]
+          _ = (1 - m j) + (m j * (1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i) := by rw [mul_add]
+          _ ≤ (1 - m j) + ((1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i) := by
+                gcongr; exact mul_le_of_le_one_left' hmj
+          _ = (1 - m j) + (1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i := (add_assoc _ _ _).symm
+    _ ≤ (1 - m j) + ∑ i ∈ s, (1 - m i) := by gcongr; exact ih hms
+
 end ENNReal
diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet/Basic.lean
similarity index 100%
rename from LMLExplore/EValues/EffectiveSet.lean
rename to LMLExplore/EValues/EffectiveSet/Basic.lean
diff --git a/LMLExplore/EValues/EffectiveSet/TotalVariation.lean b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean
new file mode 100644
index 00000000..1a6b49d8
--- /dev/null
+++ b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean
@@ -0,0 +1,288 @@
+/-
+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 LMLExplore.EValues.EffectiveSet.Basic
+public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs
+public import Mathlib.Probability.ProductMeasure
+
+import LMLExplore.MeasureTheory.Measure.TotalVariation.Basic
+import LMLExplore.MeasureTheory.Measure.TotalVariation.Pi
+import TauCeti.MeasureTheory.Measure.TotalVariation.Basic
+
+/-!
+# Nulls dense in total variation
+
+The effective null `effectiveSet S` of a null `S` is closed under setwise convergence
+(`ProbabilityTheory.mem_effectiveSet_of_measure_le_liminf`), hence in total variation. So every
+limit in total variation of members of a null of probability measures belongs to its effective
+null, and no e-variable for `S` has expectation above `1` under it. A null that is dense in
+total variation among the probability measures therefore has the e-variables of the null of all
+laws: e-variables cannot tell it apart from the null of all laws, and they have no power.
+
+* **One observation.** If every point mass `Measure.dirac x` is a limit in total variation of
+  members of `S`, the e-variables for `S` are the measurable functions bounded by `1`
+  everywhere. This applies to the laws of independent sequences, indexed by a countable type,
+  with marginals in such a null, on a space with measurable singletons: on a given sequence, the
+  marginals can be chosen to miss masses of arbitrarily small sum.
+* **Finitely many i.i.d. observations.** Total variation is subadditive over products
+  (`MeasureTheory.etvDist_pi_le_sum`), so if a probability measure `Q` is a limit in total
+  variation of members of `S`, then `Q ^ ι` is a limit of members of `S ^ ι` for every finite
+  `ι`, and lies in the effective null of the i.i.d. null `{P ^ ι | P ∈ S}`. If this holds for
+  every `Q`, an `ι`-sample function is an e-variable for the i.i.d. laws of `S` exactly when it is
+  one for the i.i.d. laws of all probability measures. Under the i.i.d. law of such a `Q`, the
+  maximal expected logarithm `maxLogGrowth Q S n` of an `n`-sample e-variable and the bipolar rate
+  `bipolarRate Q S` vanish, and a test of level `α` for the i.i.d. laws of `S` has power at most
+  `α`.
+
+The null on `ℝ` of the laws with mean `0` and a finite, positive variance
+(`ProbabilityTheory.meanZeroPosVarNull`) is the motivating instance; this is the form for
+e-variables of the theorem of Bahadur and Savage [BS56].
+
+## Main statements
+
+* `ProbabilityTheory.mem_effectiveSet_of_forall_exists_etvDist_lt`: the effective null is closed
+  in total variation.
+* `ProbabilityTheory.isEVar_iff_of_forall_exists_etvDist_dirac_lt`: if every point mass is a limit
+  in total variation of members of `S`, the e-variables for `S` are the measurable functions
+  bounded by `1`.
+* `ProbabilityTheory.isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt`: the same for the
+  laws of independent sequences with marginals in `S`.
+* `ProbabilityTheory.pi_mem_effectiveSet_of_forall_exists_etvDist_lt`: a limit `Q` in total
+  variation of members of `S` has `Q ^ ι` in the effective null of the i.i.d. null.
+* `ProbabilityTheory.isEVar_pi_iff_of_forall_exists_etvDist_lt`: a null dense in total variation
+  has, for every finite number of i.i.d. observations, the e-variables of the null of all laws.
+* `ProbabilityTheory.measure_pi_le_of_forall_exists_etvDist_lt`,
+  `ProbabilityTheory.maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt`,
+  `ProbabilityTheory.bipolarRate_eq_zero_of_forall_exists_etvDist_lt`: against such a `Q`, tests
+  have no power and evidence does not grow.
+
+## Implementation notes
+
+Membership in the effective null is derived from its closure under setwise convergence, in the
+form `ProbabilityTheory.mem_effectiveSet_of_measure_le_liminf`, which handles unbounded
+e-variables by monotone convergence. Total variation enters only through the eventwise bound
+`μ s ≤ ν s + etvDist μ ν` (`MeasureTheory.measure_le_add_etvDist`) and its subadditivity over
+products.
+
+The results are those of [EVR26, Note 22]. The proofs are rewritten from the Lean proofs in
+`EValuesResearch/Results/PowerlessNulls.lean` (commit `dd4072f`) of the paper project
+`RemyDegenne/evalues_research`, which proves the corollary directly, by common minorants and
+truncation, and the statements for one observation and for sequences through the masses
+`⨆ P ∈ S, P {x}`; here all of them go through the closure of the effective null. [BS56] is cited
+for the theorem of which this is the form for e-variables; its proofs are not used.
+
+## References
+
+* [BS56] R. R. Bahadur and L. J. Savage, *The nonexistence of certain statistical procedures in
+  nonparametric problems*, Ann. Math. Statist. 27 (1956).
+* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, Note 22, and the
+  Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026.
+-/
+
+public section
+
+open MeasureTheory Filter Set InformationTheory
+
+open scoped ENNReal Topology
+
+namespace ProbabilityTheory
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S : Set (Measure Ω)} {μ : Measure Ω}
+
+/-! ### Closure in total variation -/
+
+/-- **The effective null is closed in total variation**: a measure that is a limit in total
+variation of members of the effective null of `S` belongs to it. -/
+theorem mem_effectiveSet_of_forall_exists_etvDist_lt
+    (h : ∀ ε > 0, ∃ ν ∈ effectiveSet S, etvDist ν μ < ε) : μ ∈ effectiveSet S := by
+  -- The members of the effective null, along the filter of their distance to `μ` tending to `0`.
+  set f : effectiveSet S → ℝ≥0∞ := fun ν ↦ etvDist (ν : Measure Ω) μ
+  have : (Filter.comap f (𝓝 0)).NeBot :=
+    (ENNReal.nhds_zero_basis.comap f).neBot_iff.2 fun {ε} hε ↦
+      let ⟨ν, hν, hνμ⟩ := h ε hε
+      ⟨⟨ν, hν⟩, hνμ⟩
+  refine mem_effectiveSet_of_measure_le_liminf (l := Filter.comap f (𝓝 0)) (μs := Subtype.val)
+    (.of_forall fun ν ↦ ν.2) fun s hs ↦ ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ ?_
+  have hev : ∀ᶠ ν : effectiveSet S in Filter.comap f (𝓝 0), μ s - ε ≤ (ν : Measure Ω) s := by
+    filter_upwards [tendsto_comap.eventually (gt_mem_nhds (ENNReal.coe_pos.2 hε))] with ν hν
+    exact tsub_le_iff_right.2 (measure_le_add_of_etvDist_le hs hν.le)
+  exact tsub_le_iff_right.1 (le_liminf_of_le (by isBoundedDefault) hev)
+
+/-- A limit in total variation of members of a null `S` of measures of mass at most `1` belongs
+to the effective null of `S`. -/
+private lemma mem_effectiveSet_of_forall_exists_mem_etvDist_lt (hS : ∀ P ∈ S, P univ ≤ 1)
+    (h : ∀ ε > 0, ∃ P ∈ S, etvDist P μ < ε) : μ ∈ effectiveSet S :=
+  mem_effectiveSet_of_forall_exists_etvDist_lt fun ε hε ↦
+    let ⟨P, hP, hPμ⟩ := h ε hε
+    ⟨P, subset_effectiveSet hS hP, hPμ⟩
+
+/-! ### One observation and independent sequences -/
+
+/-- **One observation.** If every point mass is a limit in total variation of members of a null
+`S` of measures of mass at most `1` (for instance probability measures), the e-variables for `S`
+are the measurable functions bounded by `1` everywhere. -/
+theorem isEVar_iff_of_forall_exists_etvDist_dirac_lt (hS : ∀ P ∈ S, P univ ≤ 1)
+    (hS_dirac : ∀ x : Ω, ∀ ε > 0, ∃ P ∈ S, etvDist P (Measure.dirac x) < ε)
+    {X : Ω → ℝ≥0∞} :
+    IsEVar X S ↔ Measurable X ∧ ∀ x, X x ≤ 1 := by
+  refine ⟨fun hX ↦ ⟨hX.measurable, fun x ↦ ?_⟩, fun h ↦ .of_lintegral_le_measure_univ
+    (fun P hP ↦ ⟨(hS P hP).trans_lt ENNReal.one_lt_top⟩) h.1 fun P _ ↦ ?_⟩
+  · have hx : Measure.dirac x ∈ effectiveSet S :=
+      mem_effectiveSet_of_forall_exists_mem_etvDist_lt hS (hS_dirac x)
+    simpa [lintegral_dirac' x hX.measurable] using hx X hX
+  · calc ∫⁻ ω, X ω ∂P ≤ ∫⁻ _, 1 ∂P := lintegral_mono h.2
+    _ = P univ := lintegral_one
+
+variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)}
+
+/-- If every point mass is a limit in total variation of members of a null `S` of probability
+measures, so is every point mass on `ι → 𝓧`, for a countable `ι`, of laws of independent
+sequences with marginals in `S`: on the given sequence `x`, the marginals can be chosen so that
+the masses they miss have a small sum. -/
+private lemma exists_infinitePi_etvDist_dirac_lt {ι : Type*} [Countable ι]
+    [MeasurableSingletonClass 𝓧] (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hS_dirac : ∀ x : 𝓧, ∀ ε > 0, ∃ P ∈ S, etvDist P (Measure.dirac x) < ε) (x : ι → 𝓧)
+    {ε : ℝ≥0∞} (hε : 0 < ε) :
+    ∃ P ∈ Measure.infinitePi '' {P : ι → Measure 𝓧 | ∀ i, P i ∈ S},
+      etvDist P (Measure.dirac x) < ε := by
+  obtain ⟨δ, hδ0, hδ⟩ := ENNReal.exists_pos_sum_of_countable (ENNReal.half_pos hε.ne').ne' ι
+  -- For each `i`, a member of `S` that misses a mass at most `δ i` of the point `x i`.
+  have hchoose (i : ι) : ∃ P ∈ S, P {x i}ᶜ < δ i := by
+    obtain ⟨P, hP, hPx⟩ := hS_dirac (x i) (2 * δ i) (by simpa using hδ0 i)
+    have := hS P hP
+    refine ⟨P, hP, ?_⟩
+    rw [etvDist_comm, etvDist_dirac_left] at hPx
+    rw [prob_compl_eq_one_sub (measurableSet_singleton _)]
+    exact (ENNReal.mul_lt_mul_iff_right two_ne_zero ENNReal.ofNat_ne_top).1 hPx
+  choose P hPS hPx using hchoose
+  have := fun i ↦ hS _ (hPS i)
+  refine ⟨Measure.infinitePi P, ⟨P, hPS, rfl⟩, ?_⟩
+  have hcompl : Measure.infinitePi P {x}ᶜ < ε / 2 := by
+    calc Measure.infinitePi P {x}ᶜ
+    _ ≤ Measure.infinitePi P (⋃ i, Function.eval i ⁻¹' {x i}ᶜ) := by
+      refine measure_mono fun y hy ↦ ?_
+      obtain ⟨i, hi⟩ := Function.ne_iff.1 hy
+      exact mem_iUnion.2 ⟨i, hi⟩
+    _ ≤ ∑' i, Measure.infinitePi P (Function.eval i ⁻¹' {x i}ᶜ) := measure_iUnion_le _
+    _ = ∑' i, P i {x i}ᶜ := by
+      congr 1 with i
+      exact (measurePreserving_eval_infinitePi P i).measure_preimage
+        (measurableSet_singleton _).compl.nullMeasurableSet
+    _ ≤ ∑' i, (δ i : ℝ≥0∞) := by gcongr with i; exact (hPx i).le
+    _ < ε / 2 := hδ
+  rw [etvDist_comm, etvDist_dirac_left, mul_comm]
+  refine (ENNReal.lt_div_iff_mul_lt (.inl two_ne_zero) (.inl ENNReal.ofNat_ne_top)).1
+    (lt_of_le_of_lt ?_ hcompl)
+  rw [tsub_le_iff_left, ← measure_univ (μ := Measure.infinitePi P)]
+  exact measure_univ_le_add_compl _
+
+/-- **Independent sequences.** If every point mass is a limit in total variation of members of a
+null `S` of probability measures, on a space with measurable singletons, the e-variables for the
+laws of the independent sequences indexed by a countable `ι` with marginals in `S` are the
+measurable functions bounded by `1` everywhere. -/
+theorem isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt {ι : Type*} [Countable ι]
+    [MeasurableSingletonClass 𝓧] (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hS_dirac : ∀ x : 𝓧, ∀ ε > 0, ∃ P ∈ S, etvDist P (Measure.dirac x) < ε)
+    {X : (ι → 𝓧) → ℝ≥0∞} :
+    IsEVar X (Measure.infinitePi '' {P : ι → Measure 𝓧 | ∀ i, P i ∈ S}) ↔
+      Measurable X ∧ ∀ x, X x ≤ 1 := by
+  refine isEVar_iff_of_forall_exists_etvDist_dirac_lt ?_
+    fun x _ hε ↦ exists_infinitePi_etvDist_dirac_lt hS hS_dirac x hε
+  rintro _ ⟨P, hP, rfl⟩
+  have := fun i ↦ hS _ (hP i)
+  exact prob_le_one
+
+/-! ### Finitely many i.i.d. observations -/
+
+variable {ι : Type*} [Fintype ι] {Q : Measure 𝓧}
+
+/-- If `Q` is a limit in total variation of members of a null `S` of probability measures, then
+`Q ^ ι` is a limit in total variation of the products `P ^ ι` of members of `S`. -/
+private lemma exists_etvDist_pi_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    [IsProbabilityMeasure Q] (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) {ε : ℝ≥0∞} (hε : 0 < ε) :
+    ∃ P ∈ S, etvDist (Measure.pi fun _ : ι ↦ P) (Measure.pi fun _ : ι ↦ Q) < ε := by
+  obtain ⟨P, hP, hPQ⟩ := hQ (ε / Fintype.card ι)
+    (ENNReal.div_pos hε.ne' (ENNReal.natCast_ne_top _))
+  have := hS P hP
+  refine ⟨P, hP, (etvDist_pi_le_sum _ _).trans_lt ?_⟩
+  rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_comm]
+  exact (ENNReal.lt_div_iff_mul_lt (.inr (etvDist_ne_top _ _))
+    (.inl (ENNReal.natCast_ne_top _))).1 hPQ
+
+/-- **I.i.d. observations of a limit in total variation.** If a probability measure `Q` is a limit
+in total variation of members of a null `S` of probability measures, then for every finite `ι` the
+product `Q ^ ι` belongs to the effective null of the i.i.d. null `{P ^ ι | P ∈ S}`: no e-variable
+for the i.i.d. laws of `S` has expectation above `1` under the i.i.d. law of `Q`. -/
+theorem pi_mem_effectiveSet_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) :
+    Measure.pi (fun _ : ι ↦ Q) ∈ effectiveSet ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' S) := by
+  have := isProbabilityMeasure_of_forall_exists_etvDist_lt hS hQ
+  refine mem_effectiveSet_of_forall_exists_mem_etvDist_lt ?_ fun ε hε ↦ ?_
+  · rintro _ ⟨P, hP, rfl⟩
+    have := hS P hP
+    simp
+  · obtain ⟨P, hP, hPQ⟩ := exists_etvDist_pi_lt (ι := ι) hS hQ hε
+    exact ⟨_, ⟨P, hP, rfl⟩, hPQ⟩
+
+/-- **A null dense in total variation has the e-variables of all laws.** If every probability
+measure is a limit in total variation of members of a null `S` of probability measures, then for
+every finite set `ι` of i.i.d. observations, a function is an e-variable for the products `P ^ ι`
+of the members of `S` exactly when it is one for the products of all probability measures. -/
+theorem isEVar_pi_iff_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hdense : ∀ Q : Measure 𝓧, IsProbabilityMeasure Q → ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε)
+    {X : (ι → 𝓧) → ℝ≥0∞} :
+    IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' S) ↔
+      IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' {P | IsProbabilityMeasure P}) := by
+  refine ⟨fun hX ↦ .of_lintegral_le_one ?_ hX.measurable ?_,
+    fun hX ↦ hX.anti_set (image_mono fun P hP ↦ hS P hP)⟩
+  · rintro _ ⟨Q, hQ, rfl⟩
+    have : IsProbabilityMeasure Q := hQ
+    infer_instance
+  · rintro _ ⟨Q, hQ, rfl⟩
+    have : IsProbabilityMeasure Q := hQ
+    exact pi_mem_effectiveSet_of_forall_exists_etvDist_lt hS (hdense Q hQ) X hX
+
+/-- **No power against a limit in total variation.** If a probability measure `Q` is a limit in
+total variation of members of a null `S` of probability measures, a measurable set of `ι`
+observations with probability at most `α` under the i.i.d. law of every member of `S` has
+probability at most `α` under the i.i.d. law of `Q`. -/
+theorem measure_pi_le_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) {R : Set (ι → 𝓧)} (hR : MeasurableSet R)
+    {α : ℝ≥0∞} (hα : ∀ P ∈ S, Measure.pi (fun _ : ι ↦ P) R ≤ α) :
+    Measure.pi (fun _ : ι ↦ Q) R ≤ α := by
+  have := isProbabilityMeasure_of_forall_exists_etvDist_lt hS hQ
+  refine ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ ?_
+  obtain ⟨P, hP, hPQ⟩ := exists_etvDist_pi_lt (ι := ι) hS hQ (ENNReal.coe_pos.2 hε)
+  exact (measure_le_add_of_etvDist_le hR hPQ.le).trans (add_le_add (hα P hP) le_rfl)
+
+/-- **No growth against a limit in total variation.** If a probability measure `Q` is a limit in
+total variation of members of a null `S` of probability measures, the maximal expected logarithm
+under `Q ^ n` of an `n`-sample e-variable for the i.i.d. laws of `S` is `0`. -/
+theorem maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) (n : ℕ) :
+    maxLogGrowth Q S n = 0 := by
+  have := isProbabilityMeasure_of_forall_exists_etvDist_lt hS hQ
+  refine le_antisymm ?_ (maxLogGrowth_nonneg _ _ _)
+  rw [maxLogGrowth_def]
+  refine (maxUtility_le_klIntegral_of_mem_effectiveSet ?_
+    (pi_mem_effectiveSet_of_forall_exists_etvDist_lt hS hQ)).trans_eq ?_
+  · rintro _ ⟨P, hP, rfl⟩
+    have := hS P hP
+    infer_instance
+  · rw [klIntegral_eq_klDiv rfl, klDiv_self, EReal.coe_ennreal_zero]
+
+/-- **The bipolar rate against a limit in total variation is zero.** If a probability measure `Q`
+is a limit in total variation of members of a null `S` of probability measures, the optimal growth
+rate `bipolarRate Q S` of the evidence against the i.i.d. laws of `S` under the i.i.d. law of `Q`
+is `0`. -/
+theorem bipolarRate_eq_zero_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) :
+    bipolarRate Q S = 0 := by
+  simp [bipolarRate_def, maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt hS hQ]
+
+end ProbabilityTheory
diff --git a/LMLExplore/EValues/MeanZeroNull.lean b/LMLExplore/EValues/MeanZeroNull.lean
new file mode 100644
index 00000000..bb830708
--- /dev/null
+++ b/LMLExplore/EValues/MeanZeroNull.lean
@@ -0,0 +1,291 @@
+/-
+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.EffectiveSet.TotalVariation
+public import LMLExplore.EValues.EProcess
+public import Mathlib.Probability.Moments.Variance
+
+/-!
+# The mean-zero null: e-variables without power
+
+The null `meanZeroPosVarNull` of the laws on `ℝ` with mean `0` and a finite, positive variance
+is dense in total variation among the probability measures on `ℝ`: a law `Q` is approximated by
+`Q` restricted to a large interval and scaled by a factor below `1`, completed by two atoms that
+restore the mean `0` and make the variance positive. So the results of
+`LMLExplore.EValues.EffectiveSet.TotalVariation` apply, and the null cannot be tested with
+e-variables against i.i.d. alternatives, the form for e-variables of the theorem of Bahadur and
+Savage [BS56]:
+
+* for every finite number of i.i.d. observations, its e-variables are those of the null of all
+  laws on `ℝ`; for one observation, they are the measurable functions bounded by `1`
+  everywhere;
+* against the i.i.d. law of every `Q`, the maximal expected logarithm of an `n`-sample e-variable
+  and the bipolar rate vanish, and a test of level `α` has power at most `α`;
+* every e-process, for any filtration, for the laws of the independent sequences with marginals in
+  the null is at most `1` at every time and on every sequence.
+
+## Main definitions
+
+* `ProbabilityTheory.meanZeroPosVarNull`: the laws on `ℝ` with mean `0` and finite, positive
+  variance.
+
+## Main statements
+
+* `ProbabilityTheory.exists_mem_meanZeroPosVarNull_etvDist_lt`: the null is dense in total
+  variation.
+* `ProbabilityTheory.isEVar_pi_meanZeroPosVarNull_iff`: its `ι`-sample e-variables are those of
+  the i.i.d. laws of all probability measures.
+* `ProbabilityTheory.isEVar_meanZeroPosVarNull_iff`: its one-observation e-variables are the
+  measurable functions bounded by `1`.
+* `ProbabilityTheory.maxLogGrowth_meanZeroPosVarNull`,
+  `ProbabilityTheory.bipolarRate_meanZeroPosVarNull`,
+  `ProbabilityTheory.measure_pi_le_of_forall_meanZeroPosVarNull`: no growth and no power against
+  i.i.d. alternatives.
+* `ProbabilityTheory.le_one_of_isEProcess_infinitePi_meanZeroPosVarNull`: e-processes for the laws
+  of independent sequences with marginals in the null are at most `1`.
+
+## Implementation notes
+
+The density of the null, and its consequences, are the results of [EVR26, Note 22]. The
+construction of the approximating laws is adapted from the Lean proof in
+`EValuesResearch/Results/PowerlessNulls.lean` (commit `dd4072f`) of the paper project
+`RemyDegenne/evalues_research`. [BS56] is cited for the theorem of which this is the form for
+e-variables; its proofs are not used.
+
+## References
+
+* [BS56] R. R. Bahadur and L. J. Savage, *The nonexistence of certain statistical procedures in
+  nonparametric problems*, Ann. Math. Statist. 27 (1956).
+* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, Note 22, and the
+  Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026.
+-/
+
+public section
+
+open MeasureTheory Filter Set
+
+open scoped ENNReal Topology
+
+namespace ProbabilityTheory
+
+/-- The laws on `ℝ` with mean `0` and a finite, positive variance: the probability measures `μ`
+under which the identity is square integrable, with `∫ x ∂μ = 0` and `0 < variance id μ`. -/
+def meanZeroPosVarNull : Set (Measure ℝ) :=
+  {μ | IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧ ∫ x, x ∂μ = 0 ∧ 0 < variance id μ}
+
+/-- Membership in `meanZeroPosVarNull`. -/
+lemma mem_meanZeroPosVarNull_iff {μ : Measure ℝ} :
+    μ ∈ meanZeroPosVarNull ↔
+      IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧ ∫ x, x ∂μ = 0 ∧ 0 < variance id μ :=
+  Iff.rfl
+
+/-- The members of `meanZeroPosVarNull` are probability measures. -/
+lemma isProbabilityMeasure_of_mem_meanZeroPosVarNull {μ : Measure ℝ} (hμ : μ ∈ meanZeroPosVarNull) :
+    IsProbabilityMeasure μ :=
+  hμ.1
+
+/-! ### Density in total variation -/
+
+/-- Adding two atoms of the same mass `c ≠ 0` at `z - 1` and `z + 1` to a measure `ν` gives a
+measure under which the identity is not almost everywhere `0`. -/
+private lemma not_ae_eq_zero_add_smul_dirac (ν : Measure ℝ) {c : ℝ≥0∞} (hc : c ≠ 0) (z : ℝ) :
+    ¬ ∀ᵐ x ∂(ν + c • (Measure.dirac (z - 1) + Measure.dirac (z + 1))), x = 0 := by
+  intro h
+  have h₁ := (Measure.ae_ennreal_smul_measure_iff hc).1 (ae_add_measure_iff.1 h).2
+  rw [ae_add_measure_iff, ae_dirac_iff (measurableSet_singleton 0),
+    ae_dirac_iff (measurableSet_singleton 0)] at h₁
+  have h₂ : z - 1 = 0 := h₁.1
+  have h₃ : z + 1 = 0 := h₁.2
+  linarith
+
+/-- The identity is integrable under two atoms at `z - 1` and `z + 1`. -/
+private lemma integrable_id_dirac_add_dirac (z : ℝ) :
+    Integrable (fun x : ℝ ↦ x) (Measure.dirac (z - 1) + Measure.dirac (z + 1)) :=
+  (integrable_dirac (by simp)).add_measure (integrable_dirac (by simp))
+
+/-- The mean of two atoms at `z - 1` and `z + 1` is `2 * z`. -/
+private lemma integral_id_dirac_add_dirac (z : ℝ) :
+    ∫ x, x ∂(Measure.dirac (z - 1) + Measure.dirac (z + 1)) = 2 * z := by
+  rw [integral_add_measure (integrable_dirac (by simp)) (integrable_dirac (by simp)),
+    integral_dirac, integral_dirac]
+  ring
+
+/-- **Completion to a law with mean zero.** A finite measure on `ℝ` of mass less than `1` carried
+by a bounded interval is below a member of `meanZeroPosVarNull`: add two atoms of mass
+`(1 - ν univ) / 2` at `z - 1` and `z + 1`, for the `z` that makes the mean `0`. -/
+private lemma exists_mem_meanZeroPosVarNull_le (ν : Measure ℝ) [IsFiniteMeasure ν]
+    (hν : ν univ < 1) {M : ℝ} (hM : ∀ᵐ x ∂ν, |x| ≤ M) : ∃ P ∈ meanZeroPosVarNull, ν ≤ P := by
+  set b := ν.real univ with hb_def
+  have hb1 : b < 1 := ENNReal.toReal_lt_of_lt_ofReal (by simpa using hν)
+  set z := -(∫ x, x ∂ν) / (1 - b) with hz
+  set c := ENNReal.ofReal ((1 - b) / 2) with hc
+  have hc0 : c ≠ 0 := by rw [hc, ne_eq, ENNReal.ofReal_eq_zero, not_le]; linarith
+  have hct : c.toReal = (1 - b) / 2 := ENNReal.toReal_ofReal (by linarith)
+  set D := Measure.dirac (z - 1) + Measure.dirac (z + 1) with hD
+  have : IsFiniteMeasure (c • D) := Measure.smul_finite D ENNReal.ofReal_ne_top
+  set P := ν + c • D with hP
+  have hPb : ∀ᵐ x ∂P, |x| ≤ max M (|z| + 1) := by
+    rw [hP, ae_add_measure_iff, hD]
+    refine ⟨hM.mono fun x hx ↦ hx.trans (le_max_left _ _), Measure.ae_smul_measure ?_ c⟩
+    rw [ae_add_measure_iff, ae_dirac_eq, ae_dirac_eq, eventually_pure, eventually_pure]
+    constructor <;> exact (abs_le.2 ⟨by linarith [neg_abs_le z], by linarith [le_abs_self z]⟩).trans
+      (le_max_right _ _)
+  have hint {μ : Measure ℝ} [IsFiniteMeasure μ] {K : ℝ} (hK : ∀ᵐ x ∂μ, |x| ≤ K) :
+      Integrable (fun x : ℝ ↦ x) μ :=
+    Integrable.of_bound measurable_id.aestronglyMeasurable K (by simpa using hK)
+  have hPprob : IsProbabilityMeasure P := by
+    have hDuniv : D.real univ = 2 := by
+      rw [measureReal_add_apply]
+      norm_num
+    rw [isProbabilityMeasure_iff_real]
+    calc P.real univ = b + c.toReal * D.real univ := by
+          rw [measureReal_add_apply]
+          simp [b]
+    _ = 1 := by rw [hct, hDuniv]; ring
+  have hmean : ∫ x, x ∂P = 0 := by
+    have hDint : Integrable (fun x : ℝ ↦ x) (c • D) :=
+      (integrable_id_dirac_add_dirac z).smul_measure ENNReal.ofReal_ne_top
+    calc ∫ x, x ∂P = ∫ x, x ∂ν + c.toReal * ∫ x, x ∂D := by
+          rw [integral_add_measure (hint hM) hDint, integral_smul_measure, smul_eq_mul]
+    _ = ∫ x, x ∂ν + (1 - b) / 2 * (2 * z) := by rw [hct, integral_id_dirac_add_dirac]
+    _ = 0 := by
+          rw [hz]
+          field_simp
+          ring
+  have hmem : MemLp id 2 P := MemLp.of_bound measurable_id.aestronglyMeasurable (max M (|z| + 1))
+    (hPb.mono fun x hx ↦ by simpa [Real.norm_eq_abs] using hx)
+  have hvar : 0 < variance id P := by
+    refine ENNReal.toReal_pos (fun h0 ↦ not_ae_eq_zero_add_smul_dirac ν hc0 z ?_)
+      hmem.evariance_lt_top.ne
+    have h := (evariance_eq_zero_iff measurable_id.aemeasurable).1 h0
+    simp only [id_eq, hmean] at h
+    exact h
+  exact ⟨P, ⟨hPprob, hmem, hmean, hvar⟩, Measure.le_add_right le_rfl⟩
+
+/-- A probability measure on `ℝ` gives a mass more than `1 - δ` to some interval `[-M, M]`. -/
+private lemma exists_one_sub_lt_measure_Icc (Q : Measure ℝ) [IsProbabilityMeasure Q] {δ : ℝ≥0∞}
+    (hδ : δ ≠ 0) : ∃ M : ℕ, 1 - δ < Q (Icc (-(M : ℝ)) M) := by
+  have hU : (⋃ M : ℕ, Icc (-(M : ℝ)) M) = univ :=
+    eq_univ_of_forall fun x ↦ mem_iUnion.2 ⟨⌈|x|⌉₊, abs_le.1 (Nat.le_ceil _)⟩
+  have htend := tendsto_measure_iUnion_atTop (μ := Q) (s := fun M : ℕ ↦ Icc (-(M : ℝ)) M)
+    fun m n hmn ↦ Icc_subset_Icc (by simpa using hmn) (by simpa using hmn)
+  rw [hU, measure_univ] at htend
+  exact (htend.eventually (lt_mem_nhds
+    (ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero hδ))).exists
+
+/-- **The null `meanZeroPosVarNull` is dense in total variation**: every probability measure on
+`ℝ` is a limit in total variation of laws with mean `0` and a finite, positive variance. -/
+theorem exists_mem_meanZeroPosVarNull_etvDist_lt (Q : Measure ℝ) [IsProbabilityMeasure Q]
+    {ε : ℝ≥0∞} (hε : 0 < ε) : ∃ P ∈ meanZeroPosVarNull, etvDist P Q < ε := by
+  -- `Q` restricted to `[-M, M]` and scaled by `1 - η` misses a mass at most `2 δ` of `Q`, and
+  -- the completion `P` of it is at distance at most twice that mass.
+  obtain ⟨δ', hδ'0, hδ'⟩ := ENNReal.exists_nnreal_pos_mul_lt (b := ε) (a := 4) (by norm_num)
+    hε.ne'
+  set δ : ℝ≥0∞ := (δ' : ℝ≥0∞)
+  have hδ0 : δ ≠ 0 := ENNReal.coe_ne_zero.2 hδ'0.ne'
+  have hδ2 : 2 * (2 * δ) < ε := by
+    calc 2 * (2 * δ) = δ * 4 := by ring
+    _ < ε := hδ'
+  obtain ⟨M, hM⟩ := exists_one_sub_lt_measure_Icc Q hδ0
+  set I := Icc (-(M : ℝ)) M
+  set η := min δ 2⁻¹
+  have hη0 : η ≠ 0 := by simp [η, hδ0]
+  have hη1 : η ≤ 1 := ((min_le_right _ _).trans_lt ENNReal.one_half_lt_one).le
+  set ν := (1 - η) • Q.restrict I
+  have hνQ : ν ≤ Q := fun s ↦ by
+    rw [smul_apply, smul_eq_mul]
+    exact (mul_le_of_le_one_left' tsub_le_self).trans (Measure.restrict_le_self s)
+  have hνuniv : ν univ = (1 - η) * Q I := by simp [ν]
+  have : IsFiniteMeasure ν := isFiniteMeasure_of_le Q hνQ
+  have hν1 : ν univ < 1 := by
+    rw [hνuniv]
+    calc (1 - η) * Q I ≤ 1 - η := mul_le_of_le_one_right' prob_le_one
+    _ < 1 := ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero hη0
+  have hνM : ∀ᵐ x ∂ν, |x| ≤ (M : ℝ) :=
+    Measure.ae_smul_measure
+      (ae_restrict_of_forall_mem measurableSet_Icc fun x hx ↦ abs_le.2 (mem_Icc.1 hx)) _
+  obtain ⟨P, hP, hνP⟩ := exists_mem_meanZeroPosVarNull_le ν hν1 hνM
+  have := hP.1
+  -- `ν` misses a mass less than `2 δ` of `Q`.
+  have hmiss : 1 - ν univ ≤ 2 * δ := by
+    refine tsub_le_iff_left.2 ?_
+    calc (1 : ℝ≥0∞) ≤ Q I + δ := tsub_le_iff_right.1 hM.le
+    _ = (1 - η) * Q I + η * Q I + δ := by rw [← add_mul, tsub_add_cancel_of_le hη1, one_mul]
+    _ ≤ ν univ + 2 * δ := by
+      rw [hνuniv, two_mul, add_assoc]
+      gcongr
+      exact (mul_le_of_le_one_right' prob_le_one).trans (min_le_left _ _)
+  refine ⟨P, hP, lt_of_le_of_lt ?_ hδ2⟩
+  calc etvDist P Q ≤ etvDist P ν + etvDist ν Q := etvDist_triangle _ _ _
+  _ = (1 - ν univ) + (1 - ν univ) := by
+    rw [etvDist_of_ge hνP, etvDist_of_le hνQ, measure_univ (μ := P), measure_univ (μ := Q)]
+  _ ≤ 2 * (2 * δ) := by rw [← two_mul]; gcongr
+
+/-! ### E-variables -/
+
+/-- **Same e-variables as for all laws.** For every finite set `ι` of i.i.d. real observations, a
+function is an e-variable for the i.i.d. laws of the mean-zero null exactly when it is one for the
+i.i.d. laws of all probability measures on `ℝ`. -/
+theorem isEVar_pi_meanZeroPosVarNull_iff {ι : Type*} [Fintype ι] {X : (ι → ℝ) → ℝ≥0∞} :
+    IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' meanZeroPosVarNull) ↔
+      IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' {P | IsProbabilityMeasure P}) :=
+  isEVar_pi_iff_of_forall_exists_etvDist_lt (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull)
+    fun Q _ _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt Q hε
+
+/-- **One observation.** The e-variables for the laws on `ℝ` with mean `0` and a finite, positive
+variance are the measurable functions bounded by `1` everywhere. -/
+theorem isEVar_meanZeroPosVarNull_iff {X : ℝ → ℝ≥0∞} :
+    IsEVar X meanZeroPosVarNull ↔ Measurable X ∧ ∀ x, X x ≤ 1 :=
+  isEVar_iff_of_forall_exists_etvDist_dirac_lt
+    (fun _ hP ↦ (isProbabilityMeasure_of_mem_meanZeroPosVarNull hP).measure_univ.le)
+    fun x _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt (Measure.dirac x) hε
+
+/-! ### No power against i.i.d. alternatives -/
+
+/-- **No growth.** For every law `Q` on `ℝ` and every number `n` of observations, the maximal
+expected logarithm under `Q ^ n` of an `n`-sample e-variable for the i.i.d. laws of the mean-zero
+null is `0`. -/
+theorem maxLogGrowth_meanZeroPosVarNull (Q : Measure ℝ) [IsProbabilityMeasure Q] (n : ℕ) :
+    maxLogGrowth Q meanZeroPosVarNull n = 0 :=
+  maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt
+    (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull)
+    (fun _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt Q hε) n
+
+/-- **The bipolar rate is zero.** For every law `Q` on `ℝ`, the optimal growth rate of the
+evidence against the i.i.d. laws of the mean-zero null under the i.i.d. law of `Q` is `0`. -/
+theorem bipolarRate_meanZeroPosVarNull (Q : Measure ℝ) [IsProbabilityMeasure Q] :
+    bipolarRate Q meanZeroPosVarNull = 0 :=
+  bipolarRate_eq_zero_of_forall_exists_etvDist_lt
+    (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull)
+    fun _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt Q hε
+
+/-- **No power.** A measurable set of `ι` real observations with probability at most `α` under
+the i.i.d. law of every member of the mean-zero null has probability at most `α` under the
+i.i.d. law of every probability measure on `ℝ`. -/
+theorem measure_pi_le_of_forall_meanZeroPosVarNull {ι : Type*} [Fintype ι] {R : Set (ι → ℝ)}
+    (hR : MeasurableSet R) {α : ℝ≥0∞}
+    (hα : ∀ P ∈ meanZeroPosVarNull, Measure.pi (fun _ : ι ↦ P) R ≤ α) (Q : Measure ℝ)
+    [IsProbabilityMeasure Q] :
+    Measure.pi (fun _ : ι ↦ Q) R ≤ α :=
+  measure_pi_le_of_forall_exists_etvDist_lt (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull)
+    (fun _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt Q hε) hR hα
+
+/-- **Independent sequences.** Every e-process, for any filtration, for the laws of the
+independent sequences of real observations whose marginals have mean `0` and a finite, positive
+variance is at most `1` at every time and on every sequence. -/
+theorem le_one_of_isEProcess_infinitePi_meanZeroPosVarNull
+    {ℱ : Filtration ℕ (MeasurableSpace.pi : MeasurableSpace (ℕ → ℝ))} {E : ℕ → (ℕ → ℝ) → ℝ≥0∞}
+    (hE : IsEProcess E ℱ
+      (Measure.infinitePi '' {P : ℕ → Measure ℝ | ∀ n, P n ∈ meanZeroPosVarNull}))
+    (n : ℕ) (x : ℕ → ℝ) :
+    E n x ≤ 1 :=
+  ((isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt
+    (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull)
+    (fun y _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt (Measure.dirac y) hε)).1
+      (hE.isEVar n)).2 x
+
+end ProbabilityTheory
diff --git a/LMLExplore/EValues/Numeraire.lean b/LMLExplore/EValues/Numeraire.lean
index 3d4ee92b..a3982e7b 100644
--- a/LMLExplore/EValues/Numeraire.lean
+++ b/LMLExplore/EValues/Numeraire.lean
@@ -6,7 +6,7 @@ Authors: LMLExplore contributors
 module
 
 public import Statlib.EValues.RIPr
-public import LMLExplore.EValues.EffectiveSet
+public import LMLExplore.EValues.EffectiveSet.Basic
 public import LMLExplore.EValues.EVariable
 public import LMLExplore.MeasureTheory.Measure.AbsolutelyContinuousSet
 public import LMLExplore.MeasureTheory.Measure.WithDensity
diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean
index cb2f1807..f215ba63 100644
--- a/LMLExplore/MeasureTheory/Constructions/Pi.lean
+++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean
@@ -7,11 +7,14 @@ module
 
 public import Mathlib.MeasureTheory.Constructions.Pi
 public import Mathlib.Probability.ConditionalProbability
+import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RNDerivProd
 import TauCeti.MeasureTheory.Constructions.Pi
 
 /-!
-# Measures on products: laws of coordinatewise images, restricted factors, bounds by lines and
-fixed prefixes
+# Measures on products: monotonicity, laws of coordinatewise images, restricted factors, bounds
+by lines and fixed prefixes
+
+The product of finite measures is monotone in its factors.
 
 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
@@ -31,6 +34,8 @@ it contains `ω`.
 
 ## Main statements
 
+* `MeasureTheory.Measure.pi_mono`: if `μ i ≤ ν i` for every `i`, with every `ν i` finite, then
+  `Measure.pi μ ≤ Measure.pi ν`.
 * `MeasureTheory.Measure.map_pi_comp_eq_map_pi_map`:
   `(Measure.pi μ).map (fun y ↦ f fun i ↦ X i (y i)) = (Measure.pi fun i ↦ (μ i).map (X i)).map f`.
 * `MeasureTheory.Measure.pi_restrict_eq_pow_smul_pi_cond`:
@@ -54,6 +59,20 @@ namespace MeasureTheory.Measure
 variable {ι : Type*} [Fintype ι] {Ω 𝓨 : ι → Type*} {mΩ : ∀ i, MeasurableSpace (Ω i)}
   [∀ i, MeasurableSpace (𝓨 i)] {β : Type*} {mβ : MeasurableSpace β}
 
+/-- **Monotonicity of the product measure.** The product of finite measures is monotone in its
+factors: if `μ i ≤ ν i` for every `i`, then `Measure.pi μ ≤ Measure.pi ν`. -/
+@[gcongr]
+lemma pi_mono {μ ν : ∀ i, Measure (Ω i)} [∀ i, IsFiniteMeasure (ν i)] (h : ∀ i, μ i ≤ ν i) :
+    Measure.pi μ ≤ Measure.pi ν := by
+  have (i : ι) : IsFiniteMeasure (μ i) := isFiniteMeasure_of_le (ν i) (h i)
+  rw [pi_eq_withDensity_prod_rnDeriv fun i ↦ absolutelyContinuous_of_le (h i)]
+  calc (Measure.pi ν).withDensity (fun x ↦ ∏ i, (μ i).rnDeriv (ν i) (x i))
+  _ ≤ (Measure.pi ν).withDensity 1 := by
+    refine withDensity_mono ?_
+    filter_upwards [ae_le_pi fun i ↦ rnDeriv_le_one_of_le (h i)] with x hx
+    exact Finset.prod_le_one fun i _ ↦ hx i
+  _ = Measure.pi ν := withDensity_one
+
 /-- The law under a product measure 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`. -/
 lemma map_pi_comp_eq_map_pi_map {μ : ∀ i, Measure (Ω i)} {X : ∀ i, Ω i → 𝓨 i}
diff --git a/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean b/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean
index c0baff2c..6a197ce9 100644
--- a/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean
+++ b/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean
@@ -10,6 +10,7 @@ public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs
 
 import Mathlib.MeasureTheory.Integral.Bochner.Set
 import Mathlib.MeasureTheory.Integral.IntegrableOn
+import Mathlib.MeasureTheory.Measure.TotalVariation.Basic
 import Mathlib.MeasureTheory.VectorMeasure.Integral
 import LMLExplore.Order.ConditionallyCompleteLattice.Group
 import TauCeti.MeasureTheory.Measure.TotalVariation.Basic
@@ -48,6 +49,12 @@ contraction of the oscillation of functions by a Markov kernel (Dobrushin's coef
   `|∫ f dμ - ∫ f dν| ≤ (b - a) / 2 * tvDist μ ν`, and
   `MeasureTheory.abs_integral_sub_integral_le_mul_tvDist_of_forall_sub_le` its form for `f` whose
   values differ by at most `c`.
+* `MeasureTheory.measure_le_add_etvDist`: `μ s ≤ ν s + etvDist μ ν` for every measurable `s`, and
+  `MeasureTheory.measure_le_add_of_etvDist_le` its form `μ s ≤ ν s + ε` when `etvDist ν μ ≤ ε`.
+* `MeasureTheory.isProbabilityMeasure_of_forall_exists_etvDist_lt`: a limit in total variation of
+  probability measures is a probability measure.
+* `MeasureTheory.exists_le_le_add_etvDist`: two finite measures have a common minorant `ρ` with
+  `μ univ + ν univ = 2 * ρ univ + etvDist μ ν`.
 * `MeasureTheory.abs_measureReal_sub_measureReal_le_tvDist_div_two`,
   `MeasureTheory.tvDist_le_two_mul_of_forall_measureReal_le_add`: for measures of the same mass,
   the total variation distance bounds the difference of the masses of every event, and eventwise
@@ -75,7 +82,7 @@ on the masses.
 public section
 
 open Set
-open scoped NNReal
+open scoped ENNReal NNReal
 
 namespace MeasureTheory
 
@@ -160,6 +167,62 @@ theorem abs_integral_sub_integral_le_mul_tvDist_of_forall_sub_le [IsFiniteMeasur
 
 /-! ### Eventwise bounds -/
 
+/-- **Events of measures close in total variation**, in `ℝ≥0∞`: every measurable event `s`
+satisfies `μ s ≤ ν s + etvDist μ ν`. No finiteness is assumed: the distance is `∞` unless both
+measures are finite. -/
+theorem measure_le_add_etvDist (μ ν : Measure 𝓧) {s : Set 𝓧} (hs : MeasurableSet s) :
+    μ s ≤ ν s + etvDist μ ν := by
+  by_cases h : IsFiniteMeasure μ ∧ IsFiniteMeasure ν
+  · obtain ⟨_, _⟩ := h
+    rw [etvDist_eq_iSup_sub_add_iSup_sub]
+    calc μ s ≤ ν s + (μ s - ν s) := le_add_tsub
+    _ ≤ _ := by
+      gcongr
+      exact le_add_right (le_iSup₂ (f := fun A (_ : MeasurableSet A) ↦ μ A - ν A) s hs)
+  · simp [etvDist_of_not_isFiniteMeasure h]
+
+/-- **Events of measures within `ε` in total variation**: if `etvDist ν μ ≤ ε`, every measurable
+event `s` satisfies `μ s ≤ ν s + ε`. -/
+theorem measure_le_add_of_etvDist_le {μ ν : Measure 𝓧} {s : Set 𝓧} {ε : ℝ≥0∞}
+    (hs : MeasurableSet s) (h : etvDist ν μ ≤ ε) : μ s ≤ ν s + ε :=
+  (measure_le_add_etvDist μ ν hs).trans (add_le_add le_rfl ((etvDist_comm μ ν).trans_le h))
+
+/-- A limit in total variation of probability measures is a probability measure. -/
+theorem isProbabilityMeasure_of_forall_exists_etvDist_lt {S : Set (Measure 𝓧)} {Q : Measure 𝓧}
+    (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) :
+    IsProbabilityMeasure Q := by
+  have h (ε : ℝ≥0) (hε : 0 < ε) : Q univ ≤ 1 + ε ∧ 1 ≤ Q univ + ε := by
+    obtain ⟨P, hP, hPQ⟩ := hQ ε (ENNReal.coe_pos.2 hε)
+    have := hS P hP
+    constructor
+    · simpa using measure_le_add_of_etvDist_le .univ hPQ.le
+    · simpa using measure_le_add_of_etvDist_le (μ := P) .univ ((etvDist_comm Q P).trans_le hPQ.le)
+  exact ⟨le_antisymm (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).1)
+    (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).2)⟩
+
+/-- **A common minorant of two finite measures.** On a Hahn decomposition `s`, the measure
+`μ.restrict s + ν.restrict sᶜ` is below `μ` and `ν`, and its mass is the mean of the masses of `μ`
+and `ν` minus half their total variation distance. -/
+theorem exists_le_le_add_etvDist (μ ν : Measure 𝓧) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
+    ∃ ρ : Measure 𝓧, ρ ≤ μ ∧ ρ ≤ ν ∧ μ univ + ν univ = 2 * ρ univ + etvDist μ ν := by
+  obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν
+  refine ⟨μ.restrict s + ν.restrict sᶜ, ?_, ?_, ?_⟩
+  · calc μ.restrict s + ν.restrict sᶜ ≤ μ.restrict s + μ.restrict sᶜ :=
+          add_le_add le_rfl hs.ge_on_compl
+    _ = μ := Measure.restrict_add_restrict_compl hs.measurableSet
+  · calc μ.restrict s + ν.restrict sᶜ ≤ ν.restrict s + ν.restrict sᶜ :=
+          add_le_add hs.le_on le_rfl
+    _ = ν := Measure.restrict_add_restrict_compl hs.measurableSet
+  · have h₁ : μ s ≤ ν s := by simpa using hs.le_on univ
+    have h₂ : ν sᶜ ≤ μ sᶜ := by simpa using hs.ge_on_compl univ
+    calc μ univ + ν univ = (μ s + μ sᶜ) + (ν s + ν sᶜ) := by
+          rw [measure_add_measure_compl hs.measurableSet,
+            measure_add_measure_compl hs.measurableSet]
+    _ = (μ s + (ν sᶜ + (μ sᶜ - ν sᶜ))) + ((μ s + (ν s - μ s)) + ν sᶜ) := by
+          rw [add_tsub_cancel_of_le h₁, add_tsub_cancel_of_le h₂]
+    _ = 2 * (μ s + ν sᶜ) + ((ν s - μ s) + (μ sᶜ - ν sᶜ)) := by ring
+    _ = 2 * (μ.restrict s + ν.restrict sᶜ) univ + etvDist μ ν := by simp [hs.etvDist_eq]
+
 /-- **Events of measures of the same mass close in total variation**: for finite measures `μ`
 and `ν` of the same mass, every measurable event `s` satisfies
 `|μ s - ν s| ≤ tvDist μ ν / 2`. -/
diff --git a/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean b/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean
new file mode 100644
index 00000000..fec0bf60
--- /dev/null
+++ b/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean
@@ -0,0 +1,86 @@
+/-
+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.Constructions.Pi
+public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs
+
+import LMLExplore.Basic.ENNReal.BigOperators
+import LMLExplore.MeasureTheory.Constructions.Pi
+import LMLExplore.MeasureTheory.Measure.TotalVariation.Basic
+
+/-!
+# Total variation distance between product measures
+
+The total variation distance between two finite products of probability measures is at most the
+sum of the distances between the factors:
+
+```text
+etvDist (Measure.pi μ) (Measure.pi ν) ≤ ∑ i, etvDist (μ i) (ν i).
+```
+
+In particular `n` independent observations of `μ` and of `ν` are at distance at most
+`n * etvDist μ ν`, so that the `n`-fold products of a sequence of laws that converges to `ν` in
+total variation converge to the `n`-fold product of `ν`.
+
+## Main statements
+
+* `MeasureTheory.etvDist_pi_le_sum`: the total variation distance between products of
+  probability measures is at most the sum of the distances between the factors.
+
+## Implementation notes
+
+The proof goes through a common minorant of two finite measures
+(`MeasureTheory.exists_le_le_add_etvDist`): on a Hahn decomposition `s` of `(μ, ν)`, the measure
+`ρ = μ.restrict s + ν.restrict sᶜ` is below `μ` and `ν`, with
+`μ univ + ν univ = 2 * ρ univ + etvDist μ ν`. For probability measures the product of
+the minorants is below both products (`MeasureTheory.Measure.pi_mono`) and has mass
+`∏ i, ρ i univ`, so the distance between the products is at most
+`2 * (1 - ∏ i, ρ i univ) ≤ ∑ i, 2 * (1 - ρ i univ)` (`ENNReal.one_sub_prod_le_sum_one_sub`).
+
+The argument, common minorants and the bound `1 - ∏ i, m i ≤ ∑ i, (1 - m i)`, is adapted from
+the Lean proof of [EVR26, Note 22] in `EValuesResearch/Results/PowerlessNulls.lean`
+(commit `dd4072f`) of the paper project `RemyDegenne/evalues_research`.
+
+## References
+
+* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, Note 22, and the
+  Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026.
+-/
+
+public section
+
+open Set
+open scoped ENNReal
+
+namespace MeasureTheory
+
+variable {ι : Type*} [Fintype ι] {X : ι → Type*} {mX : ∀ i, MeasurableSpace (X i)}
+
+/-- **Total variation distance between product measures.** The total variation distance between
+two finite products of probability measures is at most the sum of the distances between the
+factors. -/
+theorem etvDist_pi_le_sum (μ ν : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)]
+    [∀ i, IsProbabilityMeasure (ν i)] :
+    etvDist (Measure.pi μ) (Measure.pi ν) ≤ ∑ i, etvDist (μ i) (ν i) := by
+  choose ρ hρμ hρν hρ using fun i ↦ exists_le_le_add_etvDist (μ i) (ν i)
+  have (i : ι) : IsFiniteMeasure (ρ i) := isFiniteMeasure_of_le (μ i) (hρμ i)
+  have hm (i : ι) : ρ i univ ≤ 1 := (hρμ i univ).trans prob_le_one
+  calc etvDist (Measure.pi μ) (Measure.pi ν)
+  _ ≤ etvDist (Measure.pi μ) (Measure.pi ρ) + etvDist (Measure.pi ρ) (Measure.pi ν) :=
+    etvDist_triangle _ _ _
+  _ = 2 * (1 - ∏ i, ρ i univ) := by
+    rw [etvDist_of_ge (Measure.pi_mono hρμ), etvDist_of_le (Measure.pi_mono hρν)]
+    simp [Measure.pi_univ, two_mul]
+  _ ≤ 2 * ∑ i, (1 - ρ i univ) := by
+    gcongr; exact ENNReal.one_sub_prod_le_sum_one_sub _ fun i _ ↦ hm i
+  _ = ∑ i, 2 * (1 - ρ i univ) := Finset.mul_sum _ _ _
+  _ ≤ ∑ i, etvDist (μ i) (ν i) := by
+    gcongr with i
+    rw [ENNReal.mul_sub fun _ _ ↦ ENNReal.ofNat_ne_top, mul_one, tsub_le_iff_left]
+    simpa [one_add_one_eq_two] using (hρ i).le
+
+end MeasureTheory