diff --git a/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean b/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean
new file mode 100644
index 00000000..74c50198
--- /dev/null
+++ b/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.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.Analysis.SpecialFunctions.Log.PosLog
+public import Mathlib.MeasureTheory.Function.L1Space.Integrable
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+import LMLExplore.Analysis.SpecialFunctions.Log.Basic
+import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
+import Mathlib.MeasureTheory.Integral.DominatedConvergence
+
+/-!
+# Integrability of `log (1 + ∑ i, |f i|)`
+
+Finitely many real functions whose positive logarithms `log⁺ (f i)` are integrable under a finite
+measure have an integrable `log (1 + ∑ i, |f i|)`, and damping the sum by a factor in `[0, 1]`
+keeps the integrability. As the damping factor tends to `0`, so does the integral of the damped
+logarithm, by dominated convergence.
+
+## Main statements
+
+* `MeasureTheory.integrable_log_one_add_sum_abs`: if every `log⁺ (f i)` is integrable under a
+  finite measure, so is `log (1 + ∑ i, |f i|)`.
+* `MeasureTheory.Integrable.log_one_add_const_mul`: if `log (1 + f)` is integrable for a
+  nonnegative `f`, so is `log (1 + δ f)` for `δ ∈ [0, 1]`.
+* `MeasureTheory.Integrable.tendsto_integral_log_one_add_mul`: if `log (1 + f)` is integrable for
+  a nonnegative `f`, then `∫ log (1 + δ f)` tends to `0` as `δ ≥ 0` tends to `0`.
+-/
+
+public section
+
+open MeasureTheory Filter Topology
+
+namespace MeasureTheory
+
+variable {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
+
+/-- If every `log⁺ (f i)` is integrable under a finite measure, so is `log (1 + ∑ i, |f i|)`. -/
+theorem integrable_log_one_add_sum_abs [Fintype ι] [IsFiniteMeasure μ] {f : ι → α → ℝ}
+    (hf : ∀ i, AEMeasurable (f i) μ) (h : ∀ i, Integrable (fun x ↦ Real.posLog (f i x)) μ) :
+    Integrable (fun x ↦ Real.log (1 + ∑ i, |f i x|)) μ := by
+  have hint : Integrable
+      (fun x ↦ Real.log (Fintype.card ι) + ∑ i, Real.posLog (f i x) + Real.log 2) μ :=
+    ((integrable_const _).add (integrable_finsetSum _ fun i _ ↦ h i)).add (integrable_const _)
+  have hm : AEMeasurable (fun x ↦ Real.log (1 + ∑ i, |f i x|)) μ := by fun_prop
+  refine hint.mono' hm.aestronglyMeasurable (ae_of_all _ fun x ↦ ?_)
+  have hsum : 0 ≤ ∑ i, |f i x| := Finset.sum_nonneg fun i _ ↦ abs_nonneg _
+  rw [Real.norm_of_nonneg (Real.log_nonneg (by linarith))]
+  refine Real.log_one_add_le_posLog.trans ?_
+  gcongr
+  simpa using Real.posLog_sum Finset.univ fun i ↦ |f i x|
+
+/-- If `log (1 + f)` is integrable for a nonnegative `f`, so is `log (1 + δ f)` for
+`δ ∈ [0, 1]`. -/
+theorem Integrable.log_one_add_const_mul {f : α → ℝ}
+    (h : Integrable (fun x ↦ Real.log (1 + f x)) μ) (hfm : AEMeasurable f μ) (hf : ∀ x, 0 ≤ f x)
+    {δ : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) :
+    Integrable (fun x ↦ Real.log (1 + δ * f x)) μ := by
+  have hm : AEMeasurable (fun x ↦ Real.log (1 + δ * f x)) μ := by fun_prop
+  refine h.mono' hm.aestronglyMeasurable (ae_of_all _ fun x ↦ ?_)
+  rw [Real.norm_eq_abs]
+  exact Real.abs_log_one_add_mul_le hδ hδ1 (hf x)
+
+/-- If `log (1 + f)` is integrable for a nonnegative `f`, then `∫ log (1 + δ f)` tends to `0` as
+the damping factor `δ ≥ 0` tends to `0`, by dominated convergence. -/
+theorem Integrable.tendsto_integral_log_one_add_mul {f : α → ℝ}
+    (h : Integrable (fun x ↦ Real.log (1 + f x)) μ) (hfm : AEMeasurable f μ) (hf : ∀ x, 0 ≤ f x)
+    {β : Type*} {l : Filter β} [l.IsCountablyGenerated] {δ : β → ℝ} (hδ : Tendsto δ l (𝓝 0))
+    (hδ0 : ∀ᶠ n in l, 0 ≤ δ n) :
+    Tendsto (fun n ↦ ∫ x, Real.log (1 + δ n * f x) ∂μ) l (𝓝 0) := by
+  rw [← integral_zero α ℝ (μ := μ)]
+  refine tendsto_integral_filter_of_dominated_convergence _
+    (.of_forall fun n ↦ (by fun_prop : AEMeasurable (fun x ↦ Real.log (1 + δ n * f x)) μ)
+      |>.aestronglyMeasurable)
+    ((hδ0.and (hδ.eventually (ge_mem_nhds one_pos))).mono fun n hn ↦ ae_of_all _ fun x ↦ ?_) h
+    (ae_of_all _ fun x ↦ ?_)
+  · rw [Real.norm_eq_abs]
+    exact Real.abs_log_one_add_mul_le hn.1 hn.2 (hf x)
+  · have : Tendsto (fun n ↦ 1 + δ n * f x) l (𝓝 1) := by
+      simpa using (hδ.mul_const (f x)).const_add 1
+    simpa [Function.comp_def] using (Real.continuousAt_log one_ne_zero).tendsto.comp this
+
+end MeasureTheory
diff --git a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean
index 01d032c0..02e0c2c6 100644
--- a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean
+++ b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean
@@ -67,6 +67,7 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv
   RF-Express [MDJKLV21].
 * `Real.sum_div_max_one_le_four_mul_log`: the form of [MDJKLV21, Lemma 9], for `u k ∈ [0, 1]`
   and with the constant `4`.
+* `Real.abs_log_one_add_mul_le`: `|log (1 + δ t)| ≤ log (1 + t)` for `t ≥ 0` and `δ ∈ [0, 1]`.
 * `Real.tendsto_sub_one_sub_log_atTop`, `Real.tendsto_sub_one_sub_log_nhdsGT_zero`:
   `t - 1 - log t → ∞` as `t → ∞` and as `t → 0⁺`. The divergences of the Poisson and gamma
   families are multiples of this function of a ratio of means.
@@ -674,4 +675,12 @@ theorem tendsto_sub_one_sub_log_nhdsGT_zero :
   simp only [Function.comp_apply]
   linarith
 
+/-- Damping by a factor `δ ∈ [0, 1]` decreases `log (1 + t)`, for `t ≥ 0`, and keeps it
+nonnegative. -/
+theorem abs_log_one_add_mul_le {δ t : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (ht : 0 ≤ t) :
+    |log (1 + δ * t)| ≤ log (1 + t) := by
+  have h0 : 0 ≤ δ * t := mul_nonneg hδ ht
+  rw [abs_of_nonneg (log_nonneg (by linarith))]
+  exact log_le_log (by linarith) (by nlinarith)
+
 end Real
diff --git a/LMLExplore/EValues/ConstraintNull/Basic.lean b/LMLExplore/EValues/ConstraintNull/Basic.lean
index c60f0231..e52146bf 100644
--- a/LMLExplore/EValues/ConstraintNull/Basic.lean
+++ b/LMLExplore/EValues/ConstraintNull/Basic.lean
@@ -90,6 +90,11 @@ theorem isProbabilityMeasure_of_mem_constraintNull (hμ : μ ∈ constraintNull
     IsProbabilityMeasure μ :=
   hμ.1
 
+/-- The members of the null generated by constraints are finite measures. -/
+theorem isFiniteMeasure_of_mem_constraintNull (hμ : μ ∈ constraintNull Φ) : IsFiniteMeasure μ :=
+  have := isProbabilityMeasure_of_mem_constraintNull hμ
+  inferInstance
+
 /-- The members of the null generated by constraints integrate the constraints. -/
 theorem integrable_of_mem_constraintNull (hμ : μ ∈ constraintNull Φ) (hf : f ∈ Φ) :
     Integrable f μ :=
@@ -219,6 +224,15 @@ theorem mem_constraintBets_iff :
       ∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ 1 + ∑ i, (π i : ℝ) * g i x :=
   Iff.rfl
 
+/-- Nonnegative real weights `ρ` give a bet as soon as `1 + ∑ i, ρ i * g i` is nonnegative on a
+set `Y` that carries every member of the null. -/
+theorem toNNReal_mem_constraintBets {Y : Set 𝓧} (hYμ : ∀ μ ∈ constraintNull (range g), μ Yᶜ = 0)
+    {ρ : ι → ℝ} (hρ : ∀ i, 0 ≤ ρ i) (hρY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, ρ i * g i x) :
+    (fun i ↦ (ρ i).toNNReal) ∈ constraintBets g :=
+  mem_constraintBets_iff.2 fun μ hμ ↦
+    Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ by
+      simpa only [Real.coe_toNNReal _ (hρ _)] using hρY x hx
+
 /-- The zero bet, which keeps the wealth at `1`. -/
 @[simp]
 theorem zero_mem_constraintBets : 0 ∈ constraintBets g :=
diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean
index 9d9125de..c4240ea4 100644
--- a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean
+++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean
@@ -74,12 +74,21 @@ supported member of the null, so that e-variables are finite on `Y`.
   arbitrage.
 * `ProbabilityTheory.forall_integral_nonpos_iff_exists_ae_le`: **the complete class theorem**
   [LRR26, Theorem 3.1].
-* `ProbabilityTheory.IsEVar.exists_mem_constraintBets_ae_le`,
+* `ProbabilityTheory.IsEVar.exists_mem_constraintBets_le_of_noArbitrageOn`,
+  `ProbabilityTheory.IsEVar.exists_mem_constraintBets_ae_le`,
   `ProbabilityTheory.isEVar_constraintNull_iff`: the complete class theorem for e-variables
-  [LRR26, Theorem 3.1]: every e-variable is dominated by a bet.
+  [LRR26, Theorem 3.1]: every e-variable is dominated by a bet, on a set without arbitrage that
+  carries the null, and almost surely under every member of the null.
+* `ProbabilityTheory.noArbitrageOn_add_integral_div_of_lintegral_le`,
+  `ProbabilityTheory.exists_add_sum_smul_dirac_mem_constraintNull`: on a nonempty set without
+  arbitrage that carries the null, a finite measure carried by that set that integrates the
+  constraints and under which every e-variable has mean at most `c < 1` is completed into a member
+  of the null by a finitely supported measure [EVR26, Note 20].
 
 ## References
 
+* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, notes 01–34 and the
+  Lean library EValuesResearch, github.com/RemyDegenne/evalues_research (2026).
 * [LRR26] M. Larsson, A. Ramdas and J. Ruf, *Testing hypotheses generated by constraints*, Math.
   Oper. Res. (2026), arXiv:2504.02974v5.
 -/
@@ -599,6 +608,19 @@ theorem forall_integral_nonpos_iff_exists_ae_le (hg : ∀ i, Measurable (g i))
         (integral_sum_mul_nonpos_of_mem_constraintNull hμ fun i ↦ (π i).coe_nonneg)
     · rw [integral_undef hfi]
 
+/-- **The complete class theorem for e-variables on a set without arbitrage** [LRR26,
+Theorem 3.1]: on a set `Y` without arbitrage that carries the null, every e-variable for the null
+is at most a bet `1 + ∑ i, π i * g i`. -/
+theorem IsEVar.exists_mem_constraintBets_le_of_noArbitrageOn (hg : ∀ i, Measurable (g i))
+    (hY : NoArbitrageOn g Y) (hYμ : ∀ μ ∈ constraintNull (range g), μ Yᶜ = 0)
+    (hE : IsEVar E (constraintNull (range g))) :
+    ∃ π ∈ constraintBets g, ∀ x ∈ Y, E x ≤ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) := by
+  obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_toReal_le_of_isEVar hg hY hE
+  refine ⟨fun i ↦ (π i).toNNReal, toNNReal_mem_constraintBets hYμ hπK.1 fun x hx ↦
+    ENNReal.toReal_nonneg.trans (hπ x hx), fun x hx ↦ ?_⟩
+  rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hE hx).ne]
+  simpa only [Real.coe_toNNReal _ (hπK.1 _)] using ENNReal.ofReal_le_ofReal (hπ x hx)
+
 /-- **The complete class theorem for e-variables** [LRR26, Theorem 3.1]: every e-variable for the
 null generated by finitely many measurable constraints `g i` is dominated by a bet
 `1 + ∑ i, π i * g i`, almost surely under every member of the null. -/
@@ -607,15 +629,8 @@ theorem IsEVar.exists_mem_constraintBets_ae_le (hg : ∀ i, Measurable (g i))
     ∃ π ∈ constraintBets g, ∀ μ ∈ constraintNull (range g),
       E ≤ᵐ[μ] fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) := by
   obtain ⟨Y, -, hYμ, hY⟩ := exists_measurableSet_noArbitrageOn hg
-  obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_toReal_le_of_isEVar hg hY hE
-  have hπY : ∀ x ∈ Y, (E x).toReal ≤ 1 + ∑ i, ((π i).toNNReal : ℝ) * g i x := fun x hx ↦ by
-    simpa only [Real.coe_toNNReal _ (hπK.1 _)] using hπ x hx
-  refine ⟨fun i ↦ (π i).toNNReal, mem_constraintBets_iff.2 fun μ hμ ↦
-    Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦
-      ENNReal.toReal_nonneg.trans (hπY x hx), fun μ hμ ↦
-    Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ ?_⟩
-  rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hE hx).ne]
-  exact ENNReal.ofReal_le_ofReal (hπY x hx)
+  obtain ⟨π, hπ, hπY⟩ := hE.exists_mem_constraintBets_le_of_noArbitrageOn hg hY hYμ
+  exact ⟨π, hπ, fun μ hμ ↦ Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) hπY⟩
 
 /-- **The e-variables for a null generated by finitely many constraints** [LRR26, Theorem 3.1]:
 for measurable constraints `g i`, the e-variables for the null are the measurable functions that
@@ -628,4 +643,124 @@ theorem isEVar_constraintNull_iff (hg : ∀ i, Measurable (g i)) :
       fun μ hμ ↦ (lintegral_mono_ae (hEπ μ hμ)).trans
         (lintegral_ofReal_one_add_le_one_of_mem_constraintBets hπ hμ)⟩
 
+/-! ### Completion into a member of the null -/
+
+/-- **The shifted constraints admit no arbitrage**: on a set `Y` without arbitrage that carries
+the null, let `μ` be a finite measure carried by `Y` that integrates the constraints and under
+which every e-variable has mean at most `c`, for some `c < 1`. Then the constraints shifted by
+their means under `μ` divided by the mass `1 - μ 𝓧` that `μ` lacks,
+`g i + (∫ g i ∂μ) / (1 - μ 𝓧)`, admit no arbitrage on `Y`. -/
+theorem noArbitrageOn_add_integral_div_of_lintegral_le (hg : ∀ i, Measurable (g i))
+    (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0)
+    {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) (hgμ : ∀ i, Integrable (g i) μ)
+    {c : ℝ≥0∞} (hc : c < 1)
+    (hμE : ∀ E, IsEVar E (constraintNull (range g)) → ∫⁻ x, E x ∂μ ≤ c) :
+    NoArbitrageOn (fun i x ↦ g i x + (∫ y, g i y ∂μ) / (1 - μ.real univ)) Y := by
+  set m := 1 - μ.real univ with hm_def
+  refine noArbitrageOn_iff.2 fun π hπ hπY ↦ ?_
+  set σ := (∑ i, π i * ∫ x, g i x ∂μ) / m with hσ_def
+  have hσa : ∑ i, π i * ((∫ x, g i x ∂μ) / m) = σ := by
+    simp only [hσ_def, Finset.sum_div, mul_div_assoc]
+  have hπg : ∀ x ∈ Y, -σ ≤ ∑ i, π i * g i x := by
+    intro x hx
+    have := hπY x hx
+    simp only [mul_add, Finset.sum_add_distrib, hσa] at this
+    linarith
+  rcases lt_or_ge 0 σ with hσ | hσ
+  · -- a positive deficit would be paid by the mass that `μ` lacks: the bet with weights `π / σ`
+    -- would have mean `1` under `μ`
+    exfalso
+    have hsum : ∀ x, ∑ i, π i / σ * g i x = (∑ i, π i * g i x) / σ := fun x ↦ by
+      simp only [Finset.sum_div, div_mul_eq_mul_div]
+    have hEY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i / σ * g i x := by
+      intro x hx
+      rw [hsum]
+      have : -1 ≤ (∑ i, π i * g i x) / σ := by
+        rw [le_div_iff₀ hσ]
+        linarith [hπg x hx]
+      linarith
+    have hcoe : ∀ i, ((π i / σ).toNNReal : ℝ) = π i / σ := fun i ↦
+      Real.coe_toNNReal _ (div_nonneg (hπ i) hσ.le)
+    have h1 := hμE _ (isEVar_ofReal_one_add_of_mem_constraintBets hg
+      (toNNReal_mem_constraintBets hYμ (fun i ↦ div_nonneg (hπ i) hσ.le) hEY))
+    simp only [hcoe] at h1
+    rw [lintegral_ofReal_one_add_sum_mul hgμ _
+      (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hEY)] at h1
+    have h2 : ∑ i, π i / σ * ∫ x, g i x ∂μ = m := by
+      have : ∑ i, π i / σ * ∫ x, g i x ∂μ = (∑ i, π i * ∫ x, g i x ∂μ) / σ := by
+        simp only [Finset.sum_div, div_mul_eq_mul_div]
+      rw [this, hσ_def, div_div_cancel₀ (by
+        intro h0
+        rw [h0, zero_div] at hσ_def
+        exact hσ.ne' hσ_def)]
+    rw [h2, hm_def, add_sub_cancel, ENNReal.ofReal_one] at h1
+    exact lt_irrefl _ (h1.trans_lt hc)
+  · -- no deficit: the combination is nonnegative, hence zero, on `Y`
+    have h0 : ∀ x ∈ Y, 0 ≤ ∑ i, π i * g i x := fun x hx ↦ by linarith [hπg x hx]
+    have hzero := noArbitrageOn_iff.1 hY π hπ h0
+    have hb : ∑ i, π i * ∫ x, g i x ∂μ = 0 := by
+      have hgi : ∀ i, Integrable (fun x ↦ π i * g i x) μ := fun i ↦ (hgμ i).const_mul (π i)
+      simp_rw [← integral_const_mul]
+      rw [← integral_finsetSum _ fun i _ ↦ hgi i]
+      exact integral_eq_zero_of_ae (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hzero)
+    have hσ0 : σ = 0 := by rw [hσ_def, hb, zero_div]
+    intro x hx
+    simp only [mul_add, Finset.sum_add_distrib, hσa, hσ0, add_zero]
+    exact hzero x hx
+
+/-- **Completion by a finitely supported measure**: on a nonempty set `Y` without arbitrage that
+carries the null, a finite measure carried by `Y` that integrates the constraints and under which
+every e-variable has mean at most `c`, for some `c < 1`, becomes a member of the null once a
+finitely supported measure is added. It rests on the complete class theorem [LRR26, Theorem 3.1],
+and follows [EVR26, Note 20]. -/
+theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g i))
+    (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0)
+    (hYne : Y.Nonempty) {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0)
+    (hgμ : ∀ i, Integrable (g i) μ) {c : ℝ≥0∞} (hc : c < 1)
+    (hμE : ∀ E, IsEVar E (constraintNull (range g)) → ∫⁻ x, E x ∂μ ≤ c) :
+    ∃ (α : Type) (_ : Fintype α) (x : α → 𝓧) (w : α → ℝ), (∀ k, 0 ≤ w k) ∧
+      μ + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) ∈ constraintNull (range g) := by
+  classical
+  set r := μ.real univ with hr_def
+  set m := 1 - r with hm_def
+  have hm0 : 0 < m := by
+    have h1 := hμE 1 (isEVar_one _)
+    simp only [Pi.one_apply, lintegral_one] at h1
+    have h2 : r < 1 := by
+      rw [hr_def, measureReal_def]
+      exact ENNReal.toReal_lt_of_lt_ofReal (by simpa using h1.trans_lt hc)
+    linarith
+  -- the complete class theorem, applied to the constraints shifted by multiples of their means
+  -- under `μ`, gives a finitely supported law under which the shifted constraints have
+  -- nonpositive means
+  obtain ⟨x₀, hx₀⟩ := hYne
+  obtain ⟨α, _, x, w, -, hw, hwz, -⟩ := exists_charging_family_of_noArbitrageOn
+    (noArbitrageOn_add_integral_div_of_lintegral_le hg hY hYμ hμY hgμ hc hμE) hx₀
+  obtain ⟨hw0, hw1⟩ := mem_simplex_iff.1 hw
+  refine ⟨α, inferInstance, x, fun k ↦ m * w k, fun k ↦ mul_nonneg hm0.le (hw0 k), ?_⟩
+  have hdirac : ∀ (f : 𝓧 → ℝ), Measurable f → ∀ k ∈ Finset.univ,
+      Integrable f (ENNReal.ofReal (m * w k) • Measure.dirac (x k)) := fun f hf k _ ↦
+    (integrable_dirac' hf.stronglyMeasurable (by simp)).smul_measure ENNReal.ofReal_ne_top
+  refine mem_constraintNull_range_iff.2 ⟨⟨?_⟩, fun i ↦ ?_⟩
+  · simp only [add_apply, sum_apply, smul_apply, measure_univ, smul_eq_mul, mul_one]
+    -- the added mass is `m = 1 - r`, the mass that `μ` lacks
+    have hmass : ∑ k, ENNReal.ofReal (m * w k) = ENNReal.ofReal m := by
+      rw [← ENNReal.ofReal_sum_of_nonneg fun k _ ↦ mul_nonneg hm0.le (hw0 k), ← Finset.mul_sum,
+        hw1, mul_one]
+    rw [hmass, ← ofReal_measureReal, ← hr_def, ← ENNReal.ofReal_add measureReal_nonneg hm0.le,
+      hm_def, add_sub_cancel, ENNReal.ofReal_one]
+  · refine ⟨(hgμ i).add_measure (integrable_finsetSum_measure.2 (hdirac _ (hg i))), ?_⟩
+    rw [integral_add_measure (hgμ i) (integrable_finsetSum_measure.2 (hdirac _ (hg i))),
+      integral_sum_smul_dirac (fun k ↦ mul_nonneg hm0.le (hw0 k)) (hg i).stronglyMeasurable]
+    simp_rw [smul_eq_mul]
+    have h1 := hwz i
+    simp only [mul_add, Finset.sum_add_distrib, ← Finset.sum_mul, hw1, one_mul] at h1
+    have h2 : ∑ k, m * w k * g i (x k) = m * ∑ k, w k * g i (x k) := by
+      rw [Finset.mul_sum]
+      exact Finset.sum_congr rfl fun k _ ↦ by ring
+    have h3 : m * ((∫ x, g i x ∂μ) / m) = ∫ x, g i x ∂μ := by
+      field_simp
+    rw [h2]
+    nlinarith
+
 end ProbabilityTheory
diff --git a/LMLExplore/EValues/ConstraintNull/KLInf.lean b/LMLExplore/EValues/ConstraintNull/KLInf.lean
new file mode 100644
index 00000000..720cfc4c
--- /dev/null
+++ b/LMLExplore/EValues/ConstraintNull/KLInf.lean
@@ -0,0 +1,455 @@
+/-
+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.ConstraintNull.CompleteClass
+public import Mathlib.Analysis.SpecialFunctions.Log.PosLog
+public import Statlib.EValues.RIPr
+import LMLExplore.Analysis.SpecialFunctions.Integrability.PosLog
+import LMLExplore.MeasureTheory.Measure.MeasureSpaceDef
+
+/-!
+# The dual formula for the smallest relative entropy to a null generated by constraints
+
+Let `g i`, for `i` in a finite type, be measurable real constraints on a measurable space `𝓧`, and
+`Q` a probability measure on `𝓧`. The smallest relative entropy from `Q` to the null
+`constraintNull (range g)`, written $\mathrm{KL}_{\inf}$ in the bandit literature, is the largest
+expected logarithm under `Q` of an e-variable for the null, and of a bet `1 + ∑ i, π i * g i`:
+$$\inf_{P}\mathrm{KL}(Q,P)=\sup_{\pi}\mathbb E_Q\log\Big(1+\sum_i\pi_ig_i\Big)
+=\texttt{maxUtility Q (constraintNull (range g)) logUtility}.$$
+The second equality holds for every finite measure `Q`. The first holds as soon as every
+`log⁺ |g i|` is `Q`-integrable, with no constraint qualification: no member of the null is asked
+to satisfy the constraints strictly, the null may be empty, and both sides may be infinite.
+
+The formulas of Honda and Takemura for one mean constraint on the laws on `[0, 1]` and on
+`(-∞, 1]` [HT15] are cases of it, which this file does not derive. The statements and the proof
+follow [EVR26, Note 20], whose Lean library EValuesResearch proves them; the proofs here are
+adapted from it. The proof does not go through
+Lagrange duality, which needs Slater's condition. It compares both sides with the largest expected
+logarithm of an e-variable, which Statlib's numeraire [LRR25] attains, and splits along
+`exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos`.
+
+* If a nonnegative combination of the constraints is nonnegative almost surely under the null and
+  under `Q`, and positive on a set of positive `Q`-measure, its multiples are bets with unbounded
+  expected logarithms, and the three quantities are infinite.
+* Otherwise a measurable set `Y` carries the null and `Q`, and the constraints admit no arbitrage
+  on `Y`. On `Y` every e-variable is at most a bet, by the complete class theorem
+  [LRR26, Theorem 3.1], which gives the second equality. For the
+  first, let `E` be the numeraire. The measure with density `1 / E` with respect to `Q`, the
+  reverse information projection [LRR25], is damped by `1 + δ ∑ i, |g i|`, so that it integrates the
+  constraints, and scaled by `1 - ε`. It is then completed into a member of the null by a finitely
+  supported measure on `Y`: the complete class theorem [LRR26, Theorem 3.1], applied to the
+  constraints shifted by their means under the damped projection, gives the points and the
+  weights. The relative entropy
+  from `Q` to that member of the null is at most the largest expected logarithm plus
+  `E_Q[log (1 + δ ∑ i, |g i|)] - log (1 - ε)`, which tends to `0` with `δ` and `ε`.
+
+## Main statements
+
+* `ProbabilityTheory.maxUtility_constraintNull_eq_iSup_eintegral_log`: the largest expected
+  logarithm of an e-variable for the null equals the supremum of the expected logarithms of the
+  bets.
+* `ProbabilityTheory.iInf_klDiv_constraintNull_eq_maxUtility`: the smallest relative entropy to
+  the null is the largest expected logarithm of an e-variable.
+* `ProbabilityTheory.iInf_klDiv_constraintNull_eq_iSup_eintegral_log`: **the dual formula**.
+
+## References
+
+* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, notes 01–34 and the
+  Lean library EValuesResearch, github.com/RemyDegenne/evalues_research (2026).
+* [HT15] J. Honda and A. Takemura, *Non-asymptotic analysis of a new bandit algorithm for
+  semi-bounded rewards*, J. Mach. Learn. Res. 16 (2015).
+* [LRR25] M. Larsson, A. Ramdas and J. Ruf, *The numeraire e-variable and reverse information
+  projection*, Ann. Statist. 53 (2025), arXiv:2402.18810.
+* [LRR26] M. Larsson, A. Ramdas and J. Ruf, *Testing hypotheses generated by constraints*, Math.
+  Oper. Res. (2026), arXiv:2504.02974v5.
+-/
+
+public section
+
+open MeasureTheory Set InformationTheory LMLExplore
+open scoped ENNReal NNReal
+
+namespace ProbabilityTheory
+
+variable {𝓧 ι : Type*} [Fintype ι] [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {Y : Set 𝓧}
+  {Q : Measure 𝓧}
+
+/-! ### The damped reverse information projection -/
+
+/-- The density with respect to `Q` of the reverse information projection `Q / E` damped by
+`1 + δ ∑ i, |g i|` and scaled by `1 - ε`: `x ↦ (1 - ε) / (E x * (1 + δ ∑ i, |g i x|))`. -/
+private noncomputable def dampedDensity (E : 𝓧 → ℝ≥0∞) (g : ι → 𝓧 → ℝ) (δ ε : ℝ) (x : 𝓧) :
+    ℝ≥0∞ :=
+  (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))
+
+private lemma measurable_dampedDensity {E : 𝓧 → ℝ≥0∞} (hE : Measurable E)
+    (hg : ∀ i, Measurable (g i)) (δ ε : ℝ) : Measurable (dampedDensity E g δ ε) := by
+  unfold dampedDensity
+  fun_prop
+
+omit [MeasurableSpace 𝓧] in
+private lemma dampedDensity_ne_zero {E : 𝓧 → ℝ≥0∞} {δ ε : ℝ} (hδ : 0 ≤ δ) (hε1 : ε < 1) {x : 𝓧}
+    (hx : E x ≠ ∞) : dampedDensity E g δ ε x ≠ 0 := by
+  simp only [dampedDensity, ne_eq, mul_eq_zero, ENNReal.inv_eq_zero, hx, ENNReal.ofReal_eq_zero,
+    not_le, false_or]
+  exact div_pos (by linarith) (by positivity)
+
+/-- The reverse information projection `Q / E` damped by `1 + δ ∑ i, |g i|` and scaled by `1 - ε`
+integrates the constraints, as soon as `∫ 1 / E ∂Q` is finite. -/
+private lemma integrable_withDensity_inv_mul_ofReal_div {E : 𝓧 → ℝ≥0∞} (hE : Measurable E)
+    (hg : ∀ i, Measurable (g i)) (hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≠ ∞) {δ ε : ℝ} (hδ : 0 < δ)
+    (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (i : ι) :
+    Integrable (g i) (Q.withDensity (dampedDensity E g δ ε)) := by
+  refine ⟨(hg i).aestronglyMeasurable, ?_⟩
+  rw [HasFiniteIntegral, lintegral_withDensity_eq_lintegral_mul _
+    (measurable_dampedDensity hE hg δ ε) (by fun_prop)]
+  calc ∫⁻ x, (dampedDensity E g δ ε * fun x ↦ ‖g i x‖ₑ) x ∂Q
+      ≤ ∫⁻ x, ENNReal.ofReal (1 / δ) * (E x)⁻¹ ∂Q := by
+        refine lintegral_mono fun x ↦ ?_
+        have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by positivity
+        have hgi : |g i x| ≤ ∑ j, |g j x| :=
+          Finset.single_le_sum (f := fun j ↦ |g j x|) (fun j _ ↦ abs_nonneg _)
+            (Finset.mem_univ i)
+        have h1 : (1 - ε) / (1 + δ * ∑ j, |g j x|) * |g i x| ≤ 1 / δ := by
+          rw [div_mul_eq_mul_div, div_le_div_iff₀ hh0 hδ, one_mul]
+          have h2 : (1 - ε) * |g i x| * δ ≤ δ * |g i x| := by
+            nlinarith [mul_nonneg (mul_nonneg hε hδ.le) (abs_nonneg (g i x))]
+          have h3 : δ * |g i x| ≤ δ * ∑ j, |g j x| := mul_le_mul_of_nonneg_left hgi hδ.le
+          linarith
+        calc (dampedDensity E g δ ε * fun x ↦ ‖g i x‖ₑ) x
+            = (E x)⁻¹ * (ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) * ‖g i x‖ₑ) := by
+              simp only [Pi.mul_apply, dampedDensity, mul_assoc]
+          _ = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|) * |g i x|) := by
+              rw [Real.eNorm_eq_ofReal_abs, ← ENNReal.ofReal_mul
+                (div_nonneg (by linarith) hh0.le)]
+          _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 / δ) := by gcongr
+          _ = ENNReal.ofReal (1 / δ) * (E x)⁻¹ := mul_comm _ _
+    _ = ENNReal.ofReal (1 / δ) * ∫⁻ x, (E x)⁻¹ ∂Q :=
+        lintegral_const_mul' _ _ ENNReal.ofReal_ne_top
+    _ < ⊤ := ENNReal.mul_lt_top ENNReal.ofReal_lt_top hEinv.lt_top
+
+/-- The mean of a function under the damped and scaled reverse information projection is at most
+`1 - ε` times its mean divided by `E` under `Q`. -/
+private lemma lintegral_withDensity_inv_mul_ofReal_div_le {E F : 𝓧 → ℝ≥0∞} (hE : Measurable E)
+    (hF : Measurable F) (hg : ∀ i, Measurable (g i)) {δ ε : ℝ} (hδ : 0 ≤ δ) (hε1 : ε ≤ 1) :
+    ∫⁻ x, F x ∂(Q.withDensity (dampedDensity E g δ ε))
+      ≤ ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q := by
+  rw [lintegral_withDensity_eq_lintegral_mul _ (measurable_dampedDensity hE hg δ ε) hF,
+    ← lintegral_const_mul' _ _ ENNReal.ofReal_ne_top]
+  refine lintegral_mono fun x ↦ ?_
+  have : ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) ≤ ENNReal.ofReal (1 - ε) :=
+    ENNReal.ofReal_le_ofReal (div_le_self (by linarith) (le_add_of_nonneg_right (by positivity)))
+  calc (dampedDensity E g δ ε * F) x
+      = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) * F x := by
+        simp only [Pi.mul_apply, dampedDensity]
+    _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 - ε) * F x := by gcongr
+    _ = ENNReal.ofReal (1 - ε) * (F x / E x) := by rw [div_eq_mul_inv]; ring
+
+/-- The logarithm of the likelihood ratio of `Q` to the damped and scaled reverse information
+projection is `log E + log (1 + δ ∑ i, |g i|) - log (1 - ε)`, `Q`-almost everywhere. -/
+private lemma log_inv_rnDeriv_withDensity_inv_mul_ofReal_div [SigmaFinite Q] {E : 𝓧 → ℝ≥0∞}
+    (hE : Measurable E) (hg : ∀ i, Measurable (g i)) {δ ε : ℝ}
+    (hδ : 0 ≤ δ) (hε1 : ε < 1) :
+    ∀ᵐ x ∂Q, ENNReal.log (((Q.withDensity (dampedDensity E g δ ε)).rnDeriv Q)⁻¹ x) =
+      ENNReal.log (E x) +
+        ((Real.log (1 + δ * ∑ j, |g j x|) - Real.log (1 - ε) : ℝ) : EReal) := by
+  filter_upwards [Measure.rnDeriv_withDensity Q (measurable_dampedDensity hE hg δ ε)] with x hx
+  have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by positivity
+  have hpos : 0 < (1 - ε) / (1 + δ * ∑ j, |g j x|) := div_pos (by linarith) hh0
+  -- the likelihood ratio is `E x * (1 + δ ∑ j, |g j x|) / (1 - ε)`
+  have hinv : (dampedDensity E g δ ε x)⁻¹ =
+      E x * ENNReal.ofReal ((1 + δ * ∑ j, |g j x|) / (1 - ε)) := by
+    rw [dampedDensity, ENNReal.mul_inv (.inr ENNReal.ofReal_ne_top)
+      (.inr (ENNReal.ofReal_pos.2 hpos).ne'), inv_inv, ← ENNReal.ofReal_inv_of_pos hpos, inv_div]
+  rw [Pi.inv_apply, hx, hinv, ENNReal.log_mul_add,
+    ENNReal.log_ofReal_of_pos (div_pos hh0 (by linarith)), Real.log_div hh0.ne' (by linarith)]
+
+/-- **Completion of the damped reverse information projection**: when `Q` is carried by a set `Y`
+without arbitrage that carries the null, and `E` is such that `∫ F / E ∂Q ≤ 1` for every
+e-variable `F`, as the numeraire is [LRR25], the reverse information projection `Q / E` damped by
+`1 + δ ∑ i, |g i|` and scaled by `1 - ε` becomes a member of the null once a finitely supported
+measure is added. -/
+private lemma exists_withDensity_inv_mul_ofReal_div_add_sum_smul_dirac_mem_constraintNull
+    (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y)
+    (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) [IsProbabilityMeasure Q] (hQY : Q Yᶜ = 0)
+    {E : 𝓧 → ℝ≥0∞} (hE : Measurable E)
+    (hEF : ∀ F, IsEVar F (constraintNull (range g)) → ∫⁻ x, F x / E x ∂Q ≤ 1) {δ ε : ℝ}
+    (hδ : 0 < δ) (hε : 0 < ε) (hε1 : ε < 1) :
+    ∃ (α : Type) (_ : Fintype α) (x : α → 𝓧) (w : α → ℝ),
+      Q.withDensity (dampedDensity E g δ ε) +
+        ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) ∈ constraintNull (range g) := by
+  have hYne : Y.Nonempty := by
+    by_contra h
+    rw [not_nonempty_iff_eq_empty] at h
+    simp [h] at hQY
+  have hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≤ 1 := by simpa using hEF 1 (isEVar_one _)
+  set μ := Q.withDensity (dampedDensity E g δ ε)
+  have hμE : ∀ F, IsEVar F (constraintNull (range g)) →
+      ∫⁻ x, F x ∂μ ≤ ENNReal.ofReal (1 - ε) := fun F hF ↦
+    (lintegral_withDensity_inv_mul_ofReal_div_le hE hF.measurable hg hδ.le hε1.le).trans
+      (mul_le_of_le_one_right' (hEF F hF))
+  have : IsFiniteMeasure μ :=
+    ⟨by simpa using (hμE 1 (isEVar_one _)).trans_lt ENNReal.ofReal_lt_top⟩
+  obtain ⟨α, _, x, w, -, hP⟩ := exists_add_sum_smul_dirac_mem_constraintNull hg hY hYμ hYne
+    (withDensity_absolutelyContinuous Q _ hQY)
+    (integrable_withDensity_inv_mul_ofReal_div hE hg (hEinv.trans_lt ENNReal.one_lt_top).ne hδ
+      hε.le hε1.le) (ENNReal.ofReal_lt_one.2 (by linarith)) hμE
+  exact ⟨α, inferInstance, x, w, hP⟩
+
+/-! ### The nontrivial inequality of the dual formula, on a set without arbitrage -/
+
+/-- The nontrivial inequality of the dual formula, up to a damping `δ` and a slack `ε`: when `Q`
+is carried by a set `Y` without arbitrage that carries the null, and the largest expected
+logarithm `s` of an e-variable is finite, the reverse information projection `Q / E`, for the
+numeraire `E`, damped by `1 + δ ∑ i, |g i|` so that it integrates the constraints, and scaled by
+`1 - ε`, is completed into a member of the null by a finitely supported measure, at a relative
+entropy at most `s + E_Q[log (1 + δ ∑ i, |g i|)] - log (1 - ε)`. -/
+private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurable (g i))
+    (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0)
+    [IsProbabilityMeasure Q] (hQY : Q Yᶜ = 0)
+    (hQ : Integrable (fun x ↦ Real.log (1 + ∑ i, |g i x|)) Q)
+    (hs : maxUtility Q (constraintNull (range g)) logUtility ≠ ⊤) {δ ε : ℝ} (hδ : 0 < δ)
+    (hδ1 : δ ≤ 1) (hε : 0 < ε) (hε1 : ε < 1) :
+    ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) ≤
+      maxUtility Q (constraintNull (range g)) logUtility +
+        ((∫ x, Real.log (1 + δ * ∑ i, |g i x|) ∂Q - Real.log (1 - ε) : ℝ) : EReal) := by
+  have hS : ∀ μ ∈ constraintNull (range g), IsFiniteMeasure μ :=
+    fun _ ↦ isFiniteMeasure_of_mem_constraintNull
+  set s := maxUtility Q (constraintNull (range g)) logUtility with hs_def
+  set E := numeraire Q (constraintNull (range g)) with hE_def
+  have hEnum := isNumeraire_numeraire Q hS
+  have hEm : Measurable E := hEnum.isEVar.measurable
+  have hsE : s = ∫ᵉ x, ENNReal.log (E x) ∂Q := maxUtility_eq_eintegral_numeraire Q hS
+  have hE_top : ∀ᵐ x ∂Q, E x ≠ ∞ := by
+    have := ae_ne_top_of_eintegral_ne_top (by fun_prop) hEnum.eintegrable_log (hsE ▸ hs)
+    filter_upwards [this] with x hx
+    simpa using hx
+  -- the damped and scaled reverse information projection, and its completion into a member `P`
+  -- of the null
+  obtain ⟨α, _, x, w, hP⟩ :=
+    exists_withDensity_inv_mul_ofReal_div_add_sum_smul_dirac_mem_constraintNull hg hY hYμ hQY hEm
+      (fun F hF ↦ hEnum.lintegral_div_le_one hF) hδ hε hε1
+  set μ := Q.withDensity (dampedDensity E g δ ε) with hμ_def
+  set P := μ + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) with hP_def
+  have := isProbabilityMeasure_of_mem_constraintNull hP
+  have hμP : μ ≤ P := Measure.le_add_right le_rfl
+  have : IsFiniteMeasure μ := isFiniteMeasure_of_le P hμP
+  refine (iInf₂_le P hP).trans ?_
+  rw [← maxUtility_singleton_eq_klDiv Q P]
+  have hμeff : μ ∈ effectiveSet {P} := fun X hX ↦
+    calc ∫⁻ x, X x ∂μ ≤ ∫⁻ x, X x ∂P := lintegral_mono' hμP le_rfl
+      _ ≤ P univ := hX.lintegral_le_measure_univ P rfl
+      _ = 1 := measure_univ
+  have hac : Q ≪ μ := withDensity_absolutelyContinuous'
+    (measurable_dampedDensity hEm hg δ ε).aemeasurable
+    (by filter_upwards [hE_top] with x hx using dampedDensity_ne_zero hδ.le hε1 hx)
+  have hlogh0 : Integrable (fun x ↦ Real.log (1 + δ * ∑ i, |g i x|)) Q :=
+    hQ.log_one_add_const_mul (by fun_prop) (fun x ↦ by positivity) hδ.le hδ1
+  have hlogh : Integrable
+      (fun x ↦ Real.log (1 + δ * ∑ i, |g i x|) - Real.log (1 - ε)) Q :=
+    hlogh0.sub (integrable_const _)
+  -- the relative entropy from `Q` to `P` is at most that of the likelihood ratio of `Q` to `μ`
+  refine iSup₂_le fun X hX ↦ (eintegral_log_isEVar_le_eintegral_rnDeriv hμeff hac hX).trans ?_
+  have hI := eintegral_eq_integral hlogh
+  have hI_bot : ∫ᵉ x, ((Real.log (1 + δ * ∑ i, |g i x|) - Real.log (1 - ε) : ℝ) : EReal) ∂Q ≠
+      ⊥ := by
+    rw [hI]
+    exact EReal.coe_ne_bot _
+  have hI_top : ∫ᵉ x, ((Real.log (1 + δ * ∑ i, |g i x|) - Real.log (1 - ε) : ℝ) : EReal) ∂Q ≠
+      ⊤ := by
+    rw [hI]
+    exact EReal.coe_ne_top _
+  rw [eintegral_congr_ae (log_inv_rnDeriv_withDensity_inv_mul_ofReal_div hEm hg hδ.le hε1),
+    eintegral_add (by fun_prop) (by fun_prop) (eintegrable_of_eintegral_ne_bot hI_bot)
+      (.inr hI_top) (.inr hI_bot), hI, ← hsE, integral_sub hlogh0 (integrable_const _)]
+  simp
+
+/-- **The smallest relative entropy is at most the largest expected logarithm, on a set without
+arbitrage**: when `Q` is carried by a set `Y` without
+arbitrage that carries the null, and `log (1 + ∑ i, |g i|)` is `Q`-integrable, the smallest
+relative entropy from `Q` to the null is at most the largest expected logarithm of an
+e-variable. -/
+theorem iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn (hg : ∀ i, Measurable (g i))
+    (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0)
+    [IsProbabilityMeasure Q] (hQY : Q Yᶜ = 0)
+    (hQ : Integrable (fun x ↦ Real.log (1 + ∑ i, |g i x|)) Q) :
+    ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) ≤
+      maxUtility Q (constraintNull (range g)) logUtility := by
+  have hS : ∀ μ ∈ constraintNull (range g), IsFiniteMeasure μ :=
+    fun _ ↦ isFiniteMeasure_of_mem_constraintNull
+  set s := maxUtility Q (constraintNull (range g)) logUtility with hs_def
+  rcases eq_or_ne s ⊤ with hs | hs
+  · rw [hs]
+    exact le_top
+  have hsE : s = ∫ᵉ x, ENNReal.log (numeraire Q (constraintNull (range g)) x) ∂Q :=
+    maxUtility_eq_eintegral_numeraire Q hS
+  have hs0 : (0 : EReal) ≤ s := hsE ▸ (isNumeraire_numeraire Q hS).eintegral_log_nonneg
+  have hs_bot : s ≠ ⊥ := ne_bot_of_le_ne_bot (by simp) hs0
+  have hδ1 : ∀ n : ℕ, 1 / ((n : ℝ) + 1) ≤ 1 := fun n ↦ div_le_one_of_le₀ (by simp) (by positivity)
+  -- the damping tends to zero, by dominated convergence
+  have hlim := hQ.tendsto_integral_log_one_add_mul (by fun_prop) (fun x ↦ by positivity)
+    tendsto_one_div_add_atTop_nhds_zero_nat (.of_forall fun n ↦ by positivity)
+  -- choose the damping and the slack for a given margin
+  rw [← EReal.le_of_forall_lt_iff_le]
+  intro z hz
+  have hs_eq : s = ((s.toReal : ℝ) : EReal) := (EReal.coe_toReal hs hs_bot).symm
+  rw [hs_eq, EReal.coe_lt_coe_iff] at hz
+  set η := z - s.toReal with hη_def
+  have hη : 0 < η := by linarith
+  obtain ⟨n, hn⟩ := (hlim.eventually (gt_mem_nhds (half_pos hη))).exists
+  set ε := 1 - Real.exp (-(η / 2)) with hε_def
+  have hε : 0 < ε := by
+    have : Real.exp (-(η / 2)) < 1 := Real.exp_lt_one_iff.2 (by linarith)
+    linarith
+  have hε1 : ε < 1 := by
+    have := Real.exp_pos (-(η / 2))
+    linarith
+  have hlogε : Real.log (1 - ε) = -(η / 2) := by
+    rw [hε_def, sub_sub_cancel, Real.log_exp]
+  refine (iInf_klDiv_constraintNull_le_maxUtility_add hg hY hYμ hQY hQ hs
+    (δ := 1 / ((n : ℝ) + 1)) (by positivity) (hδ1 n) hε hε1).trans ?_
+  rw [← hs_def, hs_eq, ← EReal.coe_add, EReal.coe_le_coe_iff, hlogε]
+  linarith
+
+/-! ### E-variables and bets -/
+
+/-- On a set `Y` without arbitrage that carries the null and `Q`, the largest expected logarithm
+of an e-variable is at most that of a bet: every e-variable is at most a bet on `Y`, by the
+complete class theorem [LRR26, Theorem 3.1]. -/
+theorem maxUtility_constraintNull_le_iSup_eintegral_log_of_noArbitrageOn
+    (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y)
+    (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) (hQY : Q Yᶜ = 0) :
+    maxUtility Q (constraintNull (range g)) logUtility ≤
+      ⨆ π ∈ constraintBets g,
+        ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q := by
+  refine iSup₂_le fun X hX ↦ ?_
+  obtain ⟨π, hπ, hXπ⟩ := hX.exists_mem_constraintBets_le_of_noArbitrageOn hg hY hYμ
+  refine le_trans ?_ (le_iSup₂ (f := fun π (_ : π ∈ constraintBets g) ↦
+    ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q) _ hπ)
+  refine eintegral_mono_ae (Filter.eventually_of_mem (mem_ae_iff.2 hQY) fun x hx ↦ ?_)
+  simp only [Function.comp_apply, logUtility_apply]
+  exact ENNReal.log_le_log (hXπ x hx)
+
+/-- If a nonnegative combination of the constraints is nonnegative almost surely under every
+member of the null and under a finite measure `Q`, and positive on a set of positive `Q`-measure,
+then the bets have arbitrarily large expected logarithms under `Q`. -/
+theorem iSup_eintegral_log_ofReal_one_add_eq_top (hg : ∀ i, Measurable (g i))
+    [IsFiniteMeasure Q] {ρ : ι → ℝ} (hρ : ∀ i, 0 ≤ ρ i)
+    (hρμ : ∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ ∑ i, ρ i * g i x)
+    (hρQ : ∀ᵐ x ∂Q, 0 ≤ ∑ i, ρ i * g i x) (hQρ : Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0) :
+    ⨆ π ∈ constraintBets g,
+      ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q = ⊤ := by
+  obtain ⟨c, hc, hQc⟩ := exists_gt_measure_setOf_le_ne_zero hQρ
+  set A := {x | c ≤ ∑ i, ρ i * g i x} with hA_def
+  have hA : MeasurableSet A := measurableSet_le measurable_const (by fun_prop)
+  set q := (Q A).toReal with hq_def
+  have hq : 0 < q := ENNReal.toReal_pos hQc (measure_ne_top Q A)
+  rw [EReal.eq_top_iff_forall_lt]
+  intro y
+  -- the bet with weights `t ρ` is at least `1`, and at least `1 + t c` on `A`
+  set t := (Real.exp (|y| / q + 1) - 1) / c with ht_def
+  have ht : 0 ≤ t := div_nonneg (by linarith [Real.one_le_exp (by positivity : 0 ≤ |y| / q + 1)])
+    hc.le
+  have hsum : ∀ x, ∑ i, ((t * ρ i).toNNReal : ℝ) * g i x = t * ∑ i, ρ i * g i x := fun x ↦ by
+    simp only [Real.coe_toNNReal _ (mul_nonneg ht (hρ _)), mul_assoc, ← Finset.mul_sum]
+  have hbet : (fun i ↦ (t * ρ i).toNNReal) ∈ constraintBets g := by
+    refine mem_constraintBets_iff.2 fun μ hμ ↦ ?_
+    filter_upwards [hρμ μ hμ] with x hx
+    rw [hsum]
+    have := mul_nonneg ht hx
+    linarith
+  have hlog : Real.log (1 + t * c) = |y| / q + 1 := by
+    rw [ht_def, div_mul_cancel₀ _ hc.ne', add_sub_cancel, Real.log_exp]
+  have hlow : ((Real.log (1 + t * c) * q : ℝ) : EReal) ≤
+      ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, ((t * ρ i).toNNReal : ℝ) * g i x)) ∂Q := by
+    have hlc : 0 ≤ Real.log (1 + t * c) := Real.log_nonneg (by nlinarith)
+    calc ((Real.log (1 + t * c) * q : ℝ) : EReal)
+        = ∫ᵉ x, ((A.indicator (fun _ ↦ ENNReal.ofReal (Real.log (1 + t * c))) x : ℝ≥0∞) :
+            EReal) ∂Q := by
+          have : ENNReal.ofReal (Real.log (1 + t * c)) * Q A =
+              ENNReal.ofReal (Real.log (1 + t * c) * q) := by
+            rw [ENNReal.ofReal_mul hlc, hq_def, ENNReal.ofReal_toReal (measure_ne_top Q A)]
+          rw [eintegral_coe_ennreal, lintegral_indicator_const hA, this,
+            EReal.coe_ennreal_ofReal, max_eq_left (mul_nonneg hlc hq.le)]
+      _ ≤ _ := by
+          refine eintegral_mono_ae ?_
+          filter_upwards [hρQ] with x hx
+          rw [hsum]
+          have h1 : 0 < 1 + t * ∑ i, ρ i * g i x := by nlinarith
+          rw [ENNReal.log_ofReal_of_pos h1]
+          by_cases hxA : x ∈ A
+          · have hcx : c ≤ ∑ i, ρ i * g i x := by simpa [hA_def] using hxA
+            rw [indicator_of_mem hxA, EReal.coe_ennreal_ofReal, max_eq_left hlc,
+              EReal.coe_le_coe_iff]
+            exact Real.log_le_log (by nlinarith) (by nlinarith [hcx])
+          · rw [indicator_of_notMem hxA, EReal.coe_ennreal_zero, ← EReal.coe_zero,
+              EReal.coe_le_coe_iff]
+            exact Real.log_nonneg (by nlinarith)
+  calc (y : EReal) < ((Real.log (1 + t * c) * q : ℝ) : EReal) := by
+        rw [hlog, EReal.coe_lt_coe_iff]
+        nlinarith [le_abs_self y, abs_nonneg y, div_mul_cancel₀ |y| hq.ne']
+    _ ≤ _ := hlow
+    _ ≤ _ := le_iSup₂ (f := fun π (_ : π ∈ constraintBets g) ↦
+        ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q) _ hbet
+
+/-- **The largest expected logarithm of an e-variable is the supremum of those of the bets**: for
+finitely many measurable constraints `g i` and a finite measure `Q`, the largest expected
+logarithm under `Q` of an e-variable for the null is the supremum of the expected logarithms of
+the bets `1 + ∑ i, π i * g i`. The expected logarithm of a bet is `⊥` when the bet vanishes or is
+negative on a set of positive `Q`-measure. This follows [EVR26, Note 20]. -/
+theorem maxUtility_constraintNull_eq_iSup_eintegral_log (hg : ∀ i, Measurable (g i))
+    (Q : Measure 𝓧) [IsFiniteMeasure Q] :
+    maxUtility Q (constraintNull (range g)) logUtility =
+      ⨆ π ∈ constraintBets g,
+        ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q := by
+  refine le_antisymm ?_ (iSup₂_le fun π hπ ↦
+    (isEVar_ofReal_one_add_of_mem_constraintBets hg hπ).eintegral_le_maxUtility Q logUtility)
+  obtain ⟨Y, -, hYμ, hQY, hY⟩ | ⟨ρ, hρ, hρμ, hρQ, hQρ⟩ :=
+    exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos hg Q
+  · exact maxUtility_constraintNull_le_iSup_eintegral_log_of_noArbitrageOn hg hY hYμ hQY
+  · rw [iSup_eintegral_log_ofReal_one_add_eq_top hg hρ hρμ hρQ hQρ]
+    exact le_top
+
+/-! ### The dual formula -/
+
+/-- **The smallest relative entropy to the null is the largest expected logarithm of an
+e-variable**: for finitely many measurable constraints `g i` and a probability measure `Q` under
+which every `log⁺ |g i|` is integrable, with no constraint qualification. The null may be empty:
+both sides are then `⊤`. This follows [EVR26, Note 20]. -/
+theorem iInf_klDiv_constraintNull_eq_maxUtility {κ : Type*} [Finite κ] {g : κ → 𝓧 → ℝ}
+    (hg : ∀ i, Measurable (g i)) (Q : Measure 𝓧) [IsProbabilityMeasure Q]
+    (hQ : ∀ i, Integrable (fun x ↦ Real.posLog (g i x)) Q) :
+    ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) =
+      maxUtility Q (constraintNull (range g)) logUtility := by
+  have := Fintype.ofFinite κ
+  refine le_antisymm ?_ (le_iInf₂ fun P hP ↦ ?_)
+  · obtain ⟨Y, -, hYμ, hQY, hY⟩ | ⟨ρ, hρ, hρμ, hρQ, hQρ⟩ :=
+      exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos hg Q
+    · exact iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn hg hY hYμ hQY
+        (integrable_log_one_add_sum_abs (fun i ↦ (hg i).aemeasurable) hQ)
+    · rw [maxUtility_constraintNull_eq_iSup_eintegral_log hg Q,
+        iSup_eintegral_log_ofReal_one_add_eq_top hg hρ hρμ hρQ hQρ]
+      exact le_top
+  · have := isProbabilityMeasure_of_mem_constraintNull hP
+    rw [← maxUtility_singleton_eq_klDiv Q P]
+    exact maxUtility_anti (singleton_subset_iff.2 hP)
+
+/-- **The dual formula for the smallest relative entropy to a null generated by finitely many
+constraints**: for measurable constraints `g i` and a probability measure `Q` under which every
+`log⁺ |g i|` is integrable, the smallest relative entropy from `Q` to the null is the supremum of
+the expected logarithms of the bets `1 + ∑ i, π i * g i`, with no constraint qualification. The
+formulas of [HT15] for one mean constraint are cases of it. This follows [EVR26, Note 20]. -/
+theorem iInf_klDiv_constraintNull_eq_iSup_eintegral_log (hg : ∀ i, Measurable (g i))
+    (Q : Measure 𝓧) [IsProbabilityMeasure Q]
+    (hQ : ∀ i, Integrable (fun x ↦ Real.posLog (g i x)) Q) :
+    ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) =
+      ⨆ π ∈ constraintBets g,
+        ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q := by
+  rw [iInf_klDiv_constraintNull_eq_maxUtility hg Q hQ,
+    maxUtility_constraintNull_eq_iSup_eintegral_log hg Q]
+
+end ProbabilityTheory
diff --git a/LMLExplore/MeasureTheory/Measure/MeasureSpaceDef.lean b/LMLExplore/MeasureTheory/Measure/MeasureSpaceDef.lean
new file mode 100644
index 00000000..6809a3f0
--- /dev/null
+++ b/LMLExplore/MeasureTheory/Measure/MeasureSpaceDef.lean
@@ -0,0 +1,51 @@
+/-
+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.MeasureSpaceDef
+public import Mathlib.Algebra.Order.Archimedean.Real.Basic
+
+/-!
+# A superlevel set of positive measure
+
+If a real function exceeds `a` on a set of positive measure, then it is at least some `c > a` on a
+set of positive measure: the set `{a < f}` is the countable union of the sets
+`{a + 1 / (n + 1) ≤ f}`.
+
+## Main statements
+
+* `MeasureTheory.exists_gt_measure_setOf_le_ne_zero`: if `μ {a < f} ≠ 0`, then
+  `μ {c ≤ f} ≠ 0` for some `c > a`.
+-/
+
+public section
+
+open Set
+
+namespace MeasureTheory
+
+variable {α : Type*} [MeasurableSpace α] {μ : Measure α}
+
+/-- If a real function exceeds `a` on a set of positive measure, then it is at least some `c > a`
+on a set of positive measure. The function need not be measurable. -/
+theorem exists_gt_measure_setOf_le_ne_zero {f : α → ℝ} {a : ℝ} (h : μ {x | a < f x} ≠ 0) :
+    ∃ c, a < c ∧ μ {x | c ≤ f x} ≠ 0 := by
+  by_contra! h'
+  refine h ?_
+  have : {x | a < f x} = ⋃ n : ℕ, {x | a + 1 / ((n : ℝ) + 1) ≤ f x} := by
+    ext x
+    simp only [mem_ofPred_eq, mem_iUnion]
+    constructor
+    · intro hx
+      obtain ⟨n, hn⟩ := exists_nat_one_div_lt (sub_pos.2 hx)
+      exact ⟨n, by linarith⟩
+    · rintro ⟨n, hn⟩
+      have : 0 < 1 / ((n : ℝ) + 1) := by positivity
+      linarith
+  rw [this]
+  exact measure_iUnion_null fun n ↦ h' _ (lt_add_of_pos_right a (by positivity))
+
+end MeasureTheory