diff --git a/LMLExplore/Algebra/Order/Archimedean/Basic.lean b/LMLExplore/Algebra/Order/Archimedean/Basic.lean new file mode 100644 index 00000000..f2ac98f6 --- /dev/null +++ b/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) diff --git a/LMLExplore/Algebra/Order/Field/Basic.lean b/LMLExplore/Algebra/Order/Field/Basic.lean index f11cca86..dab3f138 100644 --- a/LMLExplore/Algebra/Order/Field/Basic.lean +++ b/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 diff --git a/LMLExplore/EValues/ConstraintNull/Basic.lean b/LMLExplore/EValues/ConstraintNull/Basic.lean new file mode 100644 index 00000000..c60f0231 --- /dev/null +++ b/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 diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean new file mode 100644 index 00000000..cc72149e --- /dev/null +++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean @@ -0,0 +1,599 @@ +/- +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.Basic +import LMLExplore.Algebra.Order.Archimedean.Basic +import LMLExplore.Algebra.Order.Field.Basic +import LMLExplore.LinearAlgebra.Pi +import Mathlib.Analysis.Convex.Combination +import Mathlib.Analysis.Convex.Topology +import Mathlib.Analysis.LocallyConvex.Separation +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas +import Mathlib.Topology.Algebra.Module.FiniteDimension + +/-! +# The complete class theorem for finitely many constraints + +Let `g i`, for `i` in a finite type, be measurable real constraints on a measurable space `𝓧`. The +complete class theorem of Larsson, Ramdas and Ruf [LRR26, Theorem 3.1] says that a measurable +`f : 𝓧 → ℝ` has `∫ f ∂μ ≤ 0` under every member `μ` of the null `constraintNull (range g)` exactly +when `f ≤ ∑ i, π i * g i` almost surely under every member of the null, for some weights `π ≥ 0`. +In particular, the e-variables for the null are the measurable functions dominated, almost surely +under every member of the null, by a bet `1 + ∑ i, π i * g i`. + +The proof of [LRR26] shows that a cone is closed in a weak topology and applies a bipolar theorem. +The proof here is finite-dimensional, in three steps. + +* *A set carrying the null.* Removing, finitely many times, the set where a nonnegative + combination of the constraints that is nonnegative on what remains is positive, gives a + 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. +* *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 + (`ProbabilityTheory.nonredundantWeights`) and that keep the combination above `-c` at well chosen + finitely many points have a total mass at most proportional to `c` [LRR26, proof of Lemma 7.2], + and every nonnegative combination has such weights on `Y` [LRR26, Lemma 3.2]. A finite + intersection argument in the compact set of these weights removes `δ` and the finiteness. + +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`. + +## Main definitions + +* `ProbabilityTheory.NoArbitrageOn a Y`: every nonnegative combination of the functions `a i` that + is nonnegative on `Y` vanishes on `Y`. +* `ProbabilityTheory.nonredundantWeights a Y`: the nonnegative weights whose support is not + redundant on `Y` [LRR26, (3.1)]. + +## Main statements + +* `ProbabilityTheory.exists_mem_nonredundantWeights_sum_mul_eq`: every nonnegative combination is, + 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.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_integral_nonpos_iff_exists_ae_le`: **the complete class theorem** + [LRR26, Theorem 3.1]. +* `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. + +## 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 ι] {a : ι → 𝓧 → ℝ} {Y : Set 𝓧} + +/-! ### Nonredundant weights and the absence of arbitrage -/ + +/-- The functions `a i` admit no arbitrage on `Y`: every nonnegative combination of them that is +nonnegative on `Y` vanishes on `Y`. -/ +def NoArbitrageOn (a : ι → 𝓧 → ℝ) (Y : Set 𝓧) : Prop := + ∀ ρ : ι → ℝ, (∀ i, 0 ≤ ρ i) → (∀ x ∈ Y, 0 ≤ ∑ i, ρ i * a i x) → + ∀ x ∈ Y, ∑ i, ρ i * a i x = 0 + +/-- The absence of arbitrage on `Y`, restated. -/ +theorem noArbitrageOn_iff : NoArbitrageOn a Y ↔ ∀ ρ : ι → ℝ, (∀ i, 0 ≤ ρ i) → + (∀ x ∈ Y, 0 ≤ ∑ i, ρ i * a i x) → ∀ x ∈ Y, ∑ i, ρ i * a i x = 0 := + Iff.rfl + +/-- The nonnegative weights whose support is not redundant on `Y` [LRR26, (3.1)]: no nonzero +nonnegative combination of the functions `a i` with support inside that of the weights vanishes +on `Y`. -/ +def nonredundantWeights (a : ι → 𝓧 → ℝ) (Y : Set 𝓧) : Set (ι → ℝ) := + {π | (∀ i, 0 ≤ π i) ∧ ∀ ρ : ι → ℝ, (∀ i, 0 ≤ ρ i) → (∀ i, π i = 0 → ρ i = 0) → + (∀ x ∈ Y, ∑ i, ρ i * a i x = 0) → ρ = 0} + +/-- Membership in the nonredundant weights. -/ +theorem mem_nonredundantWeights_iff {π : ι → ℝ} : + π ∈ nonredundantWeights a Y ↔ (∀ i, 0 ≤ π i) ∧ ∀ ρ : ι → ℝ, (∀ i, 0 ≤ ρ i) → + (∀ i, π i = 0 → ρ i = 0) → (∀ x ∈ Y, ∑ i, ρ i * a i x = 0) → ρ = 0 := + Iff.rfl + +/-- The nonredundant weights form a closed set [LRR26, Section 3]. -/ +theorem isClosed_nonredundantWeights : IsClosed (nonredundantWeights a Y) := by + have h : nonredundantWeights a Y = (⋂ i, {π : ι → ℝ | 0 ≤ π i}) ∩ + ⋂ (ρ : ι → ℝ) (_ : (∀ i, 0 ≤ ρ i) ∧ (∀ x ∈ Y, ∑ i, ρ i * a i x = 0) ∧ ρ ≠ 0), + ⋃ i ∈ {i | ρ i ≠ 0}, {π | π i = 0} := by + ext π + simp only [mem_nonredundantWeights_iff, mem_inter_iff, mem_iInter, mem_ofPred_eq, mem_iUnion, + exists_prop, and_imp] + refine and_congr_right fun _ ↦ forall_congr' fun ρ ↦ ?_ + constructor + · intro h hρ hρa hne + by_contra! hcon + exact hne (h hρ (fun i hi ↦ by_contra fun h' ↦ hcon i h' hi) hρa) + · intro h hρ hπρ hρa + by_contra hne + obtain ⟨i, hi, hπi⟩ := h hρ hρa hne + exact hi (hπρ i hπi) + rw [h] + refine (isClosed_iInter fun i ↦ isClosed_le continuous_const + (by fun_prop : Continuous fun π : ι → ℝ ↦ π i)).inter + (isClosed_iInter fun (ρ : ι → ℝ) ↦ isClosed_iInter fun _ ↦ + (toFinite {i | ρ i ≠ 0}).isClosed_biUnion fun i _ ↦ + isClosed_eq (by fun_prop : Continuous fun π : ι → ℝ ↦ π i) continuous_const) + +/-- The nonredundant weights form a cone. -/ +theorem smul_mem_nonredundantWeights {π : ι → ℝ} (hπ : π ∈ nonredundantWeights a Y) {c : ℝ} + (hc : 0 ≤ c) : c • π ∈ nonredundantWeights a Y := by + refine ⟨fun i ↦ by simpa using mul_nonneg hc (hπ.1 i), fun ρ hρ hρπ hρa ↦ ?_⟩ + refine hπ.2 ρ hρ (fun i hi ↦ hρπ i ?_) hρa + simp [hi] + +/-- Every nonnegative combination of the functions `a i` is, on `Y`, a combination with +nonredundant weights [LRR26, Lemma 3.2]. -/ +theorem exists_mem_nonredundantWeights_sum_mul_eq {π : ι → ℝ} (hπ : ∀ i, 0 ≤ π i) : + ∃ π' ∈ nonredundantWeights a Y, ∀ x ∈ Y, ∑ i, π' i * a i x = ∑ i, π i * a i x := by + classical + induction h : (Finset.univ.filter fun i ↦ π i ≠ 0).card using Nat.strong_induction_on + generalizing π with + | _ n ih => + by_cases hK : π ∈ nonredundantWeights a Y + · exact ⟨π, hK, fun _ _ ↦ rfl⟩ + simp only [mem_nonredundantWeights_iff, hπ, implies_true, true_and, not_forall] at hK + obtain ⟨ρ, hρ, hπρ, hρa, hne⟩ := hK + have hsne : (Finset.univ.filter fun i ↦ ρ i ≠ 0).Nonempty := by + by_contra hs + refine hne (funext fun i ↦ ?_) + by_contra hi + exact hs ⟨i, by simpa using hi⟩ + obtain ⟨j, hj, hmin⟩ := (Finset.univ.filter fun i ↦ ρ i ≠ 0).exists_min_image + (fun i ↦ π i / ρ i) hsne + have hj' : ρ j ≠ 0 := (Finset.mem_filter.1 hj).2 + have hπj : π j ≠ 0 := fun h ↦ hj' (hπρ j h) + set t := π j / ρ j with ht + set π'' : ι → ℝ := fun i ↦ π i - t * ρ i with hπ'' + have hπ''0 : ∀ i, 0 ≤ π'' i := by + intro i + by_cases hi : ρ i = 0 + · simp [π'', hi, hπ i] + · have hρi : 0 < ρ i := lt_of_le_of_ne (hρ i) (Ne.symm hi) + have := hmin i (Finset.mem_filter.2 ⟨Finset.mem_univ _, hi⟩) + rw [le_div_iff₀ hρi] at this + simp only [π'', sub_nonneg] + exact this + have hπ''j : π'' j = 0 := by + simp only [π'', ht] + field_simp + ring + have hsub : (Finset.univ.filter fun i ↦ π'' i ≠ 0) ⊂ + (Finset.univ.filter fun i ↦ π i ≠ 0) := by + refine Finset.ssubset_iff_of_subset ?_ |>.2 ⟨j, by simpa using hπj, by simp [hπ''j]⟩ + intro i hi + simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi ⊢ + intro hπi + exact hi (by simp [π'', hπi, hπρ i hπi]) + obtain ⟨π', hπ', heq⟩ := ih _ (h ▸ Finset.card_lt_card hsub) hπ''0 rfl + refine ⟨π', hπ', fun x hx ↦ (heq x hx).trans ?_⟩ + have := hρa x hx + simp only [π'', sub_mul, Finset.sum_sub_distrib, mul_assoc, ← Finset.mul_sum, this, + mul_zero, sub_zero] + +/-- A closed set of nonredundant weights with bounded total mass is compact. -/ +theorem isCompact_nonredundantWeights_inter {T : Set (ι → ℝ)} (hT : IsClosed T) {c : ℝ} + (hc : ∀ π ∈ nonredundantWeights a Y ∩ T, ∑ i, π i ≤ c) : + IsCompact (nonredundantWeights a Y ∩ T) := by + refine Metric.isCompact_of_isClosed_isBounded (isClosed_nonredundantWeights.inter hT) ?_ + refine (Metric.isBounded_iff_subset_closedBall 0).2 ⟨max c 0, fun π hπ ↦ ?_⟩ + rw [Metric.mem_closedBall, dist_zero_right, pi_norm_le_iff_of_nonneg (le_max_right _ _)] + intro i + rw [Real.norm_of_nonneg (hπ.1.1 i)] + exact ((Finset.single_le_sum (fun j _ ↦ hπ.1.1 j) (Finset.mem_univ i)).trans + (hc π hπ)).trans (le_max_left _ _) + +/-- Without arbitrage on `Y`, there are a finite set `F₀ ⊆ Y` and `R ≥ 0` such that every +nonredundant weight keeping the combination of the functions `a i` above `-c` on `F₀` has total +mass at most `R * c` [LRR26, proof of Lemma 7.2]. -/ +theorem exists_finset_sum_le_of_noArbitrageOn (h : NoArbitrageOn a Y) : + ∃ F₀ : Finset 𝓧, ↑F₀ ⊆ Y ∧ ∃ R : ℝ, 0 ≤ R ∧ ∀ π ∈ nonredundantWeights a Y, ∀ c : ℝ, + 0 ≤ c → (∀ x ∈ F₀, -c ≤ ∑ i, π i * a i x) → ∑ i, π i ≤ R * c := by + classical + -- The nonredundant weights of total mass `1` form a compact set `S`. Without arbitrage, it + -- misses the intersection of the closed sets `t (x, n)` of the weights keeping the combination + -- above `-1 / (n + 1)` at `x ∈ Y`. + set S := nonredundantWeights a Y ∩ {ρ | ∑ i, ρ i = 1} + have hS : IsCompact S := isCompact_nonredundantWeights_inter + (isClosed_eq (by fun_prop) continuous_const) (c := 1) fun ρ hρ ↦ hρ.2.le + let t : Y × ℕ → Set (ι → ℝ) := fun p ↦ {ρ | -(1 / ((p.2 : ℝ) + 1)) ≤ ∑ i, ρ i * a i p.1} + have htc : ∀ p, IsClosed (t p) := fun p ↦ isClosed_le continuous_const (by fun_prop) + have hdisj : Disjoint S (⋂ p, t p) := by + rw [disjoint_left] + rintro ρ ⟨hρK, hρS⟩ hρt + simp only [mem_iInter, t, mem_ofPred_eq] at hρt + have h0 : ∀ x ∈ Y, 0 ≤ ∑ i, ρ i * a i x := fun x hx ↦ + le_of_forall_nat_le_add_one_div fun n ↦ by + have := hρt (⟨x, hx⟩, n) + simp only at this + linarith + have hρ0 := hρK.2 ρ hρK.1 (fun i hi ↦ hi) (h ρ hρK.1 h0) + simp [hρ0] at hρS + -- Finite subcover: finitely many `t p`, `p ∈ u`, already miss `S`; their points form `F₀`. + obtain ⟨u, hu⟩ := hS.elim_finite_subfamily_closed t htc hdisj + set N := u.sup Prod.snd + refine ⟨u.image fun p ↦ (p.1 : 𝓧), ?_, (N : ℝ) + 1, by positivity, ?_⟩ + · intro x hx + simp only [Finset.coe_image, mem_image, Finset.mem_coe] at hx + obtain ⟨p, -, rfl⟩ := hx + exact p.1.2 + intro π hπ c hc hπc + have hsum0 : 0 ≤ ∑ i, π i := Finset.sum_nonneg fun i _ ↦ hπ.1 i + rcases hsum0.eq_or_lt with hs | hs + · rw [← hs] + positivity + -- Normalisation to the simplex: `s⁻¹ • π ∈ S`, so it leaves some `t p` with `p ∈ u`. + set s := ∑ i, π i with hs_def + have hρS : s⁻¹ • π ∈ S := by + refine ⟨smul_mem_nonredundantWeights hπ (inv_nonneg.2 hs.le), ?_⟩ + simp only [mem_ofPred_eq, Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum] + exact inv_mul_cancel₀ hs.ne' + have hnot : s⁻¹ • π ∉ ⋂ p ∈ u, t p := fun h' ↦ disjoint_left.1 hu hρS h' + simp only [mem_iInter, not_forall, t, mem_ofPred_eq, not_le, Pi.smul_apply, + smul_eq_mul, mul_assoc, ← Finset.mul_sum] at hnot + obtain ⟨p, hp, hlt⟩ := hnot + -- The final bound: `-c ≤ ∑ i, π i * a i p.1 < -s / (p.2 + 1) ≤ -s / (N + 1)`. + have hc' := hπc _ (Finset.mem_image_of_mem _ hp) + have hN := Nat.one_div_le_one_div (α := ℝ) (Finset.le_sup (f := Prod.snd) hp) + rw [inv_mul_lt_iff₀ hs] at hlt + have : s * (1 / ((N : ℝ) + 1)) < c := by linarith [mul_le_mul_of_nonneg_left hN hs.le] + rw [mul_one_div, div_lt_iff₀ (by positivity)] at this + linarith + +/-- 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 +separates a compact convex hull from a closed convex set. -/ +private lemma exists_le_add_sum_mul_of_finset {f : 𝓧 → ℝ} + (hf : ∀ (α : Type) [Fintype α] (x : α → 𝓧) (w : α → ℝ), (∀ k, x k ∈ Y) → + w ∈ simplex α → (∀ i, ∑ k, w k * a i (x k) ≤ 0) → ∑ k, w k * f (x k) ≤ 0) + {F : Finset 𝓧} (hF : ↑F ⊆ Y) {δ : ℝ} (hδ : 0 < δ) : + ∃ π : ι → ℝ, (∀ i, 0 ≤ π i) ∧ ∀ x ∈ F, f x ≤ δ + ∑ i, π i * a i x := by + classical + -- Separate the compact convex hull of the points `(f x, (a i x)ᵢ)`, `x ∈ F`, from the closed + -- convex set of the points `(r, y)` with `δ ≤ r` and `y ≤ 0`. + let φ : 𝓧 → ℝ × (ι → ℝ) := fun x ↦ (f x, fun i ↦ a i x) + have hdisj : Disjoint (convexHull ℝ (φ '' F)) (Ici δ ×ˢ Iic 0) := by + rw [disjoint_left] + rintro p hp ⟨hp1, hp2⟩ + obtain ⟨α, _, w, z, hw0, hw1, hz, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hp + choose x hxF hxz using hz + have hsum2 : ∀ i, ∑ k, w k * a i (x k) ≤ 0 := fun i ↦ by + simpa [← hxz, φ, Prod.snd_sum, Finset.sum_apply] using hp2 i + have key := hf α x w (fun k ↦ hF (hxF k)) (mem_simplex_iff.2 ⟨hw0, hw1⟩) hsum2 + have h1 : δ ≤ ∑ k, w k * f (x k) := by simpa [← hxz, φ, Prod.fst_sum] using hp1 + linarith + obtain ⟨ℓ, u, v, hℓP, huv, hℓQ⟩ := geometric_hahn_banach_compact_closed + (convex_convexHull ℝ _) ((F.finite_toSet.image φ).isCompact_convexHull ℝ) + ((convex_Ici δ).prod (convex_Iic 0)) (isClosed_Ici.prod isClosed_Iic) hdisj + -- Read off the separating functional: `ℓ (r, y) = β * r - ∑ i, π i * y i`. + set β := ℓ (1, 0) with hβ_def + set π : ι → ℝ := fun i ↦ -ℓ (0, Pi.single i 1) with hπ_def + have hℓ : ∀ p : ℝ × (ι → ℝ), ℓ p = β * p.1 - ∑ i, π i * p.2 i := fun p ↦ by + simpa [π, mul_comm, sub_eq_add_neg] using + LinearMap.prod_pi_apply_eq_sum_univ (ℓ : ℝ × (ι → ℝ) →ₗ[ℝ] ℝ) p.1 p.2 + -- `ℓ` is bounded below on the closed convex set, so `β` and the `π i` are nonnegative. + have hβ : 0 ≤ β := by + refine nonneg_of_forall_lt_add_mul (A := β * δ) (v := v) fun t ht ↦ ?_ + have := hℓQ (δ + t, 0) ⟨by simpa using ht, mem_Iic.2 le_rfl⟩ + rw [hℓ] at this + simpa [add_mul, mul_comm] using this + have hπ : ∀ i, 0 ≤ π i := by + intro i + refine nonneg_of_forall_lt_add_mul (A := β * δ) (v := v) fun t ht ↦ ?_ + have := hℓQ (δ, fun j ↦ if i = j then -t else 0) + ⟨mem_Ici.2 le_rfl, fun j ↦ by simp only [Pi.zero_apply]; split_ifs <;> linarith⟩ + rw [hℓ] at this + simpa [mul_ite, Finset.sum_ite_eq, mul_comm] using this + have hx : ∀ x ∈ F, β * f x - ∑ i, π i * a i x < u := fun x hx ↦ by + simpa [hℓ, φ] using hℓP (φ x) (subset_convexHull ℝ _ (mem_image_of_mem φ hx)) + have hv : v < β * δ := by simpa [hℓ] using hℓQ (δ, 0) ⟨mem_Ici.2 le_rfl, mem_Iic.2 le_rfl⟩ + rcases hβ.eq_or_lt with hβ0 | hβ0 + · -- The separating functional is vertical: the combination is positive on `F`, and a large + -- multiple of it dominates `f` there. + rw [← hβ0, zero_mul] at hv + set M := (∑ y ∈ F, |f y|) / -u + have hM : 0 ≤ M := div_nonneg (Finset.sum_nonneg fun _ _ ↦ abs_nonneg _) (by linarith) + refine ⟨M • π, fun i ↦ by simpa using mul_nonneg hM (hπ i), fun x hxF ↦ ?_⟩ + have h1 := hx x hxF + rw [← hβ0, zero_mul, zero_sub] at h1 + have h2 : M * -u ≤ M * ∑ i, π i * a i x := mul_le_mul_of_nonneg_left (by linarith) hM + have h3 : M * -u = ∑ y ∈ F, |f y| := div_mul_cancel₀ _ (by linarith) + have h4 : f x ≤ ∑ y ∈ F, |f y| := + (le_abs_self _).trans (Finset.single_le_sum (fun y _ ↦ abs_nonneg (f y)) hxF) + simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, ← Finset.mul_sum] + linarith + · -- Otherwise, dividing by `β` gives `f ≤ δ + ∑ i, β⁻¹ * π i * a i` on `F`. + refine ⟨β⁻¹ • π, fun i ↦ by simpa using mul_nonneg (inv_nonneg.2 hβ) (hπ i), + fun x hxF ↦ ?_⟩ + have h1 := hx x hxF + simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, ← Finset.mul_sum] + have h2 : f x - δ < β⁻¹ * ∑ i, π i * a i x := by + rw [lt_inv_mul_iff₀ hβ0] + nlinarith + linarith + +/-- **The complete class theorem on a set without arbitrage**, in finite-dimensional form: if `f` +has a nonpositive mean under every finitely supported law on `Y` under which the functions `a i` +have nonpositive means, then `f ≤ ∑ i, π i * a i` on `Y` for some nonredundant weights `π`. -/ +theorem exists_mem_nonredundantWeights_le_of_noArbitrageOn (h : NoArbitrageOn a Y) {f : 𝓧 → ℝ} + (hf : ∀ (α : Type) [Fintype α] (x : α → 𝓧) (w : α → ℝ), (∀ k, x k ∈ Y) → + w ∈ simplex α → (∀ i, ∑ k, w k * a i (x k) ≤ 0) → ∑ k, w k * f (x k) ≤ 0) : + ∃ π ∈ nonredundantWeights a Y, ∀ x ∈ Y, f x ≤ ∑ i, π i * a i x := by + classical + -- The nonredundant weights keeping the combination above `-C` on `F₀` form a compact set. + obtain ⟨F₀, hF₀, R, hR, hbound⟩ := exists_finset_sum_le_of_noArbitrageOn h + have hC0 : 0 ≤ 1 + ∑ x ∈ F₀, |f x| := + add_nonneg zero_le_one (Finset.sum_nonneg fun _ _ ↦ abs_nonneg _) + set C := 1 + ∑ x ∈ F₀, |f x| with hC + set T : Set (ι → ℝ) := {π | ∀ x ∈ F₀, -C ≤ ∑ i, π i * a i x} + have hTc : IsClosed T := by + simp only [T, ofPred_forall] + exact isClosed_biInter fun x _ ↦ isClosed_le continuous_const (by fun_prop) + have hs : IsCompact (nonredundantWeights a Y ∩ T) := + isCompact_nonredundantWeights_inter hTc (c := R * C) fun π hπ ↦ + hbound π hπ.1 C hC0 hπ.2 + -- By the finite step, it meets every finite intersection of the closed sets `t (x, n)` of the + -- weights with `f x ≤ 1 / (n + 1) + ∑ i, π i * a i x`, so it meets their intersection. + let t : Y × ℕ → Set (ι → ℝ) := fun p ↦ + {π | f p.1 ≤ 1 / ((p.2 : ℝ) + 1) + ∑ i, π i * a i p.1} + have htc : ∀ p, IsClosed (t p) := fun p ↦ isClosed_le continuous_const (by fun_prop) + obtain ⟨π, ⟨hπK, -⟩, hπt⟩ := hs.inter_iInter_nonempty t htc fun u ↦ by + set N := u.sup Prod.snd + set F := F₀ ∪ u.image fun p ↦ (p.1 : 𝓧) + have hF : ↑F ⊆ Y := by + intro x hx + simp only [F, Finset.coe_union, Finset.coe_image, mem_union, Finset.mem_coe, + mem_image] at hx + rcases hx with hx | ⟨p, -, rfl⟩ + · exact hF₀ hx + · exact p.1.2 + obtain ⟨π, hπ0, hπ⟩ := exists_le_add_sum_mul_of_finset hf hF + (δ := 1 / ((N : ℝ) + 1)) (by positivity) + obtain ⟨π', hπ'K, hπ'eq⟩ := exists_mem_nonredundantWeights_sum_mul_eq (a := a) (Y := Y) hπ0 + refine ⟨π', ⟨hπ'K, fun x hx ↦ ?_⟩, ?_⟩ + · have h1 := hπ x (Finset.mem_union_left _ hx) + have h2 : -|f x| ≤ f x := neg_abs_le _ + have h3 : |f x| ≤ ∑ y ∈ F₀, |f y| := + Finset.single_le_sum (f := fun y ↦ |f y|) (fun y _ ↦ abs_nonneg _) hx + have h4 : 1 / ((N : ℝ) + 1) ≤ 1 := by + rw [div_le_one (by positivity)] + linarith [N.cast_nonneg (α := ℝ)] + rw [hπ'eq x (hF₀ hx)] + linarith + · simp only [mem_iInter] + intro p hp + have h1 := hπ p.1 (Finset.mem_union_right _ (Finset.mem_image_of_mem _ hp)) + have h2 := Nat.one_div_le_one_div (α := ℝ) (Finset.le_sup (f := Prod.snd) hp) + simp only [t, mem_ofPred_eq] + rw [hπ'eq p.1 p.1.2] + linarith + refine ⟨π, hπK, fun x hx ↦ le_of_forall_nat_le_add_one_div fun n ↦ ?_⟩ + have := mem_iInter.1 hπt (⟨x, hx⟩, n) + simp only [t, mem_ofPred_eq] at this + linarith + +/-- Without arbitrage on `Y`, every point of `Y` is charged by a finitely supported law on `Y` +under which the functions `a i` have nonpositive means. This is what makes e-variables for the +null finite on `Y` (`ProbabilityTheory.lt_top_of_isEVar_of_noArbitrageOn`). -/ +theorem exists_charging_family_of_noArbitrageOn (h : NoArbitrageOn a Y) {x₀ : 𝓧} + (hx₀ : x₀ ∈ Y) : + ∃ (α : Type) (_ : Fintype α) (x : α → 𝓧) (w : α → ℝ), (∀ k, x k ∈ Y) ∧ w ∈ simplex α ∧ + (∀ i, ∑ k, w k * a i (x k) ≤ 0) ∧ ∃ k, x k = x₀ ∧ 0 < w k := by + classical + by_contra hcon + -- if no such law charges `x₀`, then `E - 1`, with `E = n • 1_{x₀}`, has nonpositive means + -- under all of them, for any `n` + obtain ⟨F₀, hF₀, R, hR, hbound⟩ := exists_finset_sum_le_of_noArbitrageOn h + obtain ⟨n, hn⟩ := exists_nat_gt (1 + R * ∑ i, |a i x₀|) + set E : 𝓧 → ℝ := fun y ↦ if y = x₀ then (n : ℝ) else 0 + have hE0 : ∀ y, 0 ≤ E y := fun y ↦ by + simp only [E] + split_ifs <;> positivity + have hE : ∀ (α : Type) [Fintype α] (x : α → 𝓧) (w : α → ℝ), (∀ k, x k ∈ Y) → + w ∈ simplex α → (∀ i, ∑ k, w k * a i (x k) ≤ 0) → ∑ k, w k * (E (x k) - 1) ≤ 0 := by + intro α _ x w hxY hw hwa + have : ∀ k, w k * E (x k) = 0 := by + intro k + by_cases hk : x k = x₀ + · have : w k = 0 := by + by_contra hne + exact hcon ⟨α, inferInstance, x, w, hxY, hw, hwa, k, hk, + lt_of_le_of_ne ((mem_simplex_iff.1 hw).1 k) (Ne.symm hne)⟩ + simp [this] + · simp [E, hk] + simp [mul_sub, this, (mem_simplex_iff.1 hw).2] + -- the finite-dimensional theorem dominates `E - 1` by weights of total mass at most `R` + obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_le_of_noArbitrageOn h + (f := fun y ↦ E y - 1) hE + have hsum : ∑ i, π i ≤ R * 1 := hbound π hπK 1 zero_le_one fun x hx ↦ by + have := hπ x (hF₀ hx) + linarith [hE0 x] + -- at `x₀` this gives `n - 1 ≤ R * ∑ i, |a i x₀|`, contradicting the choice of `n` + have h1 := hπ x₀ hx₀ + simp only [E, ↓reduceIte] at h1 + have h2 : ∑ i, π i * a i x₀ ≤ R * ∑ i, |a i x₀| := by + rw [Finset.mul_sum] + refine Finset.sum_le_sum fun i _ ↦ ?_ + calc π i * a i x₀ ≤ π i * |a i x₀| := + mul_le_mul_of_nonneg_left (le_abs_self _) (hπK.1 i) + _ ≤ R * |a i x₀| := mul_le_mul_of_nonneg_right + ((Finset.single_le_sum (fun j _ ↦ hπK.1 j) (Finset.mem_univ i)).trans + (by simpa using hsum)) (abs_nonneg _) + linarith + +/-! ### A set carrying the null -/ + +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 + 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 + intro n + induction n using Nat.strong_induction_on with + | _ n ih => + intro Y hY hμY hn + by_cases hT : NoArbitrageOn g Y + · exact ⟨Y, hY, hμY, hT⟩ + simp only [noArbitrageOn_iff, not_forall] at hT + obtain ⟨ρ, hρ0, hρY, x₀, hx₀, hne⟩ := hT + 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 + intro x hx + simp only [Y', mem_compl_iff, mem_inter_iff, mem_ofPred_eq, not_and, not_le] at hx + by_cases hxY : x ∈ Y + · exact Or.inr (hx hxY) + · exact Or.inl hxY + -- the combination has a nonnegative integrand and a nonpositive integral under the null + 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 + (le_antisymm (integral_sum_mul_nonpos_of_mem_constraintNull hμ hρ0) + (integral_nonneg_of_ae hnn)) + 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) + -- 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 ↦ ?_ + let ℓ : (ι → ℝ) →ₗ[ℝ] ℝ := Fintype.linearCombination ℝ ρ + have hℓ : ∀ y, ℓ (fun i ↦ g i y) = ∑ i, ρ i * g i y := fun y ↦ by + simp [ℓ, Fintype.linearCombination_apply, mul_comm] + have hle : V Y' ≤ LinearMap.ker ℓ := by + refine Submodule.span_le.2 ?_ + rintro _ ⟨y, ⟨hyY, hy⟩, rfl⟩ + simp only [SetLike.mem_coe, LinearMap.mem_ker, hℓ] + exact le_antisymm hy (hρY y hyY) + 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 + +/-- 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) + (hE : IsEVar E (constraintNull (range g))) {x₀ : 𝓧} (hx₀ : x₀ ∈ Y) : E x₀ < ∞ := by + obtain ⟨α, _, x, w, -, hw, hwg, k, hk, hwk⟩ := exists_charging_family_of_noArbitrageOn hY hx₀ + have h2 : ENNReal.ofReal (w k) * E (x k) ≤ 1 := + (Finset.single_le_sum (fun j _ ↦ zero_le) (Finset.mem_univ k)).trans + (sum_ofReal_mul_le_one_of_isEVar (forall_mem_range.2 hg) hE hw (forall_mem_range.2 hwg)) + rw [hk] at h2 + by_contra htop + rw [not_lt, top_le_iff] at htop + rw [htop, ENNReal.mul_top (by simpa using hwk)] at h2 + exact ENNReal.one_ne_top (top_le_iff.1 h2) + +/-! ### The complete class theorem -/ + +/-- **The complete class theorem on a set without arbitrage**: a measurable `f` with a nonpositive +integral under every member of the null is at most `∑ i, π i * g i` on `Y`, for some nonredundant +weights `π`. -/ +theorem exists_mem_nonredundantWeights_le_of_forall_integral_nonpos (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hf : Measurable f) + (h : ∀ μ ∈ constraintNull (range g), ∫ x, f x ∂μ ≤ 0) : + ∃ π ∈ nonredundantWeights g Y, ∀ x ∈ Y, f x ≤ ∑ i, π i * g i x := + exists_mem_nonredundantWeights_le_of_noArbitrageOn hY fun _ _ _ _ _ hw hwg ↦ + sum_mul_nonpos_of_forall_integral_nonpos (forall_mem_range.2 hg) hf h hw + (forall_mem_range.2 hwg) + +/-- **The complete class theorem for e-variables on a set without arbitrage**: every e-variable +for the null is at most `1 + ∑ i, π i * g i` on `Y`, for some nonredundant weights `π`. -/ +theorem exists_mem_nonredundantWeights_toReal_le_of_isEVar (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hE : IsEVar E (constraintNull (range g))) : + ∃ π ∈ nonredundantWeights g Y, ∀ x ∈ Y, (E x).toReal ≤ 1 + ∑ i, π i * g i x := by + obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_le_of_noArbitrageOn hY + (f := fun x ↦ (E x).toReal - 1) fun α _ x w hxY hw hwg ↦ by + have hfin : ∀ k, E (x k) ≠ ∞ := fun k ↦ + (lt_top_of_isEVar_of_noArbitrageOn hg hY hE (hxY k)).ne + have := ENNReal.toReal_mono ENNReal.one_ne_top + (sum_ofReal_mul_le_one_of_isEVar (forall_mem_range.2 hg) hE hw (forall_mem_range.2 hwg)) + rw [ENNReal.toReal_sum fun k _ ↦ ENNReal.mul_ne_top ENNReal.ofReal_ne_top (hfin k)] at this + have hw0 := (mem_simplex_iff.1 hw).1 + simp only [ENNReal.toReal_mul, ENNReal.toReal_ofReal (hw0 _), ENNReal.toReal_one] at this + simp only [mul_sub, mul_one, Finset.sum_sub_distrib, (mem_simplex_iff.1 hw).2] + linarith + exact ⟨π, hπK, fun x hx ↦ by linarith [hπ x hx]⟩ + +/-- **The complete class theorem for finitely many constraints** [LRR26, Theorem 3.1]: for +measurable constraints `g i` and a measurable `f`, the integral of `f` is nonpositive under every +member of the null generated by the `g i` exactly when `f ≤ ∑ i, π i * g i` almost surely under +every member of the null, for some weights `π ≥ 0`. No integrability of `f` is assumed: the +integral of a function that is not integrable is `0`. -/ +theorem forall_integral_nonpos_iff_exists_ae_le (hg : ∀ i, Measurable (g i)) + (hf : Measurable f) : + (∀ μ ∈ constraintNull (range g), ∫ x, f x ∂μ ≤ 0) ↔ + ∃ π : ι → ℝ≥0, ∀ μ ∈ constraintNull (range g), f ≤ᵐ[μ] fun x ↦ ∑ i, (π i : ℝ) * g i x := by + refine ⟨fun h ↦ ?_, fun ⟨π, hπ⟩ μ hμ ↦ ?_⟩ + · obtain ⟨Y, -, hYμ, hY⟩ := exists_measurableSet_noArbitrageOn hg + obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_le_of_forall_integral_nonpos hg hY hf h + refine ⟨fun i ↦ (π i).toNNReal, fun μ hμ ↦ + Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ ?_⟩ + simpa only [Real.coe_toNNReal _ (hπK.1 _)] using hπ x hx + · by_cases hfi : Integrable f μ + · exact (integral_mono_ae hfi (integrable_sum_mul_of_mem_constraintNull hμ _) + (hπ μ hμ)).trans + (integral_sum_mul_nonpos_of_mem_constraintNull hμ fun i ↦ (π i).coe_nonneg) + · rw [integral_undef hfi] + +/-- **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. -/ +theorem IsEVar.exists_mem_constraintBets_ae_le (hg : ∀ i, Measurable (g i)) + (hE : IsEVar E (constraintNull (range g))) : + ∃ π ∈ 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) + +/-- **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 +are dominated by a bet `1 + ∑ i, π i * g i`, almost surely under every member of the null. -/ +theorem isEVar_constraintNull_iff (hg : ∀ i, Measurable (g i)) : + IsEVar 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_le hg⟩, fun ⟨hEm, _, hπ, hEπ⟩ ↦ + IsEVar.of_lintegral_le_one (fun _ ↦ isProbabilityMeasure_of_mem_constraintNull) hEm + fun μ hμ ↦ (lintegral_mono_ae (hEπ μ hμ)).trans + (lintegral_ofReal_one_add_le_one_of_mem_constraintBets hπ hμ)⟩ + +end ProbabilityTheory diff --git a/LMLExplore/MeasureTheory/Measure/Weighted.lean b/LMLExplore/MeasureTheory/Measure/Weighted.lean index 1adc0bac..ea3bc388 100644 --- a/LMLExplore/MeasureTheory/Measure/Weighted.lean +++ b/LMLExplore/MeasureTheory/Measure/Weighted.lean @@ -40,7 +40,9 @@ LMLPapers project. of `q` is contained in that of `p`; * `lintegral_weightedMeasure_eq_sum`, `integral_weightedMeasure_eq_sum`: integrals against `weightedMeasure p` are weighted sums; -* `measurable_weightedMeasure`: `p ↦ weightedMeasure p` is measurable. +* `measurable_weightedMeasure`: `p ↦ weightedMeasure p` is measurable; +* `integral_sum_smul_dirac`: the integral against a finite sum `∑ k, w k • δ_{x k}` of weighted + Dirac measures at points of any measurable space is the weighted sum `∑ k, w k • f (x k)`. -/ public section @@ -142,4 +144,17 @@ lemma measurable_weightedMeasure : Measurable (weightedMeasure (ι := ι)) := by exact Finset.measurable_sum _ fun i _ ↦ (ENNReal.measurable_ofReal.comp (measurable_pi_apply i)).mul measurable_const +/-- For nonnegative weights `w k` and points `x k` of a measurable space, the integral of a +strongly measurable function with values in a Banach space against `∑ k, w k • δ_{x k}` is the +weighted sum `∑ k, w k • f (x k)`. -/ +lemma integral_sum_smul_dirac {α 𝓧 E : Type*} [Fintype α] [MeasurableSpace 𝓧] + [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : 𝓧 → E} {x : α → 𝓧} + {w : α → ℝ} (hw : ∀ k, 0 ≤ w k) (hf : StronglyMeasurable f) : + ∫ y, f y ∂(∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k)) = ∑ k, w k • f (x k) := by + have hint : ∀ k ∈ Finset.univ, + Integrable f (ENNReal.ofReal (w k) • Measure.dirac (x k)) := fun k _ ↦ + (integrable_dirac' hf (by simp)).smul_measure ENNReal.ofReal_ne_top + rw [integral_finsetSum_measure hint] + simp_rw [integral_smul_measure, integral_dirac' _ _ hf, ENNReal.toReal_ofReal (hw _)] + end LMLExplore