From 056adf0c2be31b970441d10b5ebaee3bf520c31d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 09:19:23 +0100 Subject: [PATCH 1/5] feat: nulls generated by constraints, their bets, and the complete class theorem for finitely many constraints Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- LMLExplore/EValues/ConstraintNull/Basic.lean | 261 +++++++ .../EValues/ConstraintNull/CompleteClass.lean | 650 ++++++++++++++++++ 2 files changed, 911 insertions(+) create mode 100644 LMLExplore/EValues/ConstraintNull/Basic.lean create mode 100644 LMLExplore/EValues/ConstraintNull/CompleteClass.lean diff --git a/LMLExplore/EValues/ConstraintNull/Basic.lean b/LMLExplore/EValues/ConstraintNull/Basic.lean new file mode 100644 index 00000000..a46e78e8 --- /dev/null +++ b/LMLExplore/EValues/ConstraintNull/Basic.lean @@ -0,0 +1,261 @@ +/- +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 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]. 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. + +## 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.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`: 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] + +/-- The integral of a measurable function against a finitely supported measure with nonnegative +weights. -/ +private lemma integral_sum_smul_dirac {α : Type*} [Fintype α] {x : α → 𝓧} {w : α → ℝ} + (hw : ∀ k, 0 ≤ w k) (hf : Measurable 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.stronglyMeasurable (by simp)).smul_measure ENNReal.ofReal_ne_top + rw [integral_finsetSum_measure hint] + simp_rw [integral_smul_measure, integral_dirac' _ _ hf.stronglyMeasurable, + ENNReal.toReal_ofReal (hw _), smul_eq_mul] + +/-- 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)] + 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] 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 + +/-! ### Bets on finitely many constraints -/ + +variable [Fintype ι] {g : ι → 𝓧 → ℝ} {π π' : ι → ℝ≥0} + +/-- 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 ?_ + have : ∑ i, (π i : ℝ) * ∫ x, g i x ∂μ ≤ 0 := Finset.sum_nonpos fun i _ ↦ + mul_nonpos_of_nonneg_of_nonpos (π i).coe_nonneg + (integral_nonpos_of_mem_constraintNull hμ (mem_range_self i)) + linarith + +/-- 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..72a1581f --- /dev/null +++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean @@ -0,0 +1,650 @@ +/- +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 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. + +* *The support of 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`: the support of the null. +* `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 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 [nonredundantWeights, mem_ofPred_eq, mem_inter_iff, mem_iInter, 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 [nonredundantWeights, mem_ofPred_eq, 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`, the nonredundant weights that keep the combination of the functions +`a i` above `-c` at finitely many well chosen points of `Y` have a 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 + 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 := by + intro x hx + refine le_of_forall_pos_le_add fun ε hε ↦ ?_ + obtain ⟨n, hn⟩ := exists_nat_one_div_lt hε + 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 + obtain ⟨u, hu⟩ := hS.elim_finite_subfamily_closed t htc hdisj + refine ⟨u.image fun p ↦ (p.1 : 𝓧), ?_, (u.sup Prod.snd : ℕ) + 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 + 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] at hnot + obtain ⟨p, hp, hlt⟩ := hnot + have hx : (p.1 : 𝓧) ∈ u.image fun p ↦ (p.1 : 𝓧) := Finset.mem_image_of_mem _ hp + have hc' := hπc _ hx + have hle : (p.2 : ℝ) + 1 ≤ (u.sup Prod.snd : ℕ) + 1 := by + have : p.2 ≤ u.sup Prod.snd := Finset.le_sup (f := Prod.snd) hp + exact_mod_cast Nat.add_le_add_right this 1 + have hsum : ∑ i, s⁻¹ * π i * a i p.1 = s⁻¹ * ∑ i, π i * a i p.1 := by + rw [Finset.mul_sum] + exact Finset.sum_congr rfl fun i _ ↦ by ring + rw [hsum] at hlt + have h1 : 1 / ((u.sup Prod.snd : ℕ) + 1 : ℝ) ≤ 1 / ((p.2 : ℝ) + 1) := + one_div_le_one_div_of_le (by positivity) hle + have h2 : s⁻¹ * (-c) < -(1 / ((u.sup Prod.snd : ℕ) + 1 : ℝ)) := by + calc s⁻¹ * (-c) ≤ s⁻¹ * ∑ i, π i * a i p.1 := + mul_le_mul_of_nonneg_left hc' (inv_nonneg.2 hs.le) + _ < -(1 / ((p.2 : ℝ) + 1)) := hlt + _ ≤ _ := neg_le_neg h1 + have hN : (0 : ℝ) < (u.sup Prod.snd : ℕ) + 1 := by positivity + rw [inv_mul_eq_div, div_lt_iff₀ hs] at h2 + rw [neg_mul, neg_lt_neg_iff, one_div_mul_eq_div, div_lt_iff₀ hN] at h2 + linarith + +/-- If `v < A + t * B` for every `t ≥ 0`, then `B` is nonnegative. -/ +private lemma nonneg_of_forall_lt_add_mul {A B v : ℝ} (h : ∀ t : ℝ, 0 ≤ t → v < A + t * B) : + 0 ≤ B := by + by_contra! hB + have h1 := h _ (le_max_left 0 ((A - v) / -B)) + have h3 : max 0 ((A - v) / -B) * B ≤ (A - v) / -B * B := + mul_le_mul_of_nonpos_right (le_max_right _ _) hB.le + have h4 : (A - v) / -B * B = -(A - v) := by rw [div_neg, neg_mul, div_mul_cancel₀ _ hB.ne] + 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 + let φ : 𝓧 → (ι → ℝ) × ℝ := fun x ↦ (fun i ↦ a i x, f x) + let Q : Set ((ι → ℝ) × ℝ) := {p | (∀ i, p.1 i ≤ 0) ∧ δ ≤ p.2} + have hQ : Convex ℝ Q := by + rintro p ⟨hp1, hp2⟩ q ⟨hq1, hq2⟩ s t hs ht hst + refine ⟨fun i ↦ ?_, ?_⟩ + · simp only [Prod.fst_add, Prod.smul_fst, Pi.add_apply, Pi.smul_apply, smul_eq_mul] + nlinarith [hp1 i, hq1 i] + · simp only [Prod.snd_add, Prod.smul_snd, smul_eq_mul] + nlinarith + have hQc : IsClosed Q := by + have : Q = (⋂ i, {p : (ι → ℝ) × ℝ | p.1 i ≤ 0}) ∩ {p | δ ≤ p.2} := by + ext p + simp [Q] + rw [this] + exact (isClosed_iInter fun i ↦ isClosed_le (by fun_prop) continuous_const).inter + (isClosed_le continuous_const (by fun_prop)) + have hdisj : Disjoint (convexHull ℝ (φ '' F)) Q := 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 hsum1 : ∀ i, ∑ k, w k * a i (x k) ≤ 0 := by + intro i + have := hp1 i + simpa [← hxz, φ, Prod.fst_sum, Finset.sum_apply] using this + have key := hf α x w (fun k ↦ hF (hxF k)) (mem_simplex_iff.2 ⟨hw0, hw1⟩) hsum1 + have h2 : δ ≤ ∑ k, w k * f (x k) := by simpa [← hxz, φ, Prod.snd_sum] using hp2 + linarith + obtain ⟨ℓ, u, v, hℓP, huv, hℓQ⟩ := geometric_hahn_banach_compact_closed + (convex_convexHull ℝ _) ((F.finite_toSet.image φ).isCompact_convexHull ℝ) hQ hQc hdisj + set β := ℓ (0, 1) with hβ_def + set π : ι → ℝ := fun i ↦ -ℓ ((fun j ↦ if i = j then 1 else 0), 0) with hπ_def + have hℓ : ∀ p : (ι → ℝ) × ℝ, ℓ p = -∑ i, π i * p.1 i + β * p.2 := by + intro p + have h1 : ℓ p = ℓ (p.1, 0) + p.2 * β := by + conv_lhs => rw [show p = (p.1, 0) + p.2 • ((0 : ι → ℝ), (1 : ℝ)) by ext <;> simp] + rw [map_add, map_smul, smul_eq_mul] + have h2 := LinearMap.pi_apply_eq_sum_univ + ((ℓ : (ι → ℝ) × ℝ →ₗ[ℝ] ℝ) ∘ₗ LinearMap.inl ℝ (ι → ℝ) ℝ) p.1 + simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.inl_apply, + ContinuousLinearMap.coe_coe, smul_eq_mul] at h2 + rw [h1, h2] + simp only [π, neg_mul, Finset.sum_neg_distrib, neg_neg, mul_comm (p.1 _)] + ring + have hβ : 0 ≤ β := by + refine nonneg_of_forall_lt_add_mul (A := β * δ) (v := v) fun t ht ↦ ?_ + have := hℓQ (0, δ + t) ⟨fun i ↦ le_rfl, by linarith⟩ + 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, δ) + ⟨fun j ↦ by simp only; split_ifs <;> linarith, le_rfl⟩ + rw [hℓ] at this + simpa [mul_ite, Finset.sum_ite_eq, mul_comm, add_comm] using this + have hx : ∀ x ∈ F, -∑ i, π i * a i x + β * f x < u := by + intro x hx + have := hℓP (φ x) (subset_convexHull ℝ _ (mem_image_of_mem φ hx)) + rwa [hℓ] at this + have hv : v < β * δ := by + have := hℓQ (0, δ) ⟨fun i ↦ le_rfl, le_rfl⟩ + simpa [hℓ] using this + rcases hβ.eq_or_lt with hβ0 | hβ0 + · -- the separating functional is vertical: the combination is positive on `F` + 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, add_zero] 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) + have h5 : ∑ i, (M • π) i * a i x = M * ∑ i, π i * a i x := by + rw [Finset.mul_sum] + exact Finset.sum_congr rfl fun i _ ↦ by simp [mul_assoc] + rw [h5] + linarith + · refine ⟨β⁻¹ • π, fun i ↦ by simpa using mul_nonneg (inv_nonneg.2 hβ) (hπ i), + fun x hxF ↦ ?_⟩ + have h1 := hx x hxF + have h5 : ∑ i, (β⁻¹ • π) i * a i x = β⁻¹ * ∑ i, π i * a i x := by + rw [Finset.mul_sum] + exact Finset.sum_congr rfl fun i _ ↦ by simp [mul_assoc] + rw [h5] + have h6 : β * (f x - δ) < ∑ i, π i * a i x := by nlinarith + have h7 : f x - δ < β⁻¹ * ∑ i, π i * a i x := by + rw [lt_inv_mul_iff₀ hβ0] + exact h6 + 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 `π`. The +proof combines the finite step, up to `δ`, with the compactness of the 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 + 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 + 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 : 1 / ((N : ℝ) + 1) ≤ 1 / ((p.2 : ℝ) + 1) := + one_div_le_one_div_of_le (by positivity) + (by exact_mod_cast Nat.add_le_add_right (Finset.le_sup (f := Prod.snd) hp) 1) + simp only [t, mem_ofPred_eq] + rw [hπ'eq p.1 p.1.2] + linarith + refine ⟨π, hπK, fun x hx ↦ le_of_forall_pos_le_add fun ε hε ↦ ?_⟩ + obtain ⟨n, hn⟩ := exists_nat_one_div_lt hε + 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. The proof applies the complete class +theorem to multiples of the indicator of the point. -/ +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 + 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] + 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] + 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 + +/-! ### The support of the null -/ + +variable [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {f : 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞} + +/-- A property that holds on a set carrying a measure holds almost everywhere. -/ +private lemma ae_of_forall_mem {ν : Measure 𝓧} (hν : ν Yᶜ = 0) {p : 𝓧 → Prop} + (hp : ∀ x ∈ Y, p x) : ∀ᵐ x ∂ν, p x := + Filter.mem_of_superset (mem_ae_iff.2 hν) hp + +/-- The support of a null generated by finitely many measurable constraints: a measurable set +that carries every member of the null and 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, 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 hgi : ∀ i, Integrable (fun x ↦ ρ i * g i x) μ := fun i ↦ + (integrable_of_mem_constraintNull hμ (mem_range_self i)).const_mul (ρ i) + have hint : Integrable (fun x ↦ ∑ i, ρ i * g i x) μ := integrable_finsetSum _ fun i _ ↦ hgi i + have hnn : 0 ≤ᵐ[μ] fun x ↦ ∑ i, ρ i * g i x := ae_of_forall_mem (hμY μ hμ) hρY + have hle : ∫ x, ∑ i, ρ i * g i x ∂μ ≤ 0 := by + rw [integral_finsetSum _ fun i _ ↦ hgi i] + refine Finset.sum_nonpos fun i _ ↦ ?_ + rw [integral_const_mul] + exact mul_nonpos_of_nonneg_of_nonpos (hρ0 i) + (integral_nonpos_of_mem_constraintNull hμ (mem_range_self i)) + have h0 := (integral_eq_zero_iff_of_nonneg_ae hnn hint).1 + (le_antisymm hle (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μ ↦ ae_of_forall_mem (hYμ μ hμ) fun x hx ↦ ?_⟩ + simpa only [Real.coe_toNNReal _ (hπK.1 _)] using hπ x hx + · have hgi : ∀ i, Integrable (fun x ↦ (π i : ℝ) * g i x) μ := fun i ↦ + (integrable_of_mem_constraintNull hμ (mem_range_self i)).const_mul _ + by_cases hfi : Integrable f μ + · refine (integral_mono_ae hfi (integrable_finsetSum _ fun i _ ↦ hgi i) (hπ μ hμ)).trans ?_ + rw [integral_finsetSum _ fun i _ ↦ hgi i] + refine Finset.sum_nonpos fun i _ ↦ ?_ + rw [integral_const_mul] + exact mul_nonpos_of_nonneg_of_nonpos (π i).coe_nonneg + (integral_nonpos_of_mem_constraintNull hμ (mem_range_self i)) + · 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μ ↦ + ae_of_forall_mem (hYμ μ hμ) fun x hx ↦ ENNReal.toReal_nonneg.trans (hπY x hx), fun μ hμ ↦ + ae_of_forall_mem (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 From 7e3a49d84568cb9f4f63f1f190a3d9709ca0b853 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 10:27:53 +0100 Subject: [PATCH 2/5] refactor: factor out the general helpers of the constraint-null complete class Make the general helpers public in general files (`integral_sum_smul_dirac` in `MeasureTheory/Measure/Weighted`, `nonneg_of_forall_lt_add_mul` in `Algebra/Order/Field/Basic`, the new `le_of_forall_nat_le_add_one_div` in `Algebra/Order/Archimedean/Basic`), add `noArbitrageOn_iff` and the constraint-null lemmas on nonnegative combinations of the constraints, reuse `LinearMap.prod_pi_apply_eq_sum_univ` and `Nat.one_div_le_one_div`, comment the long proofs and drop proof descriptions from theorem docstrings. Co-Authored-By: Claude Code --- .../Algebra/Order/Archimedean/Basic.lean | 31 +++ LMLExplore/Algebra/Order/Field/Basic.lean | 18 +- LMLExplore/EValues/ConstraintNull/Basic.lean | 54 ++-- .../EValues/ConstraintNull/CompleteClass.lean | 232 +++++++----------- .../MeasureTheory/Measure/Weighted.lean | 17 +- 5 files changed, 186 insertions(+), 166 deletions(-) create mode 100644 LMLExplore/Algebra/Order/Archimedean/Basic.lean diff --git a/LMLExplore/Algebra/Order/Archimedean/Basic.lean b/LMLExplore/Algebra/Order/Archimedean/Basic.lean new file mode 100644 index 00000000..47438f74 --- /dev/null +++ b/LMLExplore/Algebra/Order/Archimedean/Basic.lean @@ -0,0 +1,31 @@ +/- +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 fields + +In an 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*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean 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..19a26f71 100644 --- a/LMLExplore/Algebra/Order/Field/Basic.lean +++ b/LMLExplore/Algebra/Order/Field/Basic.lean @@ -8,15 +8,17 @@ module public import Mathlib.Algebra.Order.Field.Basic /-! -# 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 +34,15 @@ 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 h1 := h _ (le_max_left 0 ((A - v) / -B)) + have h3 : max 0 ((A - v) / -B) * B ≤ (A - v) / -B * B := + mul_le_mul_of_nonpos_right (le_max_right _ _) hB.le + have h4 : (A - v) / -B * B = -(A - v) := by rw [div_neg, neg_mul, div_mul_cancel₀ _ hB.ne] + have h5 := h1.trans_le ((add_le_add_iff_left A).2 h3) + rw [h4, neg_sub, add_sub_cancel] at h5 + exact lt_irrefl v h5 diff --git a/LMLExplore/EValues/ConstraintNull/Basic.lean b/LMLExplore/EValues/ConstraintNull/Basic.lean index a46e78e8..3db82617 100644 --- a/LMLExplore/EValues/ConstraintNull/Basic.lean +++ b/LMLExplore/EValues/ConstraintNull/Basic.lean @@ -6,6 +6,7 @@ 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 @@ -43,6 +44,10 @@ these dominate every e-variable. * `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`, @@ -120,18 +125,6 @@ theorem mem_constraintNull_range_iff {g : ι → 𝓧 → ℝ} : IsProbabilityMeasure μ ∧ ∀ i, Integrable (g i) μ ∧ ∫ x, g i x ∂μ ≤ 0 := by simp [mem_constraintNull_iff] -/-- The integral of a measurable function against a finitely supported measure with nonnegative -weights. -/ -private lemma integral_sum_smul_dirac {α : Type*} [Fintype α] {x : α → 𝓧} {w : α → ℝ} - (hw : ∀ k, 0 ≤ w k) (hf : Measurable 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.stronglyMeasurable (by simp)).smul_measure ENNReal.ofReal_ne_top - rw [integral_finsetSum_measure hint] - simp_rw [integral_smul_measure, integral_dirac' _ _ hf.stronglyMeasurable, - ENNReal.toReal_ofReal (hw _), smul_eq_mul] - /-- 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. -/ @@ -148,7 +141,8 @@ theorem sum_smul_dirac_mem_constraintNull_iff (hΦ : ∀ f ∈ Φ, Measurable f) 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)] + 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 @@ -168,7 +162,7 @@ theorem sum_mul_nonpos_of_forall_integral_nonpos (hΦ : ∀ f ∈ Φ, Measurable ∑ 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] using h _ hμ + 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. -/ @@ -183,10 +177,35 @@ theorem sum_ofReal_mul_le_one_of_isEVar (hΦ : ∀ f ∈ Φ, Measurable f) rw [measure_univ, lintegral_finsetSum_measure] at h1 simpa [lintegral_smul_measure, lintegral_dirac' _ hE.measurable] using h1 -/-! ### Bets on finitely many constraints -/ +/-! ### 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`. -/ @@ -246,10 +265,7 @@ theorem lintegral_ofReal_one_add_le_one_of_mem_constraintBets (hπ : π ∈ cons ∫⁻ 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 ?_ - have : ∑ i, (π i : ℝ) * ∫ x, g i x ∂μ ≤ 0 := Finset.sum_nonpos fun i _ ↦ - mul_nonpos_of_nonneg_of_nonpos (π i).coe_nonneg - (integral_nonpos_of_mem_constraintNull hμ (mem_range_self i)) - linarith + 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)) diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean index 72a1581f..bba598cd 100644 --- a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean +++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean @@ -6,6 +6,9 @@ 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 @@ -90,6 +93,11 @@ 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`. -/ @@ -109,7 +117,7 @@ theorem isClosed_nonredundantWeights : IsClosed (nonredundantWeights a Y) := by ⋂ (ρ : ι → ℝ) (_ : (∀ i, 0 ≤ ρ i) ∧ (∀ x ∈ Y, ∑ i, ρ i * a i x = 0) ∧ ρ ≠ 0), ⋃ i ∈ {i | ρ i ≠ 0}, {π | π i = 0} := by ext π - simp only [nonredundantWeights, mem_ofPred_eq, mem_inter_iff, mem_iInter, mem_iUnion, + 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 @@ -144,7 +152,7 @@ theorem exists_mem_nonredundantWeights_sum_mul_eq {π : ι → ℝ} (hπ : ∀ i | _ n ih => by_cases hK : π ∈ nonredundantWeights a Y · exact ⟨π, hK, fun _ _ ↦ rfl⟩ - simp only [nonredundantWeights, mem_ofPred_eq, hπ, implies_true, true_and, not_forall] at hK + 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 @@ -195,13 +203,16 @@ theorem isCompact_nonredundantWeights_inter {T : Set (ι → ℝ)} (hT : IsClose 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`, the nonredundant weights that keep the combination of the functions -`a i` above `-c` at finitely many well chosen points of `Y` have a total mass at most `R * c` -[LRR26, proof of Lemma 7.2]. -/ +/-- 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 @@ -211,17 +222,17 @@ theorem exists_finset_sum_le_of_noArbitrageOn (h : NoArbitrageOn a Y) : 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 := by - intro x hx - refine le_of_forall_pos_le_add fun ε hε ↦ ?_ - obtain ⟨n, hn⟩ := exists_nat_one_div_lt hε - have := hρt (⟨x, hx⟩, n) - simp only at this - linarith + 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 - refine ⟨u.image fun p ↦ (p.1 : 𝓧), ?_, (u.sup Prod.snd : ℕ) + 1, by positivity, ?_⟩ + 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 @@ -231,6 +242,7 @@ theorem exists_finset_sum_le_of_noArbitrageOn (h : NoArbitrageOn a Y) : 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), ?_⟩ @@ -238,37 +250,14 @@ theorem exists_finset_sum_le_of_noArbitrageOn (h : NoArbitrageOn a Y) : 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] at hnot + smul_eq_mul, mul_assoc, ← Finset.mul_sum] at hnot obtain ⟨p, hp, hlt⟩ := hnot - have hx : (p.1 : 𝓧) ∈ u.image fun p ↦ (p.1 : 𝓧) := Finset.mem_image_of_mem _ hp - have hc' := hπc _ hx - have hle : (p.2 : ℝ) + 1 ≤ (u.sup Prod.snd : ℕ) + 1 := by - have : p.2 ≤ u.sup Prod.snd := Finset.le_sup (f := Prod.snd) hp - exact_mod_cast Nat.add_le_add_right this 1 - have hsum : ∑ i, s⁻¹ * π i * a i p.1 = s⁻¹ * ∑ i, π i * a i p.1 := by - rw [Finset.mul_sum] - exact Finset.sum_congr rfl fun i _ ↦ by ring - rw [hsum] at hlt - have h1 : 1 / ((u.sup Prod.snd : ℕ) + 1 : ℝ) ≤ 1 / ((p.2 : ℝ) + 1) := - one_div_le_one_div_of_le (by positivity) hle - have h2 : s⁻¹ * (-c) < -(1 / ((u.sup Prod.snd : ℕ) + 1 : ℝ)) := by - calc s⁻¹ * (-c) ≤ s⁻¹ * ∑ i, π i * a i p.1 := - mul_le_mul_of_nonneg_left hc' (inv_nonneg.2 hs.le) - _ < -(1 / ((p.2 : ℝ) + 1)) := hlt - _ ≤ _ := neg_le_neg h1 - have hN : (0 : ℝ) < (u.sup Prod.snd : ℕ) + 1 := by positivity - rw [inv_mul_eq_div, div_lt_iff₀ hs] at h2 - rw [neg_mul, neg_lt_neg_iff, one_div_mul_eq_div, div_lt_iff₀ hN] at h2 - linarith - -/-- If `v < A + t * B` for every `t ≥ 0`, then `B` is nonnegative. -/ -private lemma nonneg_of_forall_lt_add_mul {A B v : ℝ} (h : ∀ t : ℝ, 0 ≤ t → v < A + t * B) : - 0 ≤ B := by - by_contra! hB - have h1 := h _ (le_max_left 0 ((A - v) / -B)) - have h3 : max 0 ((A - v) / -B) * B ≤ (A - v) / -B * B := - mul_le_mul_of_nonpos_right (le_max_right _ _) hB.le - have h4 : (A - v) / -B * B = -(A - v) := by rw [div_neg, neg_mul, div_mul_cancel₀ _ hB.ne] + -- 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 @@ -281,108 +270,78 @@ private lemma exists_le_add_sum_mul_of_finset {f : 𝓧 → ℝ} {F : Finset 𝓧} (hF : ↑F ⊆ Y) {δ : ℝ} (hδ : 0 < δ) : ∃ π : ι → ℝ, (∀ i, 0 ≤ π i) ∧ ∀ x ∈ F, f x ≤ δ + ∑ i, π i * a i x := by classical - let φ : 𝓧 → (ι → ℝ) × ℝ := fun x ↦ (fun i ↦ a i x, f x) - let Q : Set ((ι → ℝ) × ℝ) := {p | (∀ i, p.1 i ≤ 0) ∧ δ ≤ p.2} - have hQ : Convex ℝ Q := by - rintro p ⟨hp1, hp2⟩ q ⟨hq1, hq2⟩ s t hs ht hst - refine ⟨fun i ↦ ?_, ?_⟩ - · simp only [Prod.fst_add, Prod.smul_fst, Pi.add_apply, Pi.smul_apply, smul_eq_mul] - nlinarith [hp1 i, hq1 i] - · simp only [Prod.snd_add, Prod.smul_snd, smul_eq_mul] - nlinarith - have hQc : IsClosed Q := by - have : Q = (⋂ i, {p : (ι → ℝ) × ℝ | p.1 i ≤ 0}) ∩ {p | δ ≤ p.2} := by - ext p - simp [Q] - rw [this] - exact (isClosed_iInter fun i ↦ isClosed_le (by fun_prop) continuous_const).inter - (isClosed_le continuous_const (by fun_prop)) - have hdisj : Disjoint (convexHull ℝ (φ '' F)) Q := by + -- 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 hsum1 : ∀ i, ∑ k, w k * a i (x k) ≤ 0 := by - intro i - have := hp1 i - simpa [← hxz, φ, Prod.fst_sum, Finset.sum_apply] using this - have key := hf α x w (fun k ↦ hF (hxF k)) (mem_simplex_iff.2 ⟨hw0, hw1⟩) hsum1 - have h2 : δ ≤ ∑ k, w k * f (x k) := by simpa [← hxz, φ, Prod.snd_sum] using hp2 + 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 ℝ) hQ hQc hdisj - set β := ℓ (0, 1) with hβ_def - set π : ι → ℝ := fun i ↦ -ℓ ((fun j ↦ if i = j then 1 else 0), 0) with hπ_def - have hℓ : ∀ p : (ι → ℝ) × ℝ, ℓ p = -∑ i, π i * p.1 i + β * p.2 := by - intro p - have h1 : ℓ p = ℓ (p.1, 0) + p.2 * β := by - conv_lhs => rw [show p = (p.1, 0) + p.2 • ((0 : ι → ℝ), (1 : ℝ)) by ext <;> simp] - rw [map_add, map_smul, smul_eq_mul] - have h2 := LinearMap.pi_apply_eq_sum_univ - ((ℓ : (ι → ℝ) × ℝ →ₗ[ℝ] ℝ) ∘ₗ LinearMap.inl ℝ (ι → ℝ) ℝ) p.1 - simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.inl_apply, - ContinuousLinearMap.coe_coe, smul_eq_mul] at h2 - rw [h1, h2] - simp only [π, neg_mul, Finset.sum_neg_distrib, neg_neg, mul_comm (p.1 _)] - ring + (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 (0, δ + t) ⟨fun i ↦ le_rfl, by linarith⟩ + 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, δ) - ⟨fun j ↦ by simp only; split_ifs <;> linarith, le_rfl⟩ + 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, add_comm] using this - have hx : ∀ x ∈ F, -∑ i, π i * a i x + β * f x < u := by - intro x hx - have := hℓP (φ x) (subset_convexHull ℝ _ (mem_image_of_mem φ hx)) - rwa [hℓ] at this - have hv : v < β * δ := by - have := hℓQ (0, δ) ⟨fun i ↦ le_rfl, le_rfl⟩ - simpa [hℓ] using 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` + · -- 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, add_zero] at h1 + 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) - have h5 : ∑ i, (M • π) i * a i x = M * ∑ i, π i * a i x := by - rw [Finset.mul_sum] - exact Finset.sum_congr rfl fun i _ ↦ by simp [mul_assoc] - rw [h5] + simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, ← Finset.mul_sum] linarith - · refine ⟨β⁻¹ • π, fun i ↦ by simpa using mul_nonneg (inv_nonneg.2 hβ) (hπ i), + · -- 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 - have h5 : ∑ i, (β⁻¹ • π) i * a i x = β⁻¹ * ∑ i, π i * a i x := by - rw [Finset.mul_sum] - exact Finset.sum_congr rfl fun i _ ↦ by simp [mul_assoc] - rw [h5] - have h6 : β * (f x - δ) < ∑ i, π i * a i x := by nlinarith - have h7 : f x - δ < β⁻¹ * ∑ i, π i * a i x := by + 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] - exact h6 + 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 `π`. The -proof combines the finite step, up to `δ`, with the compactness of the nonredundant weights. -/ +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 _) @@ -394,6 +353,8 @@ theorem exists_mem_nonredundantWeights_le_of_noArbitrageOn (h : NoArbitrageOn a 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) @@ -423,21 +384,18 @@ theorem exists_mem_nonredundantWeights_le_of_noArbitrageOn (h : NoArbitrageOn a · simp only [mem_iInter] intro p hp have h1 := hπ p.1 (Finset.mem_union_right _ (Finset.mem_image_of_mem _ hp)) - have h2 : 1 / ((N : ℝ) + 1) ≤ 1 / ((p.2 : ℝ) + 1) := - one_div_le_one_div_of_le (by positivity) - (by exact_mod_cast Nat.add_le_add_right (Finset.le_sup (f := Prod.snd) hp) 1) + 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_pos_le_add fun ε hε ↦ ?_⟩ - obtain ⟨n, hn⟩ := exists_nat_one_div_lt hε + 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. The proof applies the complete class -theorem to multiples of the indicator of the point. -/ +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 α ∧ @@ -484,11 +442,6 @@ theorem exists_charging_family_of_noArbitrageOn (h : NoArbitrageOn a Y) {x₀ : variable [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {f : 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞} -/-- A property that holds on a set carrying a measure holds almost everywhere. -/ -private lemma ae_of_forall_mem {ν : Measure 𝓧} (hν : ν Yᶜ = 0) {p : 𝓧 → Prop} - (hp : ∀ x ∈ Y, p x) : ∀ᵐ x ∂ν, p x := - Filter.mem_of_superset (mem_ae_iff.2 hν) hp - /-- The support of a null generated by finitely many measurable constraints: a measurable set that carries every member of the null and on which the constraints admit no arbitrage. -/ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) : @@ -507,7 +460,7 @@ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) : intro Y hY hμY hn by_cases hT : NoArbitrageOn g Y · exact ⟨Y, hY, hμY, hT⟩ - simp only [NoArbitrageOn, not_forall] at 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) @@ -520,18 +473,12 @@ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) : -- 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 hgi : ∀ i, Integrable (fun x ↦ ρ i * g i x) μ := fun i ↦ - (integrable_of_mem_constraintNull hμ (mem_range_self i)).const_mul (ρ i) - have hint : Integrable (fun x ↦ ∑ i, ρ i * g i x) μ := integrable_finsetSum _ fun i _ ↦ hgi i - have hnn : 0 ≤ᵐ[μ] fun x ↦ ∑ i, ρ i * g i x := ae_of_forall_mem (hμY μ hμ) hρY - have hle : ∫ x, ∑ i, ρ i * g i x ∂μ ≤ 0 := by - rw [integral_finsetSum _ fun i _ ↦ hgi i] - refine Finset.sum_nonpos fun i _ ↦ ?_ - rw [integral_const_mul] - exact mul_nonpos_of_nonneg_of_nonpos (hρ0 i) - (integral_nonpos_of_mem_constraintNull hμ (mem_range_self i)) + 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 hle (integral_nonneg_of_ae hnn)) + (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 @@ -606,17 +553,13 @@ theorem forall_integral_nonpos_iff_exists_ae_le (hg : ∀ i, Measurable (g i)) 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μ ↦ ae_of_forall_mem (hYμ μ hμ) fun x hx ↦ ?_⟩ + 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 - · have hgi : ∀ i, Integrable (fun x ↦ (π i : ℝ) * g i x) μ := fun i ↦ - (integrable_of_mem_constraintNull hμ (mem_range_self i)).const_mul _ - by_cases hfi : Integrable f μ - · refine (integral_mono_ae hfi (integrable_finsetSum _ fun i _ ↦ hgi i) (hπ μ hμ)).trans ?_ - rw [integral_finsetSum _ fun i _ ↦ hgi i] - refine Finset.sum_nonpos fun i _ ↦ ?_ - rw [integral_const_mul] - exact mul_nonpos_of_nonneg_of_nonpos (π i).coe_nonneg - (integral_nonpos_of_mem_constraintNull hμ (mem_range_self i)) + · 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 @@ -631,8 +574,9 @@ theorem IsEVar.exists_mem_constraintBets_ae_le (hg : ∀ i, Measurable (g i)) 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μ ↦ - ae_of_forall_mem (hYμ μ hμ) fun x hx ↦ ENNReal.toReal_nonneg.trans (hπY x hx), fun μ hμ ↦ - ae_of_forall_mem (hYμ μ hμ) fun x hx ↦ ?_⟩ + 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) 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 From 72b7c52a0ce92d400e8fb50f20a3c6f62a6f1425 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 10:48:24 +0100 Subject: [PATCH 3/5] refactor: tighten the constraint-null docstrings and proofs Describe the set built by `exists_measurableSet_noArbitrageOn` as a set carrying the null rather than its support, and state the measurability and almost-sure conditions of the bet results in the `Basic.lean` module docstring. Simplify `nonneg_of_forall_lt_add_mul`, comment the structure of `exists_charging_family_of_noArbitrageOn`, and factor the repeated almost-everywhere step into `ae_of_forall_mem_of_measure_compl_eq_zero`. Co-Authored-By: Claude Code --- LMLExplore/Algebra/Order/Field/Basic.lean | 14 ++++---- LMLExplore/EValues/ConstraintNull/Basic.lean | 11 +++--- .../EValues/ConstraintNull/CompleteClass.lean | 24 ++++++++----- LMLExplore/MeasureTheory/OuterMeasure/AE.lean | 35 +++++++++++++++++++ 4 files changed, 63 insertions(+), 21 deletions(-) create mode 100644 LMLExplore/MeasureTheory/OuterMeasure/AE.lean diff --git a/LMLExplore/Algebra/Order/Field/Basic.lean b/LMLExplore/Algebra/Order/Field/Basic.lean index 19a26f71..dab3f138 100644 --- a/LMLExplore/Algebra/Order/Field/Basic.lean +++ b/LMLExplore/Algebra/Order/Field/Basic.lean @@ -6,6 +6,8 @@ Authors: LMLExplore contributors module public import Mathlib.Algebra.Order.Field.Basic +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith /-! # Bounds in linearly ordered fields @@ -39,10 +41,8 @@ theorem mul_div_add_le_right (hx : 0 ≤ x) (hy : 0 ≤ y) : x * y / (x + y) ≤ 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 h1 := h _ (le_max_left 0 ((A - v) / -B)) - have h3 : max 0 ((A - v) / -B) * B ≤ (A - v) / -B * B := - mul_le_mul_of_nonpos_right (le_max_right _ _) hB.le - have h4 : (A - v) / -B * B = -(A - v) := by rw [div_neg, neg_mul, div_mul_cancel₀ _ hB.ne] - have h5 := h1.trans_le ((add_le_add_iff_left A).2 h3) - rw [h4, neg_sub, add_sub_cancel] at h5 - exact lt_irrefl v h5 + 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 index 3db82617..c60f0231 100644 --- a/LMLExplore/EValues/ConstraintNull/Basic.lean +++ b/LMLExplore/EValues/ConstraintNull/Basic.lean @@ -23,9 +23,10 @@ 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]. 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. +[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 @@ -53,8 +54,8 @@ these dominate every e-variable. * `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`: a bet is an e-variable for the - null. +* `ProbabilityTheory.isEVar_ofReal_one_add_of_mem_constraintBets`: for measurable constraints, a + bet is an e-variable for the null. ## References diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean index bba598cd..b5bb8c00 100644 --- a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean +++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean @@ -9,6 +9,7 @@ public import LMLExplore.EValues.ConstraintNull.Basic import LMLExplore.Algebra.Order.Archimedean.Basic import LMLExplore.Algebra.Order.Field.Basic import LMLExplore.LinearAlgebra.Pi +import LMLExplore.MeasureTheory.OuterMeasure.AE import Mathlib.Analysis.Convex.Combination import Mathlib.Analysis.Convex.Topology import Mathlib.Analysis.LocallyConvex.Separation @@ -28,7 +29,7 @@ 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. -* *The support of the null.* Removing, finitely many times, the set where a nonnegative +* *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 @@ -61,7 +62,8 @@ supported member of the null, so that e-variables are finite on `Y`. 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`: the support of the null. +* `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** @@ -402,6 +404,8 @@ theorem exists_charging_family_of_noArbitrageOn (h : NoArbitrageOn a Y) {x₀ : (∀ 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 @@ -421,11 +425,13 @@ theorem exists_charging_family_of_noArbitrageOn (h : NoArbitrageOn a Y) {x₀ : 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 @@ -438,12 +444,12 @@ theorem exists_charging_family_of_noArbitrageOn (h : NoArbitrageOn a Y) {x₀ : (by simpa using hsum)) (abs_nonneg _) linarith -/-! ### The support of the null -/ +/-! ### A set carrying the null -/ variable [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {f : 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞} -/-- The support of a null generated by finitely many measurable constraints: a measurable set -that carries every member of the null and on which the constraints admit no arbitrage. -/ +/-- 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 @@ -475,7 +481,7 @@ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) : 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 + ae_of_forall_mem_of_measure_compl_eq_zero (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)) @@ -554,7 +560,7 @@ theorem forall_integral_nonpos_iff_exists_ae_le (hg : ∀ i, Measurable (g i)) · 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 ↦ ?_⟩ + ae_of_forall_mem_of_measure_compl_eq_zero (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μ _) @@ -574,9 +580,9 @@ theorem IsEVar.exists_mem_constraintBets_ae_le (hg : ∀ i, Measurable (g i)) 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 ↦ + ae_of_forall_mem_of_measure_compl_eq_zero (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 ↦ ?_⟩ + ae_of_forall_mem_of_measure_compl_eq_zero (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) diff --git a/LMLExplore/MeasureTheory/OuterMeasure/AE.lean b/LMLExplore/MeasureTheory/OuterMeasure/AE.lean new file mode 100644 index 00000000..85a8524d --- /dev/null +++ b/LMLExplore/MeasureTheory/OuterMeasure/AE.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.MeasureTheory.OuterMeasure.AE + +/-! +# Almost everywhere properties from a set of full measure + +A property that holds at every point of a set whose complement is null holds almost everywhere. +This is `Filter.eventually_of_mem` for the filter `MeasureTheory.ae μ`, stated with the measure of +the complement, the form in which sets of full measure usually arise. + +## Main statements + +* `MeasureTheory.ae_of_forall_mem_of_measure_compl_eq_zero`: if `μ sᶜ = 0` and `p` holds on `s`, + then `p` holds `μ`-almost everywhere. +-/ + +public section + +namespace MeasureTheory + +variable {α F : Type*} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : Set α} + {p : α → Prop} + +/-- A property that holds on a set whose complement is null holds almost everywhere. -/ +theorem ae_of_forall_mem_of_measure_compl_eq_zero (hs : μ sᶜ = 0) (hp : ∀ x ∈ s, p x) : + ∀ᵐ x ∂μ, p x := + Filter.eventually_of_mem (mem_ae_iff.2 hs) hp + +end MeasureTheory From 3fb4f1c6310cf408b927f23c050436c9edd7137b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 11:12:12 +0100 Subject: [PATCH 4/5] refactor: state le_of_forall_nat_le_add_one_div for Archimedean semifields Co-Authored-By: Claude Code --- LMLExplore/Algebra/Order/Archimedean/Basic.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/LMLExplore/Algebra/Order/Archimedean/Basic.lean b/LMLExplore/Algebra/Order/Archimedean/Basic.lean index 47438f74..f2ac98f6 100644 --- a/LMLExplore/Algebra/Order/Archimedean/Basic.lean +++ b/LMLExplore/Algebra/Order/Archimedean/Basic.lean @@ -8,10 +8,11 @@ module public import Mathlib.Algebra.Order.Archimedean.Basic /-! -# Inequalities up to `1 / (n + 1)` in Archimedean fields +# Inequalities up to `1 / (n + 1)` in Archimedean semifields -In an 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 +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. @@ -22,7 +23,8 @@ sets. public section -variable {K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {a b : K} +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 := From 62392686d799f3cc50162fe87d2d1dc1ed5fab29 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 11:39:00 +0100 Subject: [PATCH 5/5] refactor: inline ae_of_forall_mem_of_measure_compl_eq_zero at its call sites Delete LMLExplore/MeasureTheory/OuterMeasure/AE.lean, whose only lemma was a thin wrapper around Filter.eventually_of_mem (mem_ae_iff.2 _), and write that term directly in the complete class proofs. Co-Authored-By: Claude Code --- .../EValues/ConstraintNull/CompleteClass.lean | 9 +++-- LMLExplore/MeasureTheory/OuterMeasure/AE.lean | 35 ------------------- 2 files changed, 4 insertions(+), 40 deletions(-) delete mode 100644 LMLExplore/MeasureTheory/OuterMeasure/AE.lean diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean index b5bb8c00..cc72149e 100644 --- a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean +++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean @@ -9,7 +9,6 @@ public import LMLExplore.EValues.ConstraintNull.Basic import LMLExplore.Algebra.Order.Archimedean.Basic import LMLExplore.Algebra.Order.Field.Basic import LMLExplore.LinearAlgebra.Pi -import LMLExplore.MeasureTheory.OuterMeasure.AE import Mathlib.Analysis.Convex.Combination import Mathlib.Analysis.Convex.Topology import Mathlib.Analysis.LocallyConvex.Separation @@ -481,7 +480,7 @@ theorem exists_measurableSet_noArbitrageOn (hg : ∀ i, Measurable (g i)) : intro μ hμ have hint := integrable_sum_mul_of_mem_constraintNull hμ ρ have hnn : 0 ≤ᵐ[μ] fun x ↦ ∑ i, ρ i * g i x := - ae_of_forall_mem_of_measure_compl_eq_zero (hμY μ hμ) hρY + 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)) @@ -560,7 +559,7 @@ theorem forall_integral_nonpos_iff_exists_ae_le (hg : ∀ i, Measurable (g i)) · 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μ ↦ - ae_of_forall_mem_of_measure_compl_eq_zero (hYμ μ hμ) fun x hx ↦ ?_⟩ + 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μ _) @@ -580,9 +579,9 @@ theorem IsEVar.exists_mem_constraintBets_ae_le (hg : ∀ i, Measurable (g i)) 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μ ↦ - ae_of_forall_mem_of_measure_compl_eq_zero (hYμ μ hμ) fun x hx ↦ + Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ ENNReal.toReal_nonneg.trans (hπY x hx), fun μ hμ ↦ - ae_of_forall_mem_of_measure_compl_eq_zero (hYμ μ hμ) fun x hx ↦ ?_⟩ + 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) diff --git a/LMLExplore/MeasureTheory/OuterMeasure/AE.lean b/LMLExplore/MeasureTheory/OuterMeasure/AE.lean deleted file mode 100644 index 85a8524d..00000000 --- a/LMLExplore/MeasureTheory/OuterMeasure/AE.lean +++ /dev/null @@ -1,35 +0,0 @@ -/- -Copyright (c) 2026 LMLExplore contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: LMLExplore contributors --/ -module - -public import Mathlib.MeasureTheory.OuterMeasure.AE - -/-! -# Almost everywhere properties from a set of full measure - -A property that holds at every point of a set whose complement is null holds almost everywhere. -This is `Filter.eventually_of_mem` for the filter `MeasureTheory.ae μ`, stated with the measure of -the complement, the form in which sets of full measure usually arise. - -## Main statements - -* `MeasureTheory.ae_of_forall_mem_of_measure_compl_eq_zero`: if `μ sᶜ = 0` and `p` holds on `s`, - then `p` holds `μ`-almost everywhere. --/ - -public section - -namespace MeasureTheory - -variable {α F : Type*} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : Set α} - {p : α → Prop} - -/-- A property that holds on a set whose complement is null holds almost everywhere. -/ -theorem ae_of_forall_mem_of_measure_compl_eq_zero (hs : μ sᶜ = 0) (hp : ∀ x ∈ s, p x) : - ∀ᵐ x ∂μ, p x := - Filter.eventually_of_mem (mem_ae_iff.2 hs) hp - -end MeasureTheory