feat: admissible e-variables for finitely many constraints [LRR26, Corollary 3.3], and domination by an admissible bet

LMLExplore/EValues/ConstraintNull/Admissible.lean

@@ -0,0 +1,195 @@
+/-
+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.Admissible
+public import LMLExplore.EValues.ConstraintNull.CompleteClass
+import LMLExplore.LinearAlgebra.FiniteDimensional.Lemmas
+
+/-!
+# Admissible e-variables for finitely many constraints
+
+Let `g i`, for `i` in a finite type, be measurable real constraints on a measurable space `𝓧`. By
+the complete class theorem (`LMLExplore.EValues.ConstraintNull.CompleteClass`), every e-variable
+for the null `constraintNull (range g)` is dominated by a bet `1 + ∑ i, π i * g i`, almost surely
+under every member of the null. This file describes the admissible e-variables.
+
+* Every admissible e-variable is a bet, almost surely under every member of the null
+  [LRR26, Corollary 3.3].
+* A bet is admissible exactly when no bet dominates it strictly, almost surely under every member
+  of the null. Under the constraint qualification of [LRR26, Corollary 3.3], which asks that a
+  nonnegative combination of the constraints dominated by another one is equal to it, almost
+  surely under every member of the null, every bet is admissible, and the admissible e-variables
+  are the measurable functions equal to a bet almost surely under every member of the null.
+* Every e-variable is dominated by an admissible bet, with no constraint qualification. With
+  [LRR26, Lemma 6.2], this says that the admissible bets form a minimal complete class, which
+  [LRR26, Theorem 6.5] proves under the constraint qualification and [LRR26, Section 6]
+  conjectures in general.
+
+The last statement is proved on a measurable set `Y` that carries the null and on which the
+constraints admit no arbitrage. Every point of such a set is an atom of a finitely supported
+member of the null, so a property holds almost surely under every member of the null exactly when
+it holds on `Y`. Among the weights that dominate a given e-variable on `Y`, keep a bet
+nonnegative on `Y` and have a nonredundant support, which form a compact set
+[LRR26, Lemma 7.2], a maximizer of the sum of the combinations at finitely many points of `Y`
+that detect the combinations vanishing on `Y` gives an admissible bet.
+
+## Main statements
+
+* `ProbabilityTheory.IsAdmissibleEVar.exists_mem_constraintBets_ae_eq`: every admissible
+  e-variable is a bet [LRR26, Corollary 3.3].
+* `ProbabilityTheory.isAdmissibleEVar_ofReal_one_add_iff`: a bet is admissible exactly when no
+  bet dominates it strictly.
+* `ProbabilityTheory.isAdmissibleEVar_ofReal_one_add_of_mem_constraintBets`,
+  `ProbabilityTheory.isAdmissibleEVar_constraintNull_iff`: under the constraint qualification, the
+  admissible e-variables are the bets [LRR26, Corollary 3.3].
+* `ProbabilityTheory.IsEVar.exists_mem_constraintBets_isAdmissibleEVar_ae_le`: every e-variable
+  is dominated by an admissible bet.
+
+## References
+
+* [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 LMLExplore
+open scoped ENNReal NNReal
+
+namespace ProbabilityTheory
+
+variable {𝓧 ι : Type*} [Fintype ι] [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞}
+  {π : ι → ℝ≥0}
+
+/-! ### Admissible e-variables -/
+
+/-- **Every admissible e-variable is a bet** [LRR26, Corollary 3.3]: an admissible e-variable for
+the null generated by finitely many measurable constraints `g i` is equal to a bet
+`1 + ∑ i, π i * g i`, almost surely under every member of the null. -/
+theorem IsAdmissibleEVar.exists_mem_constraintBets_ae_eq (hg : ∀ i, Measurable (g i))
+    (hE : IsAdmissibleEVar E (constraintNull (range g))) :
+    ∃ π ∈ constraintBets g, ∀ μ ∈ constraintNull (range g),
+      E =ᵐ[μ] fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) := by
+  obtain ⟨π, hπ, h⟩ := hE.toIsEVar.exists_mem_constraintBets_ae_le hg
+  exact ⟨π, hπ, fun μ hμ ↦
+    (hE.ae_eq (isEVar_ofReal_one_add_of_mem_constraintBets hg hπ) h hμ).symm⟩
+
+/-- A bet on finitely many measurable constraints is admissible exactly when no bet dominates it
+strictly: every bet whose combination of the constraints is at least its own, almost surely under
+every member of the null, has a combination at most its own, almost surely under every member of
+the null. -/
+theorem isAdmissibleEVar_ofReal_one_add_iff (hg : ∀ i, Measurable (g i))
+    (hπ : π ∈ constraintBets g) :
+    IsAdmissibleEVar (fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x))
+        (constraintNull (range g)) ↔
+      ∀ π' ∈ constraintBets g,
+        (∀ μ ∈ constraintNull (range g),
+          ∀ᵐ x ∂μ, ∑ i, (π i : ℝ) * g i x ≤ ∑ i, (π' i : ℝ) * g i x) →
+        ∀ μ ∈ constraintNull (range g),
+          ∀ᵐ x ∂μ, ∑ i, (π' i : ℝ) * g i x ≤ ∑ i, (π i : ℝ) * g i x := by
+  refine ⟨fun h π' hπ' hle μ hμ ↦ ?_, fun h ↦
+    ⟨isEVar_ofReal_one_add_of_mem_constraintBets hg hπ, fun F hF hEF μ hμ ↦ ?_⟩⟩
+  · have h1 := h.ae_le (isEVar_ofReal_one_add_of_mem_constraintBets hg hπ')
+      (fun ν hν ↦ (hle ν hν).mono fun x hx ↦ ENNReal.ofReal_le_ofReal (by linarith)) hμ
+    filter_upwards [h1, mem_constraintBets_iff.1 hπ μ hμ] with x hx hx0
+    linarith [(ENNReal.ofReal_le_ofReal_iff hx0).1 hx]
+  · -- an e-variable above the bet is below another bet, which is then equal to it
+    obtain ⟨π', hπ', hFπ'⟩ := hF.exists_mem_constraintBets_ae_le hg
+    have hle : ∀ ν ∈ constraintNull (range g),
+        ∀ᵐ x ∂ν, ∑ i, (π i : ℝ) * g i x ≤ ∑ i, (π' i : ℝ) * g i x := fun ν hν ↦ by
+      filter_upwards [hEF ν hν, hFπ' ν hν, mem_constraintBets_iff.1 hπ' ν hν] with x h1 h2 h3
+      linarith [(ENNReal.ofReal_le_ofReal_iff h3).1 (h1.trans h2)]
+    filter_upwards [hFπ' μ hμ, h π' hπ' hle μ hμ] with x h1 h2
+    exact h1.trans (ENNReal.ofReal_le_ofReal (by linarith))
+
+/-- **Under the constraint qualification, every bet is admissible** [LRR26, Corollary 3.3]: if a
+nonnegative combination of finitely many measurable constraints that is at most another one,
+almost surely under every member of the null, is equal to it almost surely under every member of
+the null, then every bet is an admissible e-variable. -/
+theorem isAdmissibleEVar_ofReal_one_add_of_mem_constraintBets (hg : ∀ i, Measurable (g i))
+    (hcq : ∀ ρ ρ' : ι → ℝ≥0,
+      (∀ μ ∈ constraintNull (range g),
+        ∀ᵐ x ∂μ, ∑ i, (ρ i : ℝ) * g i x ≤ ∑ i, (ρ' i : ℝ) * g i x) →
+      ∀ μ ∈ constraintNull (range g),
+        ∀ᵐ x ∂μ, ∑ i, (ρ' i : ℝ) * g i x ≤ ∑ i, (ρ i : ℝ) * g i x)
+    (hπ : π ∈ constraintBets g) :
+    IsAdmissibleEVar (fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x))
+      (constraintNull (range g)) :=
+  (isAdmissibleEVar_ofReal_one_add_iff hg hπ).2 fun π' _ h ↦ hcq π π' h
+
+/-- **The admissible e-variables under the constraint qualification** [LRR26, Corollary 3.3]: if
+a nonnegative combination of finitely many measurable constraints that is at most another one,
+almost surely under every member of the null, is equal to it almost surely under every member of
+the null, then the admissible e-variables are the measurable functions equal to a bet
+`1 + ∑ i, π i * g i`, almost surely under every member of the null. -/
+theorem isAdmissibleEVar_constraintNull_iff (hg : ∀ i, Measurable (g i))
+    (hcq : ∀ ρ ρ' : ι → ℝ≥0,
+      (∀ μ ∈ constraintNull (range g),
+        ∀ᵐ x ∂μ, ∑ i, (ρ i : ℝ) * g i x ≤ ∑ i, (ρ' i : ℝ) * g i x) →
+      ∀ μ ∈ constraintNull (range g),
+        ∀ᵐ x ∂μ, ∑ i, (ρ' i : ℝ) * g i x ≤ ∑ i, (ρ i : ℝ) * g i x) :
+    IsAdmissibleEVar E (constraintNull (range g)) ↔ Measurable E ∧ ∃ π ∈ constraintBets g,
+      ∀ μ ∈ constraintNull (range g), E =ᵐ[μ] fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) :=
+  ⟨fun hE ↦ ⟨hE.measurable, hE.exists_mem_constraintBets_ae_eq hg⟩, fun ⟨hEm, _, hπ, hEπ⟩ ↦
+    (isAdmissibleEVar_ofReal_one_add_of_mem_constraintBets hg hcq hπ).congr hEm
+      fun μ hμ ↦ (hEπ μ hμ).symm⟩
+
+/-- **Every e-variable is dominated by an admissible bet**: for the null generated by finitely
+many measurable constraints `g i`, with no constraint qualification, every e-variable is at most
+an admissible bet `1 + ∑ i, π i * g i`, almost surely under every member of the null. So the
+admissible bets form a complete class, which is then minimal [LRR26, Lemma 6.2]; under the
+constraint qualification this is [LRR26, Theorem 6.5]. -/
+theorem IsEVar.exists_mem_constraintBets_isAdmissibleEVar_ae_le (hg : ∀ i, Measurable (g i))
+    (hE : IsEVar E (constraintNull (range g))) :
+    ∃ π ∈ constraintBets g,
+      IsAdmissibleEVar (fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x))
+        (constraintNull (range 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
+  obtain ⟨F, hFY, hF⟩ := exists_finset_forall_sum_mul_eq_zero g Y
+  -- among the nonredundant weights of the bets that dominate `π₀` on `Y`, maximize the sum of the
+  -- combinations at finitely many points that detect the combinations vanishing on `Y`
+  set U := nonredundantWeights g Y ∩ {π | ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i * g i x} ∩
+    {π | ∀ x ∈ Y, ∑ i, π₀ i * g i x ≤ ∑ i, π i * g i x} with hU_def
+  have hU : IsCompact U := by
+    refine (isCompact_nonredundantWeights_inter_nonneg hY).inter_right ?_
+    simp only [ofPred_forall]
+    exact isClosed_biInter fun x _ ↦ isClosed_le (by fun_prop) (by fun_prop)
+  have hπ₀U : π₀ ∈ U :=
+    ⟨⟨hπ₀K, fun x hx ↦ ENNReal.toReal_nonneg.trans (hπ₀ x hx)⟩, fun x hx ↦ le_rfl⟩
+  obtain ⟨π, ⟨⟨hπK, hπ1⟩, hπ0⟩, hπmax⟩ := hU.exists_isMaxOn ⟨π₀, hπ₀U⟩
+    (f := fun π ↦ ∑ x ∈ F, ∑ i, π i * g i x) (by fun_prop : Continuous _).continuousOn
+  have hcoe : ∀ i, ((π i).toNNReal : ℝ) = π i := fun i ↦
+    Real.coe_toNNReal _ ((mem_nonredundantWeights_iff.1 hπK).1 i)
+  have hbet : (fun i ↦ (π i).toNNReal) ∈ constraintBets g :=
+    mem_constraintBets_iff.2 ((forall_ae_iff_of_noArbitrageOn hg hY hYμ).2 fun x hx ↦ by
+      simpa only [hcoe] using hπ1 x hx)
+  refine ⟨_, hbet, (isAdmissibleEVar_ofReal_one_add_iff hg hbet).2 fun π' hπ' hle ↦ ?_,
+    (forall_ae_iff_of_noArbitrageOn hg hY hYμ).2 fun x hx ↦ ?_⟩
+  · -- a bet that dominates on `Y` has, on `Y`, a combination with weights in `U`; by maximality
+    -- the two combinations agree at the detecting points, hence on `Y`
+    have hleY : ∀ x ∈ Y, ∑ i, π i * g i x ≤ ∑ i, (π' i : ℝ) * g i x := by
+      simpa only [hcoe] using (forall_ae_iff_of_noArbitrageOn hg hY hYμ).1 hle
+    have hπ'Y : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, (π' i : ℝ) * g i x :=
+      (forall_ae_iff_of_noArbitrageOn hg hY hYμ).1 (mem_constraintBets_iff.1 hπ')
+    obtain ⟨π'', hπ''K, hπ''⟩ := exists_mem_nonredundantWeights_sum_mul_eq (a := g) (Y := Y)
+      fun i ↦ (π' i).coe_nonneg
+    have h1 : ∀ x ∈ Y, ∑ i, π i * g i x ≤ ∑ i, π'' i * g i x := fun x hx ↦
+      (hleY x hx).trans_eq (hπ'' x hx).symm
+    have hπ''U : π'' ∈ U := ⟨⟨hπ''K, fun x hx ↦ by rw [hπ'' x hx]; exact hπ'Y x hx⟩,
+      fun x hx ↦ (hπ0 x hx).trans (h1 x hx)⟩
+    have h2 := forall_sum_mul_eq_of_forall_le_of_sum_le hFY hF h1 (hπmax hπ''U)
+    refine (forall_ae_iff_of_noArbitrageOn hg hY hYμ).2 fun x hx ↦ ?_
+    simp only [hcoe]
+    rw [← hπ'' x hx, h2 x hx]
+  · simp only [hcoe]
+    rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hE hx).ne]
+    exact ENNReal.ofReal_le_ofReal ((hπ₀ x hx).trans (by linarith [hπ0 x hx]))
+
+end ProbabilityTheory

LMLExplore/EValues/ConstraintNull/CompleteClass.lean

@@ -44,7 +44,8 @@ The proof here is finite-dimensional, in three steps.
 
 The finite-dimensional theorem only uses the finitely supported members of the null. Applied to
 multiples of the indicator of a point, it shows that every point of `Y` is charged by a finitely
-supported member of the null, so that e-variables are finite on `Y`.
+supported member of the null, so that e-variables are finite on `Y`, and that a property holds
+almost surely under every member of the null exactly when it holds on `Y`.
 
 ## Main definitions
 
@@ -59,12 +60,18 @@ supported member of the null, so that e-variables are finite on `Y`.
   on `Y`, a combination with nonredundant weights [LRR26, Lemma 3.2].
 * `ProbabilityTheory.exists_finset_sum_le_of_noArbitrageOn`: without arbitrage, the total mass of
   nonredundant weights is controlled at finitely many points [LRR26, proof of Lemma 7.2].
+* `ProbabilityTheory.isCompact_nonredundantWeights_inter_nonneg`: without arbitrage on `Y`, the
+  nonredundant weights `π` with `1 + ∑ i, π i * a i` nonnegative on `Y` form a compact set
+  [LRR26, Lemma 7.2].
 * `ProbabilityTheory.exists_mem_nonredundantWeights_le_of_noArbitrageOn`: the complete class
   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.lt_top_of_isEVar_of_noArbitrageOn`: e-variables are finite on a set without
   arbitrage.
+* `ProbabilityTheory.forall_ae_iff_of_noArbitrageOn`: on a set without arbitrage that carries the
+  null, a property holds almost surely under every member of the null exactly when it holds on
+  the set.
 * `ProbabilityTheory.forall_integral_nonpos_iff_exists_ae_le`: **the complete class theorem**
   [LRR26, Theorem 3.1].
 * `ProbabilityTheory.IsEVar.exists_mem_constraintBets_ae_le`,
@@ -261,6 +268,16 @@ theorem exists_finset_sum_le_of_noArbitrageOn (h : NoArbitrageOn a Y) :
   rw [mul_one_div, div_lt_iff₀ (by positivity)] at this
   linarith
 
+/-- Without arbitrage on `Y`, the nonredundant weights `π` for which `1 + ∑ i, π i * a i` is
+nonnegative on `Y` form a compact set [LRR26, Lemma 7.2]. -/
+theorem isCompact_nonredundantWeights_inter_nonneg (h : NoArbitrageOn a Y) :
+    IsCompact (nonredundantWeights a Y ∩ {π | ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i * a i x}) := by
+  obtain ⟨F₀, hF₀, R, -, hbound⟩ := exists_finset_sum_le_of_noArbitrageOn h
+  refine isCompact_nonredundantWeights_inter ?_ (c := R * 1) fun π hπ ↦
+    hbound π hπ.1 1 zero_le_one fun x hx ↦ by linarith [hπ.2 x (hF₀ hx)]
+  simp only [ofPred_forall]
+  exact isClosed_biInter fun x _ ↦ isClosed_le continuous_const (by fun_prop)
+
 /-- The finite step of the complete class theorem, up to `δ`: if `f` has a nonpositive mean under
 every finitely supported law on `Y` under which the functions `a i` have nonpositive means, then on
 a finite subset of `Y` it is at most `δ` plus a nonnegative combination of the `a i`. The proof
@@ -515,6 +532,35 @@ theorem lt_top_of_isEVar_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : N
   rw [htop, ENNReal.mul_top (by simpa using hwk)] at h2
   exact ENNReal.one_ne_top (top_le_iff.1 h2)
 
+/-- Without arbitrage on `Y`, every point of `Y` is an atom of a member of the null. -/
+theorem exists_mem_constraintNull_measure_singleton_ne_zero (hg : ∀ i, Measurable (g i))
+    (hY : NoArbitrageOn g Y) {x₀ : 𝓧} (hx₀ : x₀ ∈ Y) :
+    ∃ μ ∈ constraintNull (range g), μ {x₀} ≠ 0 := by
+  obtain ⟨α, _, x, w, -, hw, hwg, k, hk, hwk⟩ := exists_charging_family_of_noArbitrageOn hY hx₀
+  rw [mem_simplex_iff] at hw
+  refine ⟨∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k),
+    (sum_smul_dirac_mem_constraintNull_iff (forall_mem_range.2 hg) hw.1).2
+      ⟨hw.2, forall_mem_range.2 hwg⟩, fun h0 ↦ ?_⟩
+  have h1 : ENNReal.ofReal (w k) * Measure.dirac (x k) {x₀} ≤
+      (∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k)) {x₀} := by
+    rw [sum_apply]
+    exact Finset.single_le_sum
+      (f := fun j ↦ (ENNReal.ofReal (w j) • Measure.dirac (x j)) {x₀}) (fun _ _ ↦ zero_le)
+      (Finset.mem_univ k)
+  rw [h0, hk, Measure.dirac_apply_of_mem (mem_singleton x₀), mul_one, nonpos_iff_eq_zero,
+    ENNReal.ofReal_eq_zero] at h1
+  exact hwk.not_ge h1
+
+/-- On a set `Y` without arbitrage that carries the null, a property holds almost surely under
+every member of the null exactly when it holds on `Y`. -/
+theorem forall_ae_iff_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y)
+    (hYμ : ∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) {p : 𝓧 → Prop} :
+    (∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, p x) ↔ ∀ x ∈ Y, p x := by
+  refine ⟨fun h x hx ↦ ?_, fun h μ hμ ↦ Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) h⟩
+  by_contra hpx
+  obtain ⟨μ, hμ, hμx⟩ := exists_mem_constraintNull_measure_singleton_ne_zero hg hY hx
+  exact hμx (measure_mono_null (singleton_subset_iff.2 hpx) (ae_iff.1 (h μ hμ)))
+
 /-! ### The complete class theorem -/
 
 /-- **The complete class theorem on a set without arbitrage**: a measurable `f` with a nonpositive