diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean
index cc72149e..9d9125de 100644
--- a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean
+++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean
@@ -33,7 +33,11 @@ The proof here is finite-dimensional, in three steps.
   measurable set `Y` that carries every member of the null and on which the constraints admit no
   arbitrage: every nonnegative combination of the constraints that is nonnegative on `Y` vanishes
   on `Y` (`ProbabilityTheory.NoArbitrageOn`). The removed sets are null for every member of the
-  null, since there the combination has a nonnegative integrand with a nonpositive integral.
+  null, since there the combination has a nonnegative integrand with a nonpositive integral. The
+  same construction, stopped at the first removed set that a given measure `Q` charges, gives
+  either such a set `Y` that also carries `Q`, or a nonnegative combination of the constraints,
+  nonnegative almost surely under the null and under `Q`, that is positive on a set of positive
+  `Q`-measure.
 * *The finite step.* On a finite subset of `Y`, separating a compact convex hull from a closed
   convex set gives the domination up to an additive `δ > 0`.
 * *Compactness.* Without arbitrage, the weights whose support is not redundant
@@ -63,6 +67,9 @@ supported member of the null, so that e-variables are finite on `Y`.
   theorem in finite-dimensional form, on a set without arbitrage.
 * `ProbabilityTheory.exists_measurableSet_noArbitrageOn`: a measurable set carrying the null, on
   which the constraints admit no arbitrage.
+* `ProbabilityTheory.exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos`: such a set
+  that also carries a given measure `Q`, or a nonnegative combination of the constraints that is
+  positive on a set of positive `Q`-measure.
 * `ProbabilityTheory.lt_top_of_isEVar_of_noArbitrageOn`: e-variables are finite on a set without
   arbitrage.
 * `ProbabilityTheory.forall_integral_nonpos_iff_exists_ae_le`: **the complete class theorem**
@@ -447,26 +454,42 @@ theorem exists_charging_family_of_noArbitrageOn (h : NoArbitrageOn a Y) {x₀ :
 
 variable [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {f : 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞}
 
-/-- A set carrying a null generated by finitely many measurable constraints: a measurable set of
-full measure for every member of the null, on which the constraints admit no arbitrage. -/
-theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) :
-    ∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧
-      NoArbitrageOn g Y := by
+/-- A set carrying a null generated by finitely many measurable constraints, seen from a measure
+`Q`: either a measurable set of full measure for every member of the null and for `Q`, on which the
+constraints admit no arbitrage, or a nonnegative combination of the constraints that is
+nonnegative almost surely under every member of the null and under `Q`, and positive on a set of
+positive `Q`-measure. -/
+theorem exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos
+    (hg : ∀ i, Measurable (g i)) (Q : Measure 𝓧) :
+    (∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧ Q Yᶜ = 0 ∧
+      NoArbitrageOn g Y) ∨
+    ∃ ρ : ι → ℝ, (∀ i, 0 ≤ ρ i) ∧
+      (∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ ∑ i, ρ i * g i x) ∧
+      (∀ᵐ x ∂Q, 0 ≤ ∑ i, ρ i * g i x) ∧ Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0 := by
   classical
   let V : Set 𝓧 → Submodule ℝ (ι → ℝ) := fun Y ↦ Submodule.span ℝ ((fun x i ↦ g i x) '' Y)
   suffices H : ∀ n : ℕ, ∀ Y : Set 𝓧, MeasurableSet Y →
-      (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) → Module.finrank ℝ (V Y) = n →
-      ∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧
-        NoArbitrageOn g Y from
-    H _ univ MeasurableSet.univ (by simp) rfl
+      (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) → Q Yᶜ = 0 → Module.finrank ℝ (V Y) = n →
+      (∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧ Q Yᶜ = 0 ∧
+        NoArbitrageOn g Y) ∨
+      ∃ ρ : ι → ℝ, (∀ i, 0 ≤ ρ i) ∧
+        (∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ ∑ i, ρ i * g i x) ∧
+        (∀ᵐ x ∂Q, 0 ≤ ∑ i, ρ i * g i x) ∧ Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0 from
+    H _ univ MeasurableSet.univ (by simp) (by simp) rfl
   intro n
   induction n using Nat.strong_induction_on with
   | _ n ih =>
-  intro Y hY hμY hn
+  intro Y hY hμY hQY hn
   by_cases hT : NoArbitrageOn g Y
-  · exact ⟨Y, hY, hμY, hT⟩
+  · exact .inl ⟨Y, hY, hμY, hQY, hT⟩
   simp only [noArbitrageOn_iff, not_forall] at hT
   obtain ⟨ρ, hρ0, hρY, x₀, hx₀, hne⟩ := hT
+  -- the combination is nonnegative almost everywhere for the measures carried by `Y`
+  have hnn : ∀ ν : Measure 𝓧, ν Yᶜ = 0 → ∀ᵐ x ∂ν, 0 ≤ ∑ i, ρ i * g i x := fun ν hν ↦
+    Filter.eventually_of_mem (mem_ae_iff.2 hν) hρY
+  by_cases hQρ : Q {x | 0 < ∑ i, ρ i * g i x} = 0
+  swap
+  · exact .inr ⟨ρ, hρ0, fun μ hμ ↦ hnn μ (hμY μ hμ), hnn Q hQY, hQρ⟩
   set Y' := Y ∩ {x | ∑ i, ρ i * g i x ≤ 0}
   have hY' : MeasurableSet Y' := hY.inter (measurableSet_le (by fun_prop) measurable_const)
   have hsub : Y'ᶜ ⊆ Yᶜ ∪ {x | 0 < ∑ i, ρ i * g i x} := by
@@ -479,13 +502,12 @@ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) :
   have hμY' : ∀ μ ∈ constraintNull (range g), μ Y'ᶜ = 0 := by
     intro μ hμ
     have hint := integrable_sum_mul_of_mem_constraintNull hμ ρ
-    have hnn : 0 ≤ᵐ[μ] fun x ↦ ∑ i, ρ i * g i x :=
-      Filter.eventually_of_mem (mem_ae_iff.2 (hμY μ hμ)) hρY
-    have h0 := (integral_eq_zero_iff_of_nonneg_ae hnn hint).1
+    have h0 := (integral_eq_zero_iff_of_nonneg_ae (hnn μ (hμY μ hμ)) hint).1
       (le_antisymm (integral_sum_mul_nonpos_of_mem_constraintNull hμ hρ0)
-        (integral_nonneg_of_ae hnn))
+        (integral_nonneg_of_ae (hnn μ (hμY μ hμ))))
     refine measure_mono_null hsub (measure_union_null (hμY μ hμ) ?_)
     exact measure_mono_null (fun x hx ↦ (mem_ofPred_eq ▸ hx).ne') (ae_iff.1 h0)
+  have hQY' : Q Y'ᶜ = 0 := measure_mono_null hsub (measure_union_null hQY hQρ)
   -- removing the set where the combination is positive lowers the dimension
   have hlt : V Y' < V Y := by
     refine lt_of_le_of_ne (Submodule.span_mono (image_mono inter_subset_left)) fun heq ↦ ?_
@@ -500,7 +522,17 @@ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) :
     have : (fun i ↦ g i x₀) ∈ V Y := Submodule.subset_span ⟨x₀, hx₀, rfl⟩
     rw [← heq] at this
     exact hne (by simpa [hℓ] using hle this)
-  exact ih _ (hn ▸ Submodule.finrank_lt_finrank_of_lt hlt) Y' hY' hμY' rfl
+  exact ih _ (hn ▸ Submodule.finrank_lt_finrank_of_lt hlt) Y' hY' hμY' hQY' rfl
+
+/-- A set carrying a null generated by finitely many measurable constraints: a measurable set of
+full measure for every member of the null, on which the constraints admit no arbitrage. -/
+theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) :
+    ∃ Y : Set 𝓧, MeasurableSet Y ∧ (∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) ∧
+      NoArbitrageOn g Y := by
+  obtain ⟨Y, hY, hμY, -, hT⟩ | ⟨_, -, -, -, h⟩ :=
+    exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos hg 0
+  · exact ⟨Y, hY, hμY, hT⟩
+  · simp at h
 
 /-- On a set without arbitrage, an e-variable for the null is finite. -/
 theorem lt_top_of_isEVar_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y)