feat: nulls generated by constraints, their bets, and the complete class theorem for finitely many constraints

LMLExplore/Algebra/Order/Archimedean/Basic.lean

@@ -0,0 +1,33 @@
+/-
+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.Algebra.Order.Archimedean.Basic
+
+/-!
+# Inequalities up to `1 / (n + 1)` in Archimedean semifields
+
+In an Archimedean linearly ordered semifield with `ExistsAddOfLE` (for instance, any Archimedean
+linearly ordered field), an inequality that holds up to `1 / (n + 1)` for every natural number `n`
+holds exactly. This is the sequential form of `le_of_forall_pos_le_add`, for
+arguments that index the error by `ℕ`, such as a finite intersection over countably many closed
+sets.
+
+## Main statements
+
+* `le_of_forall_nat_le_add_one_div`: if `a ≤ b + 1 / (n + 1)` for every `n : ℕ`, then `a ≤ b`.
+-/
+
+public section
+
+variable {K : Type*} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K]
+  [ExistsAddOfLE K] {a b : K}
+
+/-- If `a ≤ b + 1 / (n + 1)` for every natural number `n`, then `a ≤ b`. -/
+theorem le_of_forall_nat_le_add_one_div (h : ∀ n : ℕ, a ≤ b + 1 / ((n : K) + 1)) : a ≤ b :=
+  le_of_forall_pos_le_add fun _ hε ↦
+    let ⟨n, hn⟩ := exists_nat_one_div_lt hε
+    (h n).trans ((add_le_add_iff_left b).2 hn.le)

LMLExplore/Algebra/Order/Field/Basic.lean

@@ -6,17 +6,21 @@ Authors: LMLExplore contributors
 module
 
 public import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
 
 /-!
-# Bounds on `x y / (x + y)`
+# Bounds in linearly ordered fields
 
 For nonnegative `x` and `y` in a linearly ordered semifield, `x y / (x + y)` (half the harmonic
-mean of `x` and `y`) is at most `x` and at most `y`.
+mean of `x` and `y`) is at most `x` and at most `y`. In a linearly ordered field, an affine
+function `t ↦ A + t * B` that is bounded below on `t ≥ 0` has a nonnegative slope `B`.
 
 ## Main statements
 
 * `mul_div_add_le_left`: `x y / (x + y) ≤ x` for `0 ≤ x` and `0 ≤ y`.
 * `mul_div_add_le_right`: `x y / (x + y) ≤ y` for `0 ≤ x` and `0 ≤ y`.
+* `nonneg_of_forall_lt_add_mul`: if `v < A + t * B` for every `t ≥ 0`, then `0 ≤ B`.
 -/
 
 public section
@@ -32,3 +36,13 @@ theorem mul_div_add_le_left (hx : 0 ≤ x) (hy : 0 ≤ y) : x * y / (x + y) ≤
 theorem mul_div_add_le_right (hx : 0 ≤ x) (hy : 0 ≤ y) : x * y / (x + y) ≤ y := by
   rw [mul_comm, add_comm]
   exact mul_div_add_le_left hy hx
+
+/-- If `v < A + t * B` for every `t ≥ 0`, then `B` is nonnegative. -/
+theorem nonneg_of_forall_lt_add_mul {K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K]
+    {A B v : K} (h : ∀ t : K, 0 ≤ t → v < A + t * B) : 0 ≤ B := by
+  by_contra! hB
+  have h0 : v < A := by simpa using h 0 le_rfl
+  -- at `t = (A - v) / -B`, the affine function takes the value `v`
+  have h1 := h ((A - v) / -B) (div_nonneg (sub_nonneg.2 h0.le) (neg_nonneg.2 hB.le))
+  field_simp [hB.ne] at h1
+  linarith

LMLExplore/EValues/ConstraintNull/Basic.lean

@@ -0,0 +1,278 @@
+/-
+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.Analysis.Convex.Simplex
+public import LMLExplore.MeasureTheory.Measure.Weighted
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+public import Statlib.EValues.EVariable
+
+/-!
+# Nulls generated by constraints and their bets
+
+The null generated by a set `Φ` of real functions on a measurable space `𝓧`,
+`ProbabilityTheory.constraintNull Φ`, is the set of probability measures under which every member
+of `Φ` is integrable with a nonpositive integral [LRR26, Definition 2.1]. Equality constraints are
+encoded by putting both `f` and `-f` in `Φ`. The definition asks no measurability of the
+constraints, since integrability under a measure contains almost everywhere strong measurability;
+the results that need measurable constraints assume it.
+
+For finitely many constraints `g : ι → 𝓧 → ℝ`, the null generated by `Set.range g` comes with its
+bets, `ProbabilityTheory.constraintBets g`: the weights `π : ι → ℝ≥0` for which
+`1 + ∑ i, π i * g i` is nonnegative almost surely under every member of the null
+[LRR26, Corollary 3.3]. For measurable constraints, each bet gives the e-variable
+`x ↦ ENNReal.ofReal (1 + ∑ i, π i * g i x)`, and the complete class theorem
+(`LMLExplore.EValues.ConstraintNull.CompleteClass`) shows that these dominate every e-variable,
+almost surely under every member of the null.
+
+## Main definitions
+
+* `ProbabilityTheory.constraintNull Φ`: the null generated by the constraints `Φ`.
+* `ProbabilityTheory.constraintBets g`: the bets on the finitely many constraints `g`.
+
+## Main statements
+
+* `ProbabilityTheory.constraintNull_anti`, `ProbabilityTheory.constraintNull_union`,
+  `ProbabilityTheory.constraintNull_empty`: the null is antitone in the constraints, turns unions
+  of constraint sets into intersections, and is the set of all probability measures without
+  constraints.
+* `ProbabilityTheory.sum_smul_dirac_mem_constraintNull_iff`,
+  `ProbabilityTheory.dirac_mem_constraintNull_iff`: the finitely supported members of the null,
+  for measurable constraints.
+* `ProbabilityTheory.sum_mul_nonpos_of_forall_integral_nonpos`,
+  `ProbabilityTheory.sum_ofReal_mul_le_one_of_isEVar`: the means of a function with nonpositive
+  integrals, and of an e-variable, under the finitely supported members of the null.
+* `ProbabilityTheory.integrable_sum_mul_of_mem_constraintNull`,
+  `ProbabilityTheory.integral_sum_mul_nonpos_of_mem_constraintNull`: under a member of the null,
+  every combination of finitely many constraints is integrable, with a nonpositive integral when
+  its weights are nonnegative.
+* `ProbabilityTheory.zero_mem_constraintBets`, `ProbabilityTheory.convex_constraintBets`: the bets
+  form a convex set containing `0`.
+* `ProbabilityTheory.lintegral_ofReal_one_add_of_mem_constraintBets`,
+  `ProbabilityTheory.lintegral_ofReal_one_add_le_one_of_mem_constraintBets`: the expectation of a
+  bet under a member of the null is `1 + ∑ i, π i * ∫ g i`, at most `1`.
+* `ProbabilityTheory.isEVar_ofReal_one_add_of_mem_constraintBets`: for measurable constraints, a
+  bet is an e-variable for the null.
+
+## 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*} [MeasurableSpace 𝓧] {Φ Ψ : Set (𝓧 → ℝ)} {μ : Measure 𝓧}
+  {f : 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞}
+
+/-! ### The null generated by a set of constraints -/
+
+/-- The null generated by a set `Φ` of constraints [LRR26, Definition 2.1]: the probability
+measures under which every constraint is integrable with a nonpositive integral. -/
+def constraintNull (Φ : Set (𝓧 → ℝ)) : Set (Measure 𝓧) :=
+  {μ | IsProbabilityMeasure μ ∧ ∀ f ∈ Φ, Integrable f μ ∧ ∫ x, f x ∂μ ≤ 0}
+
+/-- Membership in the null generated by constraints. -/
+theorem mem_constraintNull_iff :
+    μ ∈ constraintNull Φ ↔ IsProbabilityMeasure μ ∧ ∀ f ∈ Φ, Integrable f μ ∧ ∫ x, f x ∂μ ≤ 0 :=
+  Iff.rfl
+
+/-- The members of the null generated by constraints are probability measures. -/
+theorem isProbabilityMeasure_of_mem_constraintNull (hμ : μ ∈ constraintNull Φ) :
+    IsProbabilityMeasure μ :=
+  hμ.1
+
+/-- The members of the null generated by constraints integrate the constraints. -/
+theorem integrable_of_mem_constraintNull (hμ : μ ∈ constraintNull Φ) (hf : f ∈ Φ) :
+    Integrable f μ :=
+  (hμ.2 f hf).1
+
+/-- The constraints have nonpositive integrals under the members of the null that they
+generate. -/
+theorem integral_nonpos_of_mem_constraintNull (hμ : μ ∈ constraintNull Φ) (hf : f ∈ Φ) :
+    ∫ x, f x ∂μ ≤ 0 :=
+  (hμ.2 f hf).2
+
+/-- The null generated by constraints shrinks as constraints are added. -/
+@[gcongr]
+theorem constraintNull_anti (h : Φ ⊆ Ψ) : constraintNull Ψ ⊆ constraintNull Φ :=
+  fun _ hμ ↦ ⟨hμ.1, fun f hf ↦ hμ.2 f (h hf)⟩
+
+/-- Without constraints, the null is the set of all probability measures. -/
+@[simp]
+theorem constraintNull_empty :
+    constraintNull (∅ : Set (𝓧 → ℝ)) = {μ : Measure 𝓧 | IsProbabilityMeasure μ} := by
+  ext μ
+  simp [mem_constraintNull_iff]
+
+/-- The null generated by a union of constraint sets is the intersection of the nulls. -/
+theorem constraintNull_union :
+    constraintNull (Φ ∪ Ψ) = constraintNull Φ ∩ constraintNull Ψ := by
+  ext μ
+  simp only [mem_constraintNull_iff, mem_union, mem_inter_iff]
+  grind
+
+/-- The members of the null generated by finitely or infinitely many constraints `g i`. -/
+theorem mem_constraintNull_range_iff {g : ι → 𝓧 → ℝ} :
+    μ ∈ constraintNull (range g) ↔
+      IsProbabilityMeasure μ ∧ ∀ i, Integrable (g i) μ ∧ ∫ x, g i x ∂μ ≤ 0 := by
+  simp [mem_constraintNull_iff]
+
+/-- For measurable constraints, a finitely supported measure with nonnegative weights `w k` at the
+points `x k` belongs to the null exactly when the weights sum to `1` and every constraint has a
+nonpositive mean `∑ k, w k * f (x k)` under it. -/
+theorem sum_smul_dirac_mem_constraintNull_iff (hΦ : ∀ f ∈ Φ, Measurable f) {α : Type*}
+    [Fintype α] {x : α → 𝓧} {w : α → ℝ} (hw : ∀ k, 0 ≤ w k) :
+    ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) ∈ constraintNull Φ ↔
+      ∑ k, w k = 1 ∧ ∀ f ∈ Φ, ∑ k, w k * f (x k) ≤ 0 := by
+  have huniv : (∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k)) univ =
+      ENNReal.ofReal (∑ k, w k) := by
+    simp [ENNReal.ofReal_sum_of_nonneg fun k _ ↦ hw k]
+  have hint : ∀ f ∈ Φ, Integrable f (∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k)) :=
+    fun f hf ↦ integrable_finsetSum_measure.2 fun k _ ↦
+      (integrable_dirac' (hΦ f hf).stronglyMeasurable (by simp)).smul_measure
+        ENNReal.ofReal_ne_top
+  rw [mem_constraintNull_iff, isProbabilityMeasure_iff, huniv, ENNReal.ofReal_eq_one]
+  refine and_congr Iff.rfl (forall₂_congr fun f hf ↦ ?_)
+  rw [integral_sum_smul_dirac hw (hΦ f hf).stronglyMeasurable]
+  simp_rw [smul_eq_mul]
+  exact and_iff_right (hint f hf)
+
+/-- For measurable constraints, the Dirac measure at `x` belongs to the null exactly when every
+constraint is nonpositive at `x`. -/
+theorem dirac_mem_constraintNull_iff (hΦ : ∀ f ∈ Φ, Measurable f) {x : 𝓧} :
+    Measure.dirac x ∈ constraintNull Φ ↔ ∀ f ∈ Φ, f x ≤ 0 := by
+  have h := sum_smul_dirac_mem_constraintNull_iff hΦ (α := Unit) (x := fun _ ↦ x)
+    (w := fun _ ↦ 1) fun _ ↦ zero_le_one
+  simpa using h
+
+/-- For measurable constraints `Φ`, a measurable `f` with a nonpositive integral under every member
+of the null has a nonpositive mean under every finitely supported law under which the constraints
+have nonpositive means. -/
+theorem sum_mul_nonpos_of_forall_integral_nonpos (hΦ : ∀ f ∈ Φ, Measurable f) (hf : Measurable f)
+    (h : ∀ μ ∈ constraintNull Φ, ∫ x, f x ∂μ ≤ 0) {α : Type*} [Fintype α] {x : α → 𝓧}
+    {w : α → ℝ} (hw : w ∈ simplex α) (hwΦ : ∀ φ ∈ Φ, ∑ k, w k * φ (x k) ≤ 0) :
+    ∑ k, w k * f (x k) ≤ 0 := by
+  rw [mem_simplex_iff] at hw
+  have hμ := (sum_smul_dirac_mem_constraintNull_iff hΦ hw.1).2 ⟨hw.2, hwΦ⟩
+  simpa [integral_sum_smul_dirac hw.1 hf.stronglyMeasurable] using h _ hμ
+
+/-- For measurable constraints `Φ`, an e-variable for the null has a mean at most `1` under every
+finitely supported law under which the constraints have nonpositive means. -/
+theorem sum_ofReal_mul_le_one_of_isEVar (hΦ : ∀ f ∈ Φ, Measurable f)
+    (hE : IsEVar E (constraintNull Φ)) {α : Type*} [Fintype α] {x : α → 𝓧} {w : α → ℝ}
+    (hw : w ∈ simplex α) (hwΦ : ∀ φ ∈ Φ, ∑ k, w k * φ (x k) ≤ 0) :
+    ∑ k, ENNReal.ofReal (w k) * E (x k) ≤ 1 := by
+  rw [mem_simplex_iff] at hw
+  have hμ := (sum_smul_dirac_mem_constraintNull_iff hΦ hw.1).2 ⟨hw.2, hwΦ⟩
+  have := isProbabilityMeasure_of_mem_constraintNull hμ
+  have h1 := hE.lintegral_le_measure_univ _ hμ
+  rw [measure_univ, lintegral_finsetSum_measure] at h1
+  simpa [lintegral_smul_measure, lintegral_dirac' _ hE.measurable] using h1
+
+/-! ### Nonnegative combinations of finitely many constraints -/
+
+variable [Fintype ι] {g : ι → 𝓧 → ℝ} {π π' : ι → ℝ≥0}
+
+/-- The members of the null generated by finitely many constraints `g i` integrate every
+combination of the constraints. -/
+theorem integrable_sum_mul_of_mem_constraintNull (hμ : μ ∈ constraintNull (range g))
+    (ρ : ι → ℝ) : Integrable (fun x ↦ ∑ i, ρ i * g i x) μ :=
+  integrable_finsetSum _ fun i _ ↦
+    (integrable_of_mem_constraintNull hμ (mem_range_self i)).const_mul (ρ i)
+
+/-- A nonnegative combination of the integrals of the constraints `g i` under a member of the
+null is nonpositive. -/
+theorem sum_mul_integral_nonpos_of_mem_constraintNull (hμ : μ ∈ constraintNull (range g))
+    {ρ : ι → ℝ} (hρ : ∀ i, 0 ≤ ρ i) : ∑ i, ρ i * ∫ x, g i x ∂μ ≤ 0 :=
+  Finset.sum_nonpos fun i _ ↦ mul_nonpos_of_nonneg_of_nonpos (hρ i)
+    (integral_nonpos_of_mem_constraintNull hμ (mem_range_self i))
+
+/-- A nonnegative combination of the constraints `g i` has a nonpositive integral under every
+member of the null. -/
+theorem integral_sum_mul_nonpos_of_mem_constraintNull (hμ : μ ∈ constraintNull (range g))
+    {ρ : ι → ℝ} (hρ : ∀ i, 0 ≤ ρ i) : ∫ x, ∑ i, ρ i * g i x ∂μ ≤ 0 := by
+  rw [integral_finsetSum _ fun i _ ↦
+    (integrable_of_mem_constraintNull hμ (mem_range_self i)).const_mul (ρ i)]
+  simp_rw [integral_const_mul]
+  exact sum_mul_integral_nonpos_of_mem_constraintNull hμ hρ
+
+/-! ### Bets on finitely many constraints -/
+
+/-- The bets on finitely many constraints `g` [LRR26, Corollary 3.3]: the weights `π ≥ 0` for
+which `1 + ∑ i, π i * g i` is nonnegative almost surely under every member of the null generated
+by the `g i`. -/
+def constraintBets (g : ι → 𝓧 → ℝ) : Set (ι → ℝ≥0) :=
+  {π | ∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ 1 + ∑ i, (π i : ℝ) * g i x}
+
+/-- Membership in the bets on finitely many constraints. -/
+theorem mem_constraintBets_iff :
+    π ∈ constraintBets g ↔
+      ∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ 1 + ∑ i, (π i : ℝ) * g i x :=
+  Iff.rfl
+
+/-- The zero bet, which keeps the wealth at `1`. -/
+@[simp]
+theorem zero_mem_constraintBets : 0 ∈ constraintBets g :=
+  fun _ _ ↦ ae_of_all _ fun _ ↦ by simp
+
+/-- The bets form a convex set. -/
+theorem convex_constraintBets : Convex ℝ≥0 (constraintBets g) := by
+  intro π hπ π' hπ' a b _ _ hab μ hμ
+  filter_upwards [hπ μ hμ, hπ' μ hμ] with x hx hx'
+  have h : 1 + ∑ i, (((a • π + b • π') i : ℝ≥0) : ℝ) * g i x =
+      a * (1 + ∑ i, (π i : ℝ) * g i x) + b * (1 + ∑ i, (π' i : ℝ) * g i x) := by
+    have hab' : (a : ℝ) + b = 1 := mod_cast hab
+    simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul, NNReal.coe_add, NNReal.coe_mul,
+      add_mul, Finset.sum_add_distrib, mul_add, Finset.mul_sum, mul_assoc]
+    linear_combination hab'.symm
+  rw [h]
+  positivity
+
+/-- The expectation of `1 + ∑ i, π i * g i`, under a finite measure that integrates the
+constraints and under which it is almost everywhere nonnegative. -/
+theorem lintegral_ofReal_one_add_sum_mul [IsFiniteMeasure μ] (hgμ : ∀ i, Integrable (g i) μ)
+    (π : ι → ℝ) (h : ∀ᵐ x ∂μ, 0 ≤ 1 + ∑ i, π i * g i x) :
+    ∫⁻ x, ENNReal.ofReal (1 + ∑ i, π i * g i x) ∂μ =
+      ENNReal.ofReal (μ.real univ + ∑ i, π i * ∫ x, g i x ∂μ) := by
+  have hgi : ∀ i, Integrable (fun x ↦ π i * g i x) μ := fun i ↦ (hgμ i).const_mul (π i)
+  have hint : Integrable (fun x ↦ 1 + ∑ i, π i * g i x) μ :=
+    (integrable_const 1).add (integrable_finsetSum _ fun i _ ↦ hgi i)
+  rw [← ofReal_integral_eq_lintegral_ofReal hint h,
+    integral_add (integrable_const 1) (integrable_finsetSum _ fun i _ ↦ hgi i),
+    integral_finsetSum _ fun i _ ↦ hgi i]
+  simp only [integral_const, smul_eq_mul, mul_one, integral_const_mul]
+
+/-- The expectation of a bet under a member of the null. -/
+theorem lintegral_ofReal_one_add_of_mem_constraintBets (hπ : π ∈ constraintBets g)
+    (hμ : μ ∈ constraintNull (range g)) :
+    ∫⁻ x, ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) ∂μ =
+      ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * ∫ x, g i x ∂μ) := by
+  have := isProbabilityMeasure_of_mem_constraintNull hμ
+  rw [lintegral_ofReal_one_add_sum_mul
+    (fun i ↦ integrable_of_mem_constraintNull hμ (mem_range_self i)) _ (hπ μ hμ), probReal_univ]
+
+/-- The expectation of a bet under a member of the null is at most `1`. -/
+theorem lintegral_ofReal_one_add_le_one_of_mem_constraintBets (hπ : π ∈ constraintBets g)
+    (hμ : μ ∈ constraintNull (range g)) :
+    ∫⁻ x, ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) ∂μ ≤ 1 := by
+  rw [lintegral_ofReal_one_add_of_mem_constraintBets hπ hμ, ← ENNReal.ofReal_one]
+  refine ENNReal.ofReal_le_ofReal ?_
+  linarith [sum_mul_integral_nonpos_of_mem_constraintNull hμ fun i ↦ (π i).coe_nonneg]
+
+/-- A bet on measurable constraints is an e-variable for the null that they generate. -/
+theorem isEVar_ofReal_one_add_of_mem_constraintBets (hg : ∀ i, Measurable (g i))
+    (hπ : π ∈ constraintBets g) :
+    IsEVar (fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) (constraintNull (range g)) :=
+  IsEVar.of_lintegral_le_one (fun _ ↦ isProbabilityMeasure_of_mem_constraintNull) (by fun_prop)
+    fun _ hμ ↦ lintegral_ofReal_one_add_le_one_of_mem_constraintBets hπ hμ
+
+end ProbabilityTheory