diff --git a/LMLExplore/EValues/CondEVariable.lean b/LMLExplore/EValues/CondEVariable.lean
new file mode 100644
index 00000000..c13a6ffe
--- /dev/null
+++ b/LMLExplore/EValues/CondEVariable.lean
@@ -0,0 +1,282 @@
+/-
+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.MeasureTheory.Measure.WithDensity
+public import Mathlib.MeasureTheory.Function.ConditionalLExpectation
+public import Statlib.EValues.EVariable
+
+/-!
+# Conditional e-variables
+
+A conditional e-variable given a σ-algebra `m` for a set of measures `S` is a measurable
+`X : Ω → ℝ≥0∞` whose conditional expectation given `m` is at most `1` under every `P ∈ S`. It is
+stated with set integrals, `∫⁻ ω in s, X ω ∂P ≤ P s` for every `m`-measurable `s`, which needs
+neither integrability nor σ-finiteness of the restriction of `P` to `m`. When those restrictions
+are σ-finite, it is the bound `P⁻[X|m] ≤ 1` on Mathlib's conditional expectation
+`MeasureTheory.condLExp` of `ℝ≥0∞`-valued variables. Conditional
+e-variables are the factors of test supermartingales: the factor of round `n` of a product of
+sequential e-variables, of a bet or of a portfolio is a conditional e-variable given the past
+`ℱ n` [GdHK24, Definition 1; RW, Proposition 7.20].
+
+A known factor can be pulled out: `∫⁻ Y * X ∂P ≤ ∫⁻ Y ∂P` for every `m`-measurable `Y`, through
+`MeasureTheory.lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le`. Hence a portfolio
+`∑ i, w i * E i` of conditional e-variables with `m`-measurable weights summing to at most `1` is
+a conditional e-variable.
+
+## Main definitions
+
+* `ProbabilityTheory.IsCondEVar X m S`: `X` is a conditional e-variable given `m` for `S`.
+* `ProbabilityTheory.IsExactCondEVar X m S`: `X` is an exact conditional e-variable,
+  `∫⁻ ω in s, X ω ∂P = P s` for every `m`-measurable `s`.
+
+## Main statements
+
+* `ProbabilityTheory.isCondEVar_iff_withDensity_trim_le`: `X` is a conditional e-variable exactly
+  when the restriction of `P.withDensity X` to `m` is at most that of `P`.
+* `ProbabilityTheory.isCondEVar_iff_condLExp_le`,
+  `ProbabilityTheory.isExactCondEVar_iff_condLExp_eq`: for σ-finite restrictions to `m`, the
+  bounds `P⁻[X|m] ≤ 1` and `P⁻[X|m] = 1` on the conditional expectation.
+* `ProbabilityTheory.isCondEVar_bot_iff`: for a null of finite measures, the conditional
+  e-variables given `⊥` are Statlib's e-variables.
+* `ProbabilityTheory.IsCondEVar.setLIntegral_mul_le`: an `m`-measurable factor can be pulled out.
+* `ProbabilityTheory.isCondEVar_sum_mul`, `ProbabilityTheory.isExactCondEVar_sum_mul`:
+  portfolios of conditional e-variables.
+
+## References
+
+* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in
+  Statistics 1 (2025), arXiv:2410.23614.
+* [GdHK24] P. Grünwald, R. de Heide and W. M. Koolen, *Safe testing*, J. R. Stat. Soc. Ser. B 86
+  (2024), arXiv:1906.07801.
+-/
+
+public section
+
+open MeasureTheory Set
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {Ω ι : Type*} {m m' mΩ : MeasurableSpace Ω} {S T : Set (Measure Ω)} {P : Measure Ω}
+  {X Y : Ω → ℝ≥0∞} {s : Set Ω}
+
+/-- `X` is a conditional e-variable given the σ-algebra `m` for the set of measures `S`: it is
+measurable, and its conditional expectation given `m` is at most `1` under every `P ∈ S`, in the
+form `∫⁻ ω in s, X ω ∂P ≤ P s` for every `m`-measurable `s`. -/
+structure IsCondEVar (X : Ω → ℝ≥0∞) (m : MeasurableSpace Ω) (S : Set (@Measure Ω mΩ)) :
+    Prop where
+  measurable : Measurable[mΩ] X
+  setLIntegral_le : ∀ P ∈ S, ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, X ω ∂P ≤ P s
+
+/-- `X` is an exact conditional e-variable given the σ-algebra `m` for the set of measures `S`: it
+is measurable, and its conditional expectation given `m` is `1` under every `P ∈ S`, in the form
+`∫⁻ ω in s, X ω ∂P = P s` for every `m`-measurable `s`. -/
+structure IsExactCondEVar (X : Ω → ℝ≥0∞) (m : MeasurableSpace Ω) (S : Set (@Measure Ω mΩ)) :
+    Prop where
+  measurable : Measurable[mΩ] X
+  setLIntegral_eq : ∀ P ∈ S, ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, X ω ∂P = P s
+
+/-- An exact conditional e-variable is a conditional e-variable. -/
+theorem IsExactCondEVar.isCondEVar (hX : IsExactCondEVar X m S) : IsCondEVar X m S :=
+  ⟨hX.measurable, fun P hP s hs ↦ (hX.setLIntegral_eq P hP s hs).le⟩
+
+/-- The constant `1` is an exact conditional e-variable given every σ-algebra. -/
+@[simp]
+theorem isExactCondEVar_one : IsExactCondEVar 1 m S :=
+  ⟨measurable_const, fun _ _ _ _ ↦ by simp⟩
+
+/-- The constant `1` is a conditional e-variable given every σ-algebra. -/
+@[simp]
+theorem isCondEVar_one : IsCondEVar 1 m S :=
+  isExactCondEVar_one.isCondEVar
+
+/-! ### Monotonicity and congruence -/
+
+namespace IsCondEVar
+
+/-- A conditional e-variable for `T` is one for every subset of `T`. -/
+theorem anti_set (hST : S ⊆ T) (hX : IsCondEVar X m T) : IsCondEVar X m S :=
+  ⟨hX.measurable, fun P hP ↦ hX.setLIntegral_le P (hST hP)⟩
+
+/-- A conditional e-variable given `m` is one given every coarser σ-algebra. -/
+theorem of_le (hm : m' ≤ m) (hX : IsCondEVar X m S) : IsCondEVar X m' S :=
+  ⟨hX.measurable, fun P hP s hs ↦ hX.setLIntegral_le P hP s (hm s hs)⟩
+
+/-- A measurable function almost surely equal to a conditional e-variable under every member of
+the null is a conditional e-variable. -/
+theorem congr (hX : IsCondEVar X m S) (hY : Measurable Y) (hXY : ∀ P ∈ S, X =ᵐ[P] Y) :
+    IsCondEVar Y m S :=
+  ⟨hY, fun P hP s hs ↦
+    (lintegral_congr_ae (ae_restrict_of_ae (hXY P hP))).symm.trans_le
+      (hX.setLIntegral_le P hP s hs)⟩
+
+end IsCondEVar
+
+namespace IsExactCondEVar
+
+/-- An exact conditional e-variable for `T` is one for every subset of `T`. -/
+theorem anti_set (hST : S ⊆ T) (hX : IsExactCondEVar X m T) : IsExactCondEVar X m S :=
+  ⟨hX.measurable, fun P hP ↦ hX.setLIntegral_eq P (hST hP)⟩
+
+/-- An exact conditional e-variable given `m` is one given every coarser σ-algebra. -/
+theorem of_le (hm : m' ≤ m) (hX : IsExactCondEVar X m S) : IsExactCondEVar X m' S :=
+  ⟨hX.measurable, fun P hP s hs ↦ hX.setLIntegral_eq P hP s (hm s hs)⟩
+
+/-- A measurable function almost surely equal to an exact conditional e-variable under every
+member of the null is an exact conditional e-variable. -/
+theorem congr (hX : IsExactCondEVar X m S) (hY : Measurable Y) (hXY : ∀ P ∈ S, X =ᵐ[P] Y) :
+    IsExactCondEVar Y m S :=
+  ⟨hY, fun P hP s hs ↦
+    (lintegral_congr_ae (ae_restrict_of_ae (hXY P hP))).symm.trans
+      (hX.setLIntegral_eq P hP s hs)⟩
+
+end IsExactCondEVar
+
+/-! ### Characterizations -/
+
+/-- `X` is a conditional e-variable given a sub-σ-algebra `m` exactly when it is measurable and,
+for every `P ∈ S`, the restriction of `P.withDensity X` to `m` is at most that of `P`. -/
+theorem isCondEVar_iff_withDensity_trim_le (hm : m ≤ mΩ) :
+    IsCondEVar X m S ↔ Measurable X ∧ ∀ P ∈ S, (P.withDensity X).trim hm ≤ P.trim hm := by
+  have h (P : Measure Ω) : (P.withDensity X).trim hm ≤ P.trim hm ↔
+      ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, X ω ∂P ≤ P s := by
+    simpa using withDensity_trim_le_withDensity_trim_iff (μ := P) (f := X) (g := 1) hm
+  simp_rw [h]
+  exact ⟨fun hX ↦ ⟨hX.measurable, hX.setLIntegral_le⟩, fun hX ↦ ⟨hX.1, hX.2⟩⟩
+
+/-- `X` is an exact conditional e-variable given a sub-σ-algebra `m` exactly when it is
+measurable and, for every `P ∈ S`, the restrictions of `P.withDensity X` and of `P` to `m` are
+equal. -/
+theorem isExactCondEVar_iff_withDensity_trim_eq (hm : m ≤ mΩ) :
+    IsExactCondEVar X m S ↔ Measurable X ∧ ∀ P ∈ S, (P.withDensity X).trim hm = P.trim hm := by
+  have h (P : Measure Ω) : (P.withDensity X).trim hm = P.trim hm ↔
+      ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, X ω ∂P = P s := by
+    simpa using withDensity_trim_eq_withDensity_trim_iff (μ := P) (f := X) (g := 1) hm
+  simp_rw [h]
+  exact ⟨fun hX ↦ ⟨hX.measurable, hX.setLIntegral_eq⟩, fun hX ↦ ⟨hX.1, hX.2⟩⟩
+
+/-- When the restrictions to a sub-σ-algebra `m` of the members of `S` are σ-finite, `X` is a
+conditional e-variable given `m` exactly when it is measurable and its conditional expectation
+`P⁻[X|m]` is almost surely at most `1` under every `P ∈ S`. -/
+theorem isCondEVar_iff_condLExp_le (hm : m ≤ mΩ) (hS : ∀ P ∈ S, SigmaFinite (P.trim hm)) :
+    IsCondEVar X m S ↔ Measurable X ∧ ∀ P ∈ S, P⁻[X|m] ≤ᵐ[P] 1 := by
+  refine ⟨fun hX ↦ ⟨hX.measurable, fun P hP ↦ ?_⟩, fun hX ↦ ⟨hX.1, fun P hP s hs ↦ ?_⟩⟩ <;>
+    have := hS P hP
+  · refine ae_le_of_ae_le_trim (hm := hm) <| ae_le_of_forall_setLIntegral_le_of_sigmaFinite
+      (μ := P.trim hm) (measurable_condLExp _ _ _) fun s hs _ ↦ ?_
+    rw [setLIntegral_condLExp_trim hm _ _ hs]
+    simpa [trim_measurableSet_eq hm hs] using hX.setLIntegral_le P hP s hs
+  · rw [← setLIntegral_condLExp hm P X hs]
+    simpa using lintegral_mono_ae (ae_restrict_of_ae (hX.2 P hP))
+
+/-- When the restrictions to a sub-σ-algebra `m` of the members of `S` are σ-finite, `X` is an
+exact conditional e-variable given `m` exactly when it is measurable and its conditional
+expectation `P⁻[X|m]` is almost surely `1` under every `P ∈ S`. -/
+theorem isExactCondEVar_iff_condLExp_eq (hm : m ≤ mΩ) (hS : ∀ P ∈ S, SigmaFinite (P.trim hm)) :
+    IsExactCondEVar X m S ↔ Measurable X ∧ ∀ P ∈ S, P⁻[X|m] =ᵐ[P] 1 := by
+  refine ⟨fun hX ↦ ⟨hX.measurable, fun P hP ↦ ?_⟩, fun hX ↦ ⟨hX.1, fun P hP s hs ↦ ?_⟩⟩ <;>
+    have := hS P hP
+  · exact (ae_eq_condLExp hm P X (Y := 1) (by fun_prop) fun s hs ↦ by
+      simpa using (hX.setLIntegral_eq P hP s hs).symm).symm
+  · rw [← setLIntegral_condLExp hm P X hs, lintegral_congr_ae (ae_restrict_of_ae (hX.2 P hP))]
+    simp
+
+/-- For a null of finite measures, the conditional e-variables given the trivial σ-algebra are
+exactly the e-variables. -/
+theorem isCondEVar_bot_iff (hS : ∀ P ∈ S, IsFiniteMeasure P) :
+    IsCondEVar X ⊥ S ↔ IsEVar X S := by
+  refine ⟨fun hX ↦ IsEVar.of_lintegral_le_measure_univ hS hX.measurable fun P hP ↦ ?_,
+    fun hX ↦ ⟨hX.measurable, fun P hP s hs ↦ ?_⟩⟩
+  · simpa using hX.setLIntegral_le P hP univ MeasurableSet.univ
+  · rcases MeasurableSpace.measurableSet_bot_iff.1 hs with rfl | rfl
+    · simp
+    · simpa using hX.lintegral_le_measure_univ P hP
+
+/-- A conditional e-variable given any σ-algebra is an e-variable for a null of finite
+measures. -/
+theorem IsCondEVar.isEVar (hS : ∀ P ∈ S, IsFiniteMeasure P) (hX : IsCondEVar X m S) :
+    IsEVar X S :=
+  (isCondEVar_bot_iff hS).1 (hX.of_le bot_le)
+
+/-! ### Pulling out a known factor -/
+
+/-- A factor `Y` that is measurable for a sub-σ-algebra `m` can be pulled out of the conditional
+expectation of a conditional e-variable given `m`: `∫⁻ Y * X ∂P ≤ ∫⁻ Y ∂P`. -/
+theorem IsCondEVar.lintegral_mul_le (hm : m ≤ mΩ) (hX : IsCondEVar X m S) (hP : P ∈ S)
+    (hY : Measurable[m] Y) :
+    ∫⁻ ω, Y ω * X ω ∂P ≤ ∫⁻ ω, Y ω ∂P := by
+  simpa using lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le (g := 1) hm
+    hX.measurable.aemeasurable aemeasurable_const
+    (fun s hs ↦ by simpa using hX.setLIntegral_le P hP s hs) hY
+
+/-- A factor `Y` that is measurable for a sub-σ-algebra `m` can be pulled out of the conditional
+expectation of an exact conditional e-variable given `m`: `∫⁻ Y * X ∂P = ∫⁻ Y ∂P`. -/
+theorem IsExactCondEVar.lintegral_mul_eq (hm : m ≤ mΩ) (hX : IsExactCondEVar X m S)
+    (hP : P ∈ S) (hY : Measurable[m] Y) :
+    ∫⁻ ω, Y ω * X ω ∂P = ∫⁻ ω, Y ω ∂P := by
+  simpa using lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq (g := 1) hm
+    hX.measurable.aemeasurable aemeasurable_const
+    (fun s hs ↦ by simpa using hX.setLIntegral_eq P hP s hs) hY
+
+/-- The set-integral form of `IsCondEVar.lintegral_mul_le`: for `m`-measurable `Y` and `s`,
+`∫⁻ ω in s, Y ω * X ω ∂P ≤ ∫⁻ ω in s, Y ω ∂P`. -/
+theorem IsCondEVar.setLIntegral_mul_le (hm : m ≤ mΩ) (hX : IsCondEVar X m S) (hP : P ∈ S)
+    (hY : Measurable[m] Y) (hs : MeasurableSet[m] s) :
+    ∫⁻ ω in s, Y ω * X ω ∂P ≤ ∫⁻ ω in s, Y ω ∂P := by
+  rw [← lintegral_indicator (hm s hs), ← lintegral_indicator (hm s hs)]
+  simp_rw [indicator_mul_left]
+  exact hX.lintegral_mul_le hm hP (hY.indicator hs)
+
+/-- The set-integral form of `IsExactCondEVar.lintegral_mul_eq`: for `m`-measurable `Y` and `s`,
+`∫⁻ ω in s, Y ω * X ω ∂P = ∫⁻ ω in s, Y ω ∂P`. -/
+theorem IsExactCondEVar.setLIntegral_mul_eq (hm : m ≤ mΩ) (hX : IsExactCondEVar X m S)
+    (hP : P ∈ S) (hY : Measurable[m] Y) (hs : MeasurableSet[m] s) :
+    ∫⁻ ω in s, Y ω * X ω ∂P = ∫⁻ ω in s, Y ω ∂P := by
+  rw [← lintegral_indicator (hm s hs), ← lintegral_indicator (hm s hs)]
+  simp_rw [indicator_mul_left]
+  exact hX.lintegral_mul_eq hm hP (hY.indicator hs)
+
+/-! ### Portfolios -/
+
+/-- A portfolio of conditional e-variables given a sub-σ-algebra `m`, with `m`-measurable weights
+`w ω i` summing to at most `1`, is a conditional e-variable given `m`. -/
+theorem isCondEVar_sum_mul [Fintype ι] (hm : m ≤ mΩ) {E : ι → Ω → ℝ≥0∞} {w : Ω → ι → ℝ≥0∞}
+    (hE : ∀ i, IsCondEVar (E i) m S) (hw : ∀ i, Measurable[m] (fun ω ↦ w ω i))
+    (hw_sum : ∀ ω, ∑ i, w ω i ≤ 1) :
+    IsCondEVar (fun ω ↦ ∑ i, w ω i * E i ω) m S := by
+  have hwm (i : ι) : Measurable (fun ω ↦ w ω i) := (hw i).mono hm le_rfl
+  refine ⟨Finset.measurable_fun_sum _ fun i _ ↦ (hwm i).mul (hE i).measurable,
+    fun P hP s hs ↦ ?_⟩
+  rw [lintegral_finsetSum (f := fun i ω ↦ w ω i * E i ω) _
+    fun i _ ↦ (hwm i).mul (hE i).measurable]
+  calc ∑ i, ∫⁻ ω in s, w ω i * E i ω ∂P
+      ≤ ∑ i, ∫⁻ ω in s, w ω i ∂P :=
+        Finset.sum_le_sum fun i _ ↦ (hE i).setLIntegral_mul_le hm hP (hw i) hs
+    _ = ∫⁻ ω in s, ∑ i, w ω i ∂P := 
+        (lintegral_finsetSum (f := fun i ω ↦ w ω i) _ fun i _ ↦ hwm i).symm
+    _ ≤ ∫⁻ _ in s, 1 ∂P := lintegral_mono hw_sum
+    _ = P s := by simp
+
+/-- A portfolio of exact conditional e-variables given a sub-σ-algebra `m`, with `m`-measurable
+weights `w ω i` summing to `1`, is an exact conditional e-variable given `m`. -/
+theorem isExactCondEVar_sum_mul [Fintype ι] (hm : m ≤ mΩ) {E : ι → Ω → ℝ≥0∞}
+    {w : Ω → ι → ℝ≥0∞} (hE : ∀ i, IsExactCondEVar (E i) m S)
+    (hw : ∀ i, Measurable[m] (fun ω ↦ w ω i)) (hw_sum : ∀ ω, ∑ i, w ω i = 1) :
+    IsExactCondEVar (fun ω ↦ ∑ i, w ω i * E i ω) m S := by
+  have hwm (i : ι) : Measurable (fun ω ↦ w ω i) := (hw i).mono hm le_rfl
+  refine ⟨Finset.measurable_fun_sum _ fun i _ ↦ (hwm i).mul (hE i).measurable,
+    fun P hP s hs ↦ ?_⟩
+  rw [lintegral_finsetSum (f := fun i ω ↦ w ω i * E i ω) _
+    fun i _ ↦ (hwm i).mul (hE i).measurable]
+  calc ∑ i, ∫⁻ ω in s, w ω i * E i ω ∂P
+      = ∑ i, ∫⁻ ω in s, w ω i ∂P :=
+        Finset.sum_congr rfl fun i _ ↦ (hE i).setLIntegral_mul_eq hm hP (hw i) hs
+    _ = ∫⁻ ω in s, ∑ i, w ω i ∂P := 
+        (lintegral_finsetSum (f := fun i ω ↦ w ω i) _ fun i _ ↦ hwm i).symm
+    _ = P s := by simp [hw_sum]
+
+end ProbabilityTheory
diff --git a/LMLExplore/EValues/TestSupermartingale.lean b/LMLExplore/EValues/TestSupermartingale.lean
new file mode 100644
index 00000000..91b25dfa
--- /dev/null
+++ b/LMLExplore/EValues/TestSupermartingale.lean
@@ -0,0 +1,446 @@
+/-
+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.CondEVariable
+public import LMLExplore.Probability.Martingale.Basic
+public import LMLExplore.Probability.Process.Adapted
+
+/-!
+# Test supermartingales and wealth processes
+
+A test supermartingale for a set of measures `S` is an `ℝ≥0∞`-valued process that is a
+supermartingale under every `P ∈ S` and starts with expectation at most `1` [RW, Definition 7.3;
+ShSVV11]. Values are in `ℝ≥0∞`, the supermartingale property is stated with set integrals and no
+integrability condition is imposed beyond that of the initial value, so that products of
+e-variables taking infinite values and nonintegrable bets are covered. Test supermartingales are
+the processes against which e-processes are defined and through which Ville's inequality bounds
+the probability that a sequential test ever rejects.
+
+The main construction is the wealth of a gambler who reinvests at every round: an initial wealth
+`M₀` with expectation at most `1` (an e-variable, for a null of probability measures) times the
+product of the factors `F k`, each a conditional e-variable given the past `ℱ k`
+(`ProbabilityTheory.IsCondEVar`). Conversely, every test supermartingale is almost surely such a
+wealth process. It contains the products of sequential e-variables
+[RW, Proposition 7.20; GdHK24, Proposition 2], the wealth of portfolios `∑ i, w k i * E k i` of
+conditional e-variables with predictable weights [WSJ26], and betting
+`∏ k, (1 - c k + c k * E k)` with predictable bets `c k ≤ 1` [RW, Definition 7.21; WSR24].
+
+## Main definitions
+
+* `ProbabilityTheory.IsENNSupermartingale M ℱ S`: `M : ℕ → Ω → ℝ≥0∞` is adapted and
+  `∫⁻ ω in s, M (n + 1) ω ∂P ≤ ∫⁻ ω in s, M n ω ∂P` for every `P ∈ S`, `n` and
+  `ℱ n`-measurable `s`.
+* `ProbabilityTheory.IsTestSupermartingale M ℱ S`: moreover `∫⁻ M 0 ∂P ≤ 1` for every `P ∈ S`.
+* `ProbabilityTheory.IsTestMartingale M ℱ S`: the same, with equalities of the set integrals.
+
+## Main statements
+
+* `MeasureTheory.Supermartingale.isTestSupermartingale_ofReal`,
+  `ProbabilityTheory.IsTestSupermartingale.supermartingale_toReal`: the bridges with Mathlib's
+  real supermartingales.
+* `ProbabilityTheory.IsTestSupermartingale.ae_lt_top`: a test supermartingale is almost surely
+  finite.
+* `ProbabilityTheory.isTestSupermartingale_mul_prod`, `ProbabilityTheory.isTestMartingale_mul_prod`:
+  wealth processes `M₀ * ∏ k < n, F k` of conditional e-variables.
+* `ProbabilityTheory.isTestSupermartingale_portfolio`,
+  `ProbabilityTheory.isTestSupermartingale_prod`,
+  `ProbabilityTheory.isTestSupermartingale_betting_condEVar` and their martingale versions:
+  portfolios, products of sequential e-variables and betting.
+* `ProbabilityTheory.IsENNSupermartingale.isCondEVar_div`,
+  `ProbabilityTheory.IsTestSupermartingale.ae_eq_mul_prod_div`: conversely, every test
+  supermartingale is almost surely the wealth `M 0 * ∏ k < n, M (k + 1) / M k` of its successive
+  ratios, which are conditional e-variables [WSR24, Proposition 3].
+
+## References
+
+* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in
+  Statistics 1 (2025), arXiv:2410.23614.
+* [ShSVV11] G. Shafer, A. Shen, N. Vereshchagin and V. Vovk, *Test martingales, Bayes factors and
+  p-values*, Statist. Sci. 26 (2011), arXiv:0912.4269.
+* [GdHK24] P. Grünwald, R. de Heide and W. M. Koolen, *Safe testing*, J. R. Stat. Soc. Ser. B 86
+  (2024), arXiv:1906.07801.
+* [WSR24] I. Waudby-Smith and A. Ramdas, *Estimating means of bounded random variables by
+  betting*, J. R. Stat. Soc. Ser. B 86 (2024), arXiv:2010.09686.
+* [WSJ26] I. Waudby-Smith, R. Sandoval and M. I. Jordan, *Instance-log-optimality of
+  portfolio-based e-processes and their sequential hypothesis tests*, arXiv:2504.02818.
+-/
+
+public section
+
+open MeasureTheory Set Finset
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {Ω ι : Type*} {mΩ : MeasurableSpace Ω} {ℱ : Filtration ℕ mΩ} {S T : Set (Measure Ω)}
+  {P : Measure Ω} {M M' : ℕ → Ω → ℝ≥0∞}
+
+/-- `M : ℕ → Ω → ℝ≥0∞` is a supermartingale for the filtration `ℱ` under every member of `S`:
+it is adapted and `∫⁻ ω in s, M (n + 1) ω ∂P ≤ ∫⁻ ω in s, M n ω ∂P` for every `P ∈ S`, every `n`
+and every `ℱ n`-measurable `s`. No integrability is assumed. -/
+structure IsENNSupermartingale (M : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ)
+    (S : Set (Measure Ω)) : Prop where
+  adapted : Adapted ℱ M
+  setLIntegral_succ_le : ∀ P ∈ S, ∀ n s, MeasurableSet[ℱ n] s →
+    ∫⁻ ω in s, M (n + 1) ω ∂P ≤ ∫⁻ ω in s, M n ω ∂P
+
+/-- `M : ℕ → Ω → ℝ≥0∞` is a test supermartingale for the filtration `ℱ` and the null `S`: a
+supermartingale under every member of `S` with `∫⁻ M 0 ∂P ≤ 1` for every `P ∈ S`
+[RW, Definition 7.3]. -/
+structure IsTestSupermartingale (M : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ)
+    (S : Set (Measure Ω)) : Prop extends IsENNSupermartingale M ℱ S where
+  lintegral_zero_le : ∀ P ∈ S, ∫⁻ ω, M 0 ω ∂P ≤ 1
+
+/-- `M : ℕ → Ω → ℝ≥0∞` is a test martingale for the filtration `ℱ` and the null `S`: it is
+adapted, `∫⁻ M 0 ∂P ≤ 1` and `∫⁻ ω in s, M (n + 1) ω ∂P = ∫⁻ ω in s, M n ω ∂P` for every
+`P ∈ S`, every `n` and every `ℱ n`-measurable `s` [RW, Definition 7.3]. -/
+structure IsTestMartingale (M : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ)
+    (S : Set (Measure Ω)) : Prop where
+  adapted : Adapted ℱ M
+  lintegral_zero_le : ∀ P ∈ S, ∫⁻ ω, M 0 ω ∂P ≤ 1
+  setLIntegral_succ_eq : ∀ P ∈ S, ∀ n s, MeasurableSet[ℱ n] s →
+    ∫⁻ ω in s, M (n + 1) ω ∂P = ∫⁻ ω in s, M n ω ∂P
+
+/-! ### Supermartingales in `ℝ≥0∞` -/
+
+namespace IsENNSupermartingale
+
+/-- Each value of an `ℝ≥0∞`-valued supermartingale is measurable. -/
+theorem measurable (hM : IsENNSupermartingale M ℱ S) (n : ℕ) : Measurable (M n) :=
+  (hM.adapted n).mono (ℱ.le n) le_rfl
+
+/-- A supermartingale under every member of `T` is one under every member of a subset of `T`. -/
+theorem anti_set (hST : S ⊆ T) (hM : IsENNSupermartingale M ℱ T) :
+    IsENNSupermartingale M ℱ S :=
+  ⟨hM.adapted, fun P hP ↦ hM.setLIntegral_succ_le P (hST hP)⟩
+
+/-- An adapted process almost surely equal at every time to a supermartingale, under every member
+of the null, is a supermartingale. -/
+theorem congr (hM : IsENNSupermartingale M ℱ S) (hM' : Adapted ℱ M')
+    (h : ∀ P ∈ S, ∀ n, M n =ᵐ[P] M' n) : IsENNSupermartingale M' ℱ S :=
+  ⟨hM', fun P hP n s hs ↦ by
+    rw [← lintegral_congr_ae (ae_restrict_of_ae (h P hP (n + 1))),
+      ← lintegral_congr_ae (ae_restrict_of_ae (h P hP n))]
+    exact hM.setLIntegral_succ_le P hP n s hs⟩
+
+/-- The set integrals of an `ℝ≥0∞`-valued supermartingale over an `ℱ i`-measurable set do not
+increase after time `i`. -/
+theorem setLIntegral_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) {i j : ℕ} (hij : i ≤ j)
+    {s : Set Ω} (hs : MeasurableSet[ℱ i] s) :
+    ∫⁻ ω in s, M j ω ∂P ≤ ∫⁻ ω in s, M i ω ∂P := by
+  induction j, hij using Nat.le_induction with
+  | base => exact le_rfl
+  | succ j hij ih => exact (hM.setLIntegral_succ_le P hP j s (ℱ.mono hij s hs)).trans ih
+
+/-- The expectations of an `ℝ≥0∞`-valued supermartingale do not increase. -/
+theorem lintegral_le (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S) {i j : ℕ} (hij : i ≤ j) :
+    ∫⁻ ω, M j ω ∂P ≤ ∫⁻ ω, M i ω ∂P := by
+  simpa using hM.setLIntegral_le hP hij MeasurableSet.univ
+
+/-- An `ℝ≥0∞`-valued supermartingale with finite initial expectation is almost surely finite at
+every time. -/
+theorem ae_lt_top (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S)
+    (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) : ∀ᵐ ω ∂P, ∀ n, M n ω < ∞ :=
+  ae_all_iff.2 fun n ↦
+    MeasureTheory.ae_lt_top (hM.measurable n) ((hM.lintegral_le hP n.zero_le).trans_lt h0.lt_top).ne
+
+/-- An `ℝ≥0∞`-valued supermartingale with finite initial expectation under a finite measure has
+real values forming a real supermartingale. -/
+theorem supermartingale_toReal (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) :
+    Supermartingale (fun n ω ↦ (M n ω).toReal) ℱ P := by
+  have hofReal (n : ℕ) : (fun ω ↦ ENNReal.ofReal (M n ω).toReal) =ᵐ[P] M n := by
+    filter_upwards [hM.ae_lt_top hP h0] with ω hω using ENNReal.ofReal_toReal (hω n).ne
+  refine LMLExplore.supermartingale_of_setLIntegral_succ_le (fun n ↦ (hM.adapted n).ennreal_toReal)
+    (fun n ↦ ae_of_all _ fun _ ↦ ENNReal.toReal_nonneg)
+    (integrable_toReal_of_lintegral_ne_top (hM.measurable 0).aemeasurable h0) fun n s hs ↦ ?_
+  rw [lintegral_congr_ae (ae_restrict_of_ae (hofReal (n + 1))),
+    lintegral_congr_ae (ae_restrict_of_ae (hofReal n))]
+  exact hM.setLIntegral_succ_le P hP n s hs
+
+end IsENNSupermartingale
+
+/-! ### Test supermartingales and test martingales -/
+
+namespace IsTestSupermartingale
+
+/-- Each value of a test supermartingale is measurable. -/
+theorem measurable (hM : IsTestSupermartingale M ℱ S) (n : ℕ) : Measurable (M n) :=
+  hM.toIsENNSupermartingale.measurable n
+
+/-- A test supermartingale for `T` is one for every subset of `T`. -/
+theorem anti_set (hST : S ⊆ T) (hM : IsTestSupermartingale M ℱ T) :
+    IsTestSupermartingale M ℱ S :=
+  ⟨hM.toIsENNSupermartingale.anti_set hST, fun P hP ↦ hM.lintegral_zero_le P (hST hP)⟩
+
+/-- An adapted process almost surely equal at every time to a test supermartingale, under every
+member of the null, is a test supermartingale. -/
+theorem congr (hM : IsTestSupermartingale M ℱ S) (hM' : Adapted ℱ M')
+    (h : ∀ P ∈ S, ∀ n, M n =ᵐ[P] M' n) : IsTestSupermartingale M' ℱ S :=
+  ⟨hM.toIsENNSupermartingale.congr hM' h, fun P hP ↦
+    (lintegral_congr_ae (h P hP 0)).symm.trans_le (hM.lintegral_zero_le P hP)⟩
+
+/-- Every value of a test supermartingale has expectation at most `1`. -/
+theorem lintegral_le_one (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) (n : ℕ) :
+    ∫⁻ ω, M n ω ∂P ≤ 1 :=
+  (hM.lintegral_le hP n.zero_le).trans (hM.lintegral_zero_le P hP)
+
+/-- Every value of a test supermartingale for a null of probability measures is an
+e-variable. -/
+theorem isEVar (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hM : IsTestSupermartingale M ℱ S)
+    (n : ℕ) : IsEVar (M n) S :=
+  IsEVar.of_lintegral_le_one hS (hM.measurable n) fun _ hP ↦ hM.lintegral_le_one hP n
+
+/-- A test supermartingale is almost surely finite at every time. -/
+theorem ae_lt_top (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S) :
+    ∀ᵐ ω ∂P, ∀ n, M n ω < ∞ :=
+  hM.toIsENNSupermartingale.ae_lt_top hP
+    ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne
+
+/-- The real values of a test supermartingale form a real supermartingale under every finite
+member of the null. -/
+theorem supermartingale_toReal (hM : IsTestSupermartingale M ℱ S) (hP : P ∈ S)
+    [IsFiniteMeasure P] : Supermartingale (fun n ω ↦ (M n ω).toReal) ℱ P :=
+  hM.toIsENNSupermartingale.supermartingale_toReal hP
+    ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne
+
+end IsTestSupermartingale
+
+namespace IsTestMartingale
+
+/-- Each value of a test martingale is measurable. -/
+theorem measurable (hM : IsTestMartingale M ℱ S) (n : ℕ) : Measurable (M n) :=
+  (hM.adapted n).mono (ℱ.le n) le_rfl
+
+/-- A test martingale is a test supermartingale. -/
+theorem isTestSupermartingale (hM : IsTestMartingale M ℱ S) : IsTestSupermartingale M ℱ S :=
+  ⟨⟨hM.adapted, fun P hP n s hs ↦ (hM.setLIntegral_succ_eq P hP n s hs).le⟩,
+    hM.lintegral_zero_le⟩
+
+/-- A test martingale for `T` is one for every subset of `T`. -/
+theorem anti_set (hST : S ⊆ T) (hM : IsTestMartingale M ℱ T) : IsTestMartingale M ℱ S :=
+  ⟨hM.adapted, fun P hP ↦ hM.lintegral_zero_le P (hST hP),
+    fun P hP ↦ hM.setLIntegral_succ_eq P (hST hP)⟩
+
+/-- An adapted process almost surely equal at every time to a test martingale, under every member
+of the null, is a test martingale. -/
+theorem congr (hM : IsTestMartingale M ℱ S) (hM' : Adapted ℱ M')
+    (h : ∀ P ∈ S, ∀ n, M n =ᵐ[P] M' n) : IsTestMartingale M' ℱ S :=
+  ⟨hM', fun P hP ↦ (lintegral_congr_ae (h P hP 0)).symm.trans_le (hM.lintegral_zero_le P hP),
+    fun P hP n s hs ↦ by
+      rw [← lintegral_congr_ae (ae_restrict_of_ae (h P hP (n + 1))),
+        ← lintegral_congr_ae (ae_restrict_of_ae (h P hP n))]
+      exact hM.setLIntegral_succ_eq P hP n s hs⟩
+
+/-- The set integrals of a test martingale over an `ℱ i`-measurable set are constant after
+time `i`. -/
+theorem setLIntegral_eq (hM : IsTestMartingale M ℱ S) (hP : P ∈ S) {i j : ℕ} (hij : i ≤ j)
+    {s : Set Ω} (hs : MeasurableSet[ℱ i] s) :
+    ∫⁻ ω in s, M j ω ∂P = ∫⁻ ω in s, M i ω ∂P := by
+  induction j, hij using Nat.le_induction with
+  | base => rfl
+  | succ j hij ih => exact (hM.setLIntegral_succ_eq P hP j s (ℱ.mono hij s hs)).trans ih
+
+/-- The expectations of a test martingale are constant. -/
+theorem lintegral_eq (hM : IsTestMartingale M ℱ S) (hP : P ∈ S) (i j : ℕ) :
+    ∫⁻ ω, M j ω ∂P = ∫⁻ ω, M i ω ∂P := by
+  have h (n : ℕ) : ∫⁻ ω, M n ω ∂P = ∫⁻ ω, M 0 ω ∂P := by
+    simpa using hM.setLIntegral_eq hP n.zero_le MeasurableSet.univ
+  rw [h j, h i]
+
+end IsTestMartingale
+
+/-- The constant process `1` is a test martingale for every null of probability measures. -/
+theorem isTestMartingale_one (hS : ∀ P ∈ S, IsProbabilityMeasure P) :
+    IsTestMartingale 1 ℱ S :=
+  ⟨fun _ ↦ measurable_const, fun P hP ↦ by have := hS P hP; simp, fun _ _ _ _ _ ↦ rfl⟩
+
+/-- A real nonnegative supermartingale with initial expectation at most `1` is, through
+`ENNReal.ofReal`, a test supermartingale for the null `{P}`. -/
+theorem _root_.MeasureTheory.Supermartingale.isTestSupermartingale_ofReal
+    [SigmaFiniteFiltration P ℱ] {M : ℕ → Ω → ℝ} (hM : Supermartingale M ℱ P)
+    (hM_nonneg : ∀ n, 0 ≤ᵐ[P] M n) (h0 : ∫ ω, M 0 ω ∂P ≤ 1) :
+    IsTestSupermartingale (fun n ω ↦ ENNReal.ofReal (M n ω)) ℱ {P} := by
+  refine ⟨⟨fun n ↦ (hM.stronglyAdapted n).measurable.ennreal_ofReal, ?_⟩, ?_⟩
+  · rintro P' rfl n s hs
+    rw [← ofReal_integral_eq_lintegral_ofReal (hM.integrable (n + 1)).restrict
+        (ae_restrict_of_ae (hM_nonneg (n + 1))),
+      ← ofReal_integral_eq_lintegral_ofReal (hM.integrable n).restrict
+        (ae_restrict_of_ae (hM_nonneg n))]
+    exact ENNReal.ofReal_le_ofReal (hM.setIntegral_le n.le_succ hs)
+  · rintro P' rfl
+    rw [← ofReal_integral_eq_lintegral_ofReal (hM.integrable 0) (hM_nonneg 0)]
+    exact ENNReal.ofReal_le_one.2 h0
+
+/-! ### Wealth processes -/
+
+/-- **Wealth of a reinvesting gambler.** For an `ℱ 0`-measurable initial wealth `M₀` with
+expectation at most `1` under every member of `S`, and factors `F k` that are
+`ℱ (k + 1)`-measurable conditional e-variables given `ℱ k`, the wealth
+`M₀ * ∏ k < n, F k` is a test supermartingale. -/
+theorem isTestSupermartingale_mul_prod {M₀ : Ω → ℝ≥0∞} (hM₀ : Measurable[ℱ 0] M₀)
+    (hM₀_le : ∀ P ∈ S, ∫⁻ ω, M₀ ω ∂P ≤ 1) {F : ℕ → Ω → ℝ≥0∞}
+    (hF_meas : ∀ k, Measurable[ℱ (k + 1)] (F k)) (hF : ∀ k, IsCondEVar (F k) (ℱ k) S) :
+    IsTestSupermartingale (fun n ω ↦ M₀ ω * ∏ k ∈ range n, F k ω) ℱ S := by
+  refine ⟨⟨adapted_mul_prod_range hM₀ hF_meas, fun P hP n s hs ↦ ?_⟩, by simpa using hM₀_le⟩
+  simp_rw [prod_range_succ, ← mul_assoc]
+  exact (hF n).setLIntegral_mul_le (ℱ.le n) hP (adapted_mul_prod_range hM₀ hF_meas n) hs
+
+/-- **Wealth of a reinvesting gambler, exact case.** For an `ℱ 0`-measurable initial wealth `M₀`
+with expectation at most `1` under every member of `S`, and factors `F k` that are
+`ℱ (k + 1)`-measurable exact conditional e-variables given `ℱ k`, the wealth
+`M₀ * ∏ k < n, F k` is a test martingale. -/
+theorem isTestMartingale_mul_prod {M₀ : Ω → ℝ≥0∞} (hM₀ : Measurable[ℱ 0] M₀)
+    (hM₀_le : ∀ P ∈ S, ∫⁻ ω, M₀ ω ∂P ≤ 1) {F : ℕ → Ω → ℝ≥0∞}
+    (hF_meas : ∀ k, Measurable[ℱ (k + 1)] (F k)) (hF : ∀ k, IsExactCondEVar (F k) (ℱ k) S) :
+    IsTestMartingale (fun n ω ↦ M₀ ω * ∏ k ∈ range n, F k ω) ℱ S := by
+  refine ⟨adapted_mul_prod_range hM₀ hF_meas, by simpa using hM₀_le, fun P hP n s hs ↦ ?_⟩
+  simp_rw [prod_range_succ, ← mul_assoc]
+  exact (hF n).setLIntegral_mul_eq (ℱ.le n) hP (adapted_mul_prod_range hM₀ hF_meas n) hs
+
+/-- **Wealth of portfolios** [WSJ26]. For conditional e-variables `E k i` given `ℱ k` that are
+`ℱ (k + 1)`-measurable, and `ℱ k`-measurable portfolios `w k` with `∑ i, w k ω i ≤ 1`, the wealth
+`M₀ * ∏ k < n, ∑ i, w k ω i * E k i ω` is a test supermartingale for every `ℱ 0`-measurable
+initial wealth `M₀` with expectation at most `1`. -/
+theorem isTestSupermartingale_portfolio [Fintype ι] {M₀ : Ω → ℝ≥0∞}
+    (hM₀ : Measurable[ℱ 0] M₀) (hM₀_le : ∀ P ∈ S, ∫⁻ ω, M₀ ω ∂P ≤ 1)
+    {E : ℕ → ι → Ω → ℝ≥0∞} (hE_meas : ∀ k i, Measurable[ℱ (k + 1)] (E k i))
+    (hE : ∀ k i, IsCondEVar (E k i) (ℱ k) S) {w : ℕ → Ω → ι → ℝ≥0∞}
+    (hw : ∀ k i, Measurable[ℱ k] (fun ω ↦ w k ω i)) (hw_sum : ∀ k ω, ∑ i, w k ω i ≤ 1) :
+    IsTestSupermartingale (fun n ω ↦ M₀ ω * ∏ k ∈ range n, ∑ i, w k ω i * E k i ω) ℱ S :=
+  isTestSupermartingale_mul_prod hM₀ hM₀_le
+    (fun k ↦ Finset.measurable_fun_sum _ fun i _ ↦
+      ((hw k i).mono (ℱ.mono k.le_succ) le_rfl).mul (hE_meas k i))
+    fun k ↦ isCondEVar_sum_mul (ℱ.le k) (hE k) (hw k) (hw_sum k)
+
+/-- **Wealth of portfolios, exact case** [WSJ26]. For exact conditional e-variables `E k i` given
+`ℱ k` that are `ℱ (k + 1)`-measurable, and `ℱ k`-measurable portfolios `w k` with
+`∑ i, w k ω i = 1`, the wealth `M₀ * ∏ k < n, ∑ i, w k ω i * E k i ω` is a test martingale for
+every `ℱ 0`-measurable initial wealth `M₀` with expectation at most `1`. -/
+theorem isTestMartingale_portfolio [Fintype ι] {M₀ : Ω → ℝ≥0∞}
+    (hM₀ : Measurable[ℱ 0] M₀) (hM₀_le : ∀ P ∈ S, ∫⁻ ω, M₀ ω ∂P ≤ 1)
+    {E : ℕ → ι → Ω → ℝ≥0∞} (hE_meas : ∀ k i, Measurable[ℱ (k + 1)] (E k i))
+    (hE : ∀ k i, IsExactCondEVar (E k i) (ℱ k) S) {w : ℕ → Ω → ι → ℝ≥0∞}
+    (hw : ∀ k i, Measurable[ℱ k] (fun ω ↦ w k ω i)) (hw_sum : ∀ k ω, ∑ i, w k ω i = 1) :
+    IsTestMartingale (fun n ω ↦ M₀ ω * ∏ k ∈ range n, ∑ i, w k ω i * E k i ω) ℱ S :=
+  isTestMartingale_mul_prod hM₀ hM₀_le
+    (fun k ↦ Finset.measurable_fun_sum _ fun i _ ↦
+      ((hw k i).mono (ℱ.mono k.le_succ) le_rfl).mul (hE_meas k i))
+    fun k ↦ isExactCondEVar_sum_mul (ℱ.le k) (hE k) (hw k) (hw_sum k)
+
+/-- **Products of sequential e-variables** [RW, Proposition 7.20; GdHK24, Proposition 2]. For
+conditional e-variables `E k` given `ℱ k` that are `ℱ (k + 1)`-measurable, `∏ k < n, E k` is a
+test supermartingale for every null of probability measures. -/
+theorem isTestSupermartingale_prod (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    {E : ℕ → Ω → ℝ≥0∞} (hE_meas : ∀ k, Measurable[ℱ (k + 1)] (E k))
+    (hE : ∀ k, IsCondEVar (E k) (ℱ k) S) :
+    IsTestSupermartingale (fun n ω ↦ ∏ k ∈ range n, E k ω) ℱ S := by
+  simpa using isTestSupermartingale_portfolio (ℱ := ℱ) (ι := Unit) (M₀ := 1) (w := fun _ _ _ ↦ 1)
+    measurable_const (fun P hP ↦ by have := hS P hP; simp) (fun k _ ↦ hE_meas k)
+    (fun k _ ↦ hE k) (fun _ _ ↦ measurable_const) (fun _ _ ↦ by simp)
+
+/-- **Products of sequential e-variables, exact case.** For exact conditional e-variables `E k`
+given `ℱ k` that are `ℱ (k + 1)`-measurable, `∏ k < n, E k` is a test martingale for every null
+of probability measures. -/
+theorem isTestMartingale_prod (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    {E : ℕ → Ω → ℝ≥0∞} (hE_meas : ∀ k, Measurable[ℱ (k + 1)] (E k))
+    (hE : ∀ k, IsExactCondEVar (E k) (ℱ k) S) :
+    IsTestMartingale (fun n ω ↦ ∏ k ∈ range n, E k ω) ℱ S := by
+  simpa using isTestMartingale_portfolio (ℱ := ℱ) (ι := Unit) (M₀ := 1) (w := fun _ _ _ ↦ 1)
+    measurable_const (fun P hP ↦ by have := hS P hP; simp) (fun k _ ↦ hE_meas k)
+    (fun k _ ↦ hE k) (fun _ _ ↦ measurable_const) (fun _ _ ↦ by simp)
+
+/-- **Betting** [RW, Definition 7.21; WSR24]. For conditional e-variables `E k` given `ℱ k` that
+are `ℱ (k + 1)`-measurable, and `ℱ k`-measurable bets `c k ≤ 1`, the wealth
+`∏ k < n, (1 - c k + c k * E k)` is a test supermartingale for every null of probability
+measures. -/
+theorem isTestSupermartingale_betting_condEVar (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    {E : ℕ → Ω → ℝ≥0∞} (hE_meas : ∀ k, Measurable[ℱ (k + 1)] (E k))
+    (hE : ∀ k, IsCondEVar (E k) (ℱ k) S) {c : ℕ → Ω → ℝ≥0∞}
+    (hc : ∀ k, Measurable[ℱ k] (c k)) (hc_le : ∀ k ω, c k ω ≤ 1) :
+    IsTestSupermartingale (fun n ω ↦ ∏ k ∈ range n, (1 - c k ω + c k ω * E k ω)) ℱ S := by
+  have := isTestSupermartingale_portfolio (ℱ := ℱ) (M₀ := 1) (w := fun k ω ↦ ![1 - c k ω, c k ω])
+    (E := fun k ↦ ![1, E k]) measurable_const (fun P hP ↦ by have := hS P hP; simp)
+    (fun k i ↦ by fin_cases i <;> simp [measurable_one, hE_meas k])
+    (fun k i ↦ by fin_cases i <;> simp [hE k])
+    (fun k i ↦ by fin_cases i <;> simp [(hc k).const_sub, hc k])
+    (fun k ω ↦ by simp [tsub_add_cancel_of_le (hc_le k ω)])
+  simpa [Fin.sum_univ_two] using this
+
+/-- **Betting, exact case.** For exact conditional e-variables `E k` given `ℱ k` that are
+`ℱ (k + 1)`-measurable, and `ℱ k`-measurable bets `c k ≤ 1`, the wealth
+`∏ k < n, (1 - c k + c k * E k)` is a test martingale for every null of probability measures. -/
+theorem isTestMartingale_betting_condEVar (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    {E : ℕ → Ω → ℝ≥0∞} (hE_meas : ∀ k, Measurable[ℱ (k + 1)] (E k))
+    (hE : ∀ k, IsExactCondEVar (E k) (ℱ k) S) {c : ℕ → Ω → ℝ≥0∞}
+    (hc : ∀ k, Measurable[ℱ k] (c k)) (hc_le : ∀ k ω, c k ω ≤ 1) :
+    IsTestMartingale (fun n ω ↦ ∏ k ∈ range n, (1 - c k ω + c k ω * E k ω)) ℱ S := by
+  have := isTestMartingale_portfolio (ℱ := ℱ) (M₀ := 1) (w := fun k ω ↦ ![1 - c k ω, c k ω])
+    (E := fun k ↦ ![1, E k]) measurable_const (fun P hP ↦ by have := hS P hP; simp)
+    (fun k i ↦ by fin_cases i <;> simp [measurable_one, hE_meas k])
+    (fun k i ↦ by fin_cases i <;> simp [hE k])
+    (fun k i ↦ by fin_cases i <;> simp [(hc k).const_sub, hc k])
+    (fun k ω ↦ by simp [tsub_add_cancel_of_le (hc_le k ω)])
+  simpa [Fin.sum_univ_two] using this
+
+/-! ### Test supermartingales as wealth processes -/
+
+/-- The successive ratios `M (k + 1) / M k` of an `ℝ≥0∞`-valued supermartingale, with
+`0 / 0 = 0` and `x / ∞ = 0`, are conditional e-variables given `ℱ k`. -/
+theorem IsENNSupermartingale.isCondEVar_div (hM : IsENNSupermartingale M ℱ S) (k : ℕ) :
+    IsCondEVar (fun ω ↦ M (k + 1) ω / M k ω) (ℱ k) S := by
+  refine ⟨(hM.measurable (k + 1)).div (hM.measurable k), fun P hP s hs ↦ ?_⟩
+  -- pull the `ℱ k`-measurable factor `𝟙_s / M k` out of the supermartingale inequality
+  have hY : Measurable[ℱ k] (s.indicator fun ω ↦ (M k ω)⁻¹) := (hM.adapted k).inv.indicator hs
+  calc ∫⁻ ω in s, M (k + 1) ω / M k ω ∂P
+      = ∫⁻ ω, s.indicator (fun ω ↦ (M k ω)⁻¹) ω * M (k + 1) ω ∂P := by
+        rw [← lintegral_indicator (ℱ.le k s hs)]
+        congr 1 with ω
+        by_cases hω : ω ∈ s <;> simp [hω, div_eq_mul_inv, mul_comm]
+    _ ≤ ∫⁻ ω, s.indicator (fun ω ↦ (M k ω)⁻¹) ω * M k ω ∂P :=
+        lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le (ℱ.le k)
+          (hM.measurable (k + 1)).aemeasurable (hM.measurable k).aemeasurable
+          (hM.setLIntegral_succ_le P hP k) hY
+    _ ≤ ∫⁻ ω, s.indicator 1 ω ∂P := lintegral_mono fun ω ↦ by
+        by_cases hω : ω ∈ s <;> simp [hω, ENNReal.inv_mul_le_one]
+    _ = P s := lintegral_indicator_one (ℱ.le k s hs)
+
+/-- **`ℝ≥0∞`-valued supermartingales are wealth processes** [WSR24, Proposition 3]. An
+`ℝ≥0∞`-valued supermartingale with finite initial expectation under `P` is `P`-almost surely its
+initial value times the product of its successive ratios `M (k + 1) / M k`, with `0 / 0 = 0`;
+these ratios are conditional e-variables (`IsENNSupermartingale.isCondEVar_div`). -/
+theorem IsENNSupermartingale.ae_eq_mul_prod_div (hM : IsENNSupermartingale M ℱ S) (hP : P ∈ S)
+    (h0 : ∫⁻ ω, M 0 ω ∂P ≠ ∞) :
+    ∀ᵐ ω ∂P, ∀ n, M n ω = M 0 ω * ∏ k ∈ range n, M (k + 1) ω / M k ω := by
+  -- almost surely, the process stays at `0` once it reaches it
+  have hzero : ∀ᵐ ω ∂P, ∀ k, M k ω = 0 → M (k + 1) ω = 0 := by
+    refine ae_all_iff.2 fun k ↦ ?_
+    have hs : MeasurableSet[ℱ k] {ω | M k ω = 0} := hM.adapted k (measurableSet_singleton 0)
+    have h : ∫⁻ ω in {ω | M k ω = 0}, M (k + 1) ω ∂P = 0 := by
+      refine le_antisymm ((hM.setLIntegral_succ_le P hP k _ hs).trans_eq ?_) bot_le
+      exact (setLIntegral_eq_zero_iff (ℱ.le k _ hs) (hM.measurable k)).2
+        (ae_of_all _ fun _ hω ↦ hω)
+    exact (setLIntegral_eq_zero_iff (ℱ.le k _ hs) (hM.measurable (k + 1))).1 h
+  filter_upwards [hzero, hM.ae_lt_top hP h0] with ω hz hfin n
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [prod_range_succ, ← mul_assoc, ← ih]
+    rcases eq_or_ne (M n ω) 0 with h | h
+    · simp [h, hz n h]
+    · exact (ENNReal.mul_div_cancel h (hfin n).ne).symm
+
+/-- **Test supermartingales are wealth processes** [WSR24, Proposition 3]. A test supermartingale
+is almost surely, under every member of the null, its initial value times the product of its
+successive ratios `M (k + 1) / M k`, with `0 / 0 = 0`, which are conditional e-variables. -/
+theorem IsTestSupermartingale.ae_eq_mul_prod_div (hM : IsTestSupermartingale M ℱ S)
+    (hP : P ∈ S) :
+    ∀ᵐ ω ∂P, ∀ n, M n ω = M 0 ω * ∏ k ∈ range n, M (k + 1) ω / M k ω :=
+  hM.toIsENNSupermartingale.ae_eq_mul_prod_div hP
+    ((hM.lintegral_zero_le P hP).trans_lt ENNReal.one_lt_top).ne
+
+end ProbabilityTheory
diff --git a/LMLExplore/MeasureTheory/Function/ConditionalExpectation/LebesgueBochner.lean b/LMLExplore/MeasureTheory/Function/ConditionalExpectation/LebesgueBochner.lean
index e48c82f6..629a31cc 100644
--- a/LMLExplore/MeasureTheory/Function/ConditionalExpectation/LebesgueBochner.lean
+++ b/LMLExplore/MeasureTheory/Function/ConditionalExpectation/LebesgueBochner.lean
@@ -5,6 +5,7 @@ Authors: LMLExplore contributors
 -/
 module
 
+public import LMLExplore.MeasureTheory.Measure.WithDensity
 public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
 
 /-!
@@ -38,38 +39,19 @@ theorem lintegral_mul_ofReal_le_of_condExp_le (hm : m ≤ mΩ) [SigmaFinite (μ.
     {f h : Ω → ℝ} (hf : Integrable f μ) (hf_nonneg : 0 ≤ᵐ[μ] f) (hfh : μ[f | m] ≤ᵐ[μ] h)
     {g : Ω → ℝ≥0∞} (hg : Measurable[m] g) :
     ∫⁻ ω, g ω * ENNReal.ofReal (f ω) ∂μ ≤ ∫⁻ ω, g ω * ENNReal.ofReal (h ω) ∂μ := by
-  have hF : AEMeasurable (fun ω ↦ ENNReal.ofReal (f ω)) μ := hf.1.aemeasurable.ennreal_ofReal
-  refine @Measurable.ennreal_induction Ω m
-    (fun g ↦ ∫⁻ ω, g ω * ENNReal.ofReal (f ω) ∂μ ≤ ∫⁻ ω, g ω * ENNReal.ofReal (h ω) ∂μ)
-    (fun c s hs ↦ ?_) (fun g₁ g₂ _ hg₁ _ h₁ h₂ ↦ ?_) (fun g hg hmono ih ↦ ?_) g hg
-  · -- indicators: `∫_s f = ∫_s μ[f | m] ≤ ∫_s h`
-    have hind : ∀ F : Ω → ℝ≥0∞,
-        ∫⁻ ω, s.indicator (fun _ ↦ c) ω * F ω ∂μ = ∫⁻ ω in s, c * F ω ∂μ := fun F ↦ by
-      rw [← lintegral_indicator (hm s hs)]
-      congr 1 with ω
-      by_cases hω : ω ∈ s <;> simp [hω]
-    rw [hind, hind, lintegral_const_mul'' c hF.restrict]
-    refine le_trans ?_ (lintegral_const_mul_le c _)
-    gcongr c * ?_
-    calc ∫⁻ ω in s, ENNReal.ofReal (f ω) ∂μ = ENNReal.ofReal (∫ ω in s, f ω ∂μ) :=
-          (ofReal_integral_eq_lintegral_ofReal hf.integrableOn (ae_restrict_of_ae hf_nonneg)).symm
-      _ = ENNReal.ofReal (∫ ω in s, μ[f | m] ω ∂μ) := by rw [setIntegral_condExp hm hf hs]
-      _ = ∫⁻ ω in s, ENNReal.ofReal (μ[f | m] ω) ∂μ :=
-          ofReal_integral_eq_lintegral_ofReal integrable_condExp.integrableOn
-            (ae_restrict_of_ae (condExp_nonneg hf_nonneg))
-      _ ≤ ∫⁻ ω in s, ENNReal.ofReal (h ω) ∂μ :=
-          lintegral_mono_ae (ae_restrict_of_ae (hfh.mono fun ω hω ↦ ENNReal.ofReal_le_ofReal hω))
-  · -- sums
-    simp only [Pi.add_apply, add_mul]
-    rw [lintegral_add_left' (f := fun ω ↦ g₁ ω * ENNReal.ofReal (f ω))
-      ((hg₁.mono hm le_rfl).aemeasurable.mul hF)]
-    exact (add_le_add h₁ h₂).trans (le_lintegral_add _ _)
-  · -- increasing suprema, by monotone convergence
-    simp only [ENNReal.iSup_mul]
-    rw [lintegral_iSup' (f := fun n ω ↦ g n ω * ENNReal.ofReal (f ω))
-      (fun n ↦ ((hg n).mono hm le_rfl).aemeasurable.mul hF)
-      (ae_of_all _ fun ω n k hnk ↦ by dsimp only; gcongr; exact hmono hnk ω)]
-    exact iSup_le fun n ↦ (ih n).trans
-      (lintegral_mono fun ω ↦ le_iSup (fun i ↦ g i ω * ENNReal.ofReal (h ω)) n)
+  calc ∫⁻ ω, g ω * ENNReal.ofReal (f ω) ∂μ
+      ≤ ∫⁻ ω, g ω * ENNReal.ofReal (μ[f | m] ω) ∂μ :=
+        lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le
+          (f := fun ω ↦ ENNReal.ofReal (f ω)) (g := fun ω ↦ ENNReal.ofReal (μ[f | m] ω)) hm
+          hf.1.aemeasurable.ennreal_ofReal integrable_condExp.1.aemeasurable.ennreal_ofReal
+          (fun s hs ↦ by
+            -- `∫_s f = ∫_s μ[f | m]`, in `ℝ≥0∞`
+            rw [← ofReal_integral_eq_lintegral_ofReal hf.integrableOn
+                (ae_restrict_of_ae hf_nonneg),
+              ← ofReal_integral_eq_lintegral_ofReal integrable_condExp.integrableOn
+                (ae_restrict_of_ae (condExp_nonneg hf_nonneg)),
+              setIntegral_condExp hm hf hs]) hg
+    _ ≤ ∫⁻ ω, g ω * ENNReal.ofReal (h ω) ∂μ :=
+        lintegral_mono_ae (hfh.mono fun ω hω ↦ by gcongr)
 
 end LMLExplore
diff --git a/LMLExplore/MeasureTheory/Measure/WithDensity.lean b/LMLExplore/MeasureTheory/Measure/WithDensity.lean
new file mode 100644
index 00000000..79628bbe
--- /dev/null
+++ b/LMLExplore/MeasureTheory/Measure/WithDensity.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import Mathlib.MeasureTheory.Measure.WithDensity
+
+/-!
+# Comparing densities on a sub-σ-algebra
+
+For a sub-σ-algebra `m` and two densities `f g : Ω → ℝ≥0∞`, the inequality
+`∫⁻ ω in s, f ω ∂μ ≤ ∫⁻ ω in s, g ω ∂μ` for every `m`-measurable `s` says that `f` is at most `g`
+"conditionally on `m`", with no integrability assumption and no conditional expectation. It is the
+inequality `(μ.withDensity f).trim hm ≤ (μ.withDensity g).trim hm` between the restrictions of the
+two measures with densities to `m`, and it extends from indicators to every `m`-measurable weight
+`Y : Ω → ℝ≥0∞`: `∫⁻ Y * f ≤ ∫⁻ Y * g`. This is how a known factor is pulled out of a conditional
+expectation in `ℝ≥0∞`, the step behind every bound on a product of a predictable factor and a
+conditionally bounded increment.
+
+## Main statements
+
+* `MeasureTheory.withDensity_trim_le_withDensity_trim_iff`,
+  `MeasureTheory.withDensity_trim_eq_withDensity_trim_iff`: the set-integral comparisons over the
+  `m`-measurable sets are the comparisons of the trimmed measures with densities.
+* `MeasureTheory.lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le`,
+  `MeasureTheory.lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq`: they extend to
+  `m`-measurable weights.
+-/
+
+public section
+
+open scoped ENNReal
+
+namespace MeasureTheory
+
+variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f g Y : Ω → ℝ≥0∞}
+
+/-- The restrictions to a sub-σ-algebra `m` of `μ.withDensity f` and `μ.withDensity g` compare
+exactly when the set integrals of `f` and `g` over the `m`-measurable sets do. -/
+theorem withDensity_trim_le_withDensity_trim_iff (hm : m ≤ mΩ) :
+    (μ.withDensity f).trim hm ≤ (μ.withDensity g).trim hm ↔
+      ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, f ω ∂μ ≤ ∫⁻ ω in s, g ω ∂μ := by
+  refine (@Measure.le_iff Ω m _ _).trans (forall₂_congr fun s hs ↦ ?_)
+  rw [trim_measurableSet_eq hm hs, trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs),
+    withDensity_apply _ (hm s hs)]
+
+/-- The restrictions to a sub-σ-algebra `m` of `μ.withDensity f` and `μ.withDensity g` are equal
+exactly when the set integrals of `f` and `g` over the `m`-measurable sets are. -/
+theorem withDensity_trim_eq_withDensity_trim_iff (hm : m ≤ mΩ) :
+    (μ.withDensity f).trim hm = (μ.withDensity g).trim hm ↔
+      ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, f ω ∂μ = ∫⁻ ω in s, g ω ∂μ := by
+  refine (@Measure.ext_iff Ω m _ _).trans (forall₂_congr fun s hs ↦ ?_)
+  rw [trim_measurableSet_eq hm hs, trim_measurableSet_eq hm hs, withDensity_apply _ (hm s hs),
+    withDensity_apply _ (hm s hs)]
+
+/-- The integral of `Y * f` against an `m`-measurable weight `Y` is the integral of `Y` against the
+restriction of `μ.withDensity f` to `m`. -/
+theorem lintegral_mul_eq_lintegral_trim_withDensity (hm : m ≤ mΩ) (hf : AEMeasurable f μ)
+    (hY : Measurable[m] Y) :
+    ∫⁻ ω, Y ω * f ω ∂μ = ∫⁻ ω, Y ω ∂(μ.withDensity f).trim hm := by
+  rw [lintegral_trim hm hY, lintegral_withDensity_eq_lintegral_mul₀ hf
+    (hY.mono hm le_rfl).aemeasurable]
+  simp_rw [Pi.mul_apply, mul_comm]
+
+/-- If the set integrals of `f` are at most those of `g` over the `m`-measurable sets, then
+`∫⁻ Y * f ≤ ∫⁻ Y * g` for every `m`-measurable `Y : Ω → ℝ≥0∞`: the factor `Y`, known given `m`,
+can be pulled out. -/
+theorem lintegral_mul_le_lintegral_mul_of_forall_setLIntegral_le (hm : m ≤ mΩ)
+    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    (h : ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, f ω ∂μ ≤ ∫⁻ ω in s, g ω ∂μ)
+    (hY : Measurable[m] Y) :
+    ∫⁻ ω, Y ω * f ω ∂μ ≤ ∫⁻ ω, Y ω * g ω ∂μ := by
+  rw [lintegral_mul_eq_lintegral_trim_withDensity hm hf hY,
+    lintegral_mul_eq_lintegral_trim_withDensity hm hg hY]
+  exact lintegral_mono' ((withDensity_trim_le_withDensity_trim_iff hm).2 h) le_rfl
+
+/-- If the set integrals of `f` and `g` agree over the `m`-measurable sets, then
+`∫⁻ Y * f = ∫⁻ Y * g` for every `m`-measurable `Y : Ω → ℝ≥0∞`. -/
+theorem lintegral_mul_eq_lintegral_mul_of_forall_setLIntegral_eq (hm : m ≤ mΩ)
+    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    (h : ∀ s, MeasurableSet[m] s → ∫⁻ ω in s, f ω ∂μ = ∫⁻ ω in s, g ω ∂μ)
+    (hY : Measurable[m] Y) :
+    ∫⁻ ω, Y ω * f ω ∂μ = ∫⁻ ω, Y ω * g ω ∂μ := by
+  rw [lintegral_mul_eq_lintegral_trim_withDensity hm hf hY,
+    lintegral_mul_eq_lintegral_trim_withDensity hm hg hY,
+    (withDensity_trim_eq_withDensity_trim_iff hm).2 h]
+
+end MeasureTheory
diff --git a/LMLExplore/Probability/Process/Adapted.lean b/LMLExplore/Probability/Process/Adapted.lean
new file mode 100644
index 00000000..414d3d5a
--- /dev/null
+++ b/LMLExplore/Probability/Process/Adapted.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import Mathlib.Probability.Process.Adapted
+
+/-!
+# Adapted products
+
+A product `M₀ * ∏ k < n, F k` is adapted to a filtration `ℱ` indexed by `ℕ` when `M₀` is
+`ℱ 0`-measurable and each factor `F k` is `ℱ (k + 1)`-measurable. Such products are the wealth
+processes of a gambler who reinvests at every round.
+
+## Main statements
+
+* `MeasureTheory.adapted_mul_prod_range`: the process `n ↦ M₀ * ∏ k < n, F k` is adapted.
+-/
+
+public section
+
+open Finset
+
+namespace MeasureTheory
+
+variable {Ω β : Type*} {mΩ : MeasurableSpace Ω} [MeasurableSpace β] [CommMonoid β]
+  [MeasurableMul₂ β] {ℱ : Filtration ℕ mΩ}
+
+/-- The process `n ↦ M₀ * ∏ k < n, F k` is adapted when `M₀` is `ℱ 0`-measurable and each factor
+`F k` is `ℱ (k + 1)`-measurable. -/
+theorem adapted_mul_prod_range {M₀ : Ω → β} (hM₀ : Measurable[ℱ 0] M₀) {F : ℕ → Ω → β}
+    (hF : ∀ k, Measurable[ℱ (k + 1)] (F k)) :
+    Adapted ℱ (fun n ω ↦ M₀ ω * ∏ k ∈ range n, F k ω) := fun n ↦
+  (hM₀.mono (ℱ.mono n.zero_le) le_rfl).mul <| Finset.measurable_fun_prod _ fun k hk ↦
+    (hF k).mono (ℱ.mono (mem_range.1 hk)) le_rfl
+
+end MeasureTheory