From 1b8c75f42bec353b90612921a75837c5b86ae2de Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 12:38:03 +0100 Subject: [PATCH 1/4] feat: admissible e-variables for finitely many constraints [LRR26, Corollary 3.3], and domination by an admissible bet For the null generated by finitely many measurable constraints: every admissible e-variable is a bet, a bet is admissible exactly when no bet dominates it strictly, under the constraint qualification every bet is admissible [LRR26, Corollary 3.3], and every e-variable is dominated by an admissible bet with no constraint qualification (EValues roadmap, Layer 1.4). The last statement uses that a property holds under every member of the null exactly when it holds on a set without arbitrage that carries the null, and the compactness of the nonredundant weights of the bets [LRR26, Lemma 7.2]. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- .../EValues/ConstraintNull/Admissible.lean | 281 ++++++++++++++++++ 1 file changed, 281 insertions(+) create mode 100644 LMLExplore/EValues/ConstraintNull/Admissible.lean diff --git a/LMLExplore/EValues/ConstraintNull/Admissible.lean b/LMLExplore/EValues/ConstraintNull/Admissible.lean new file mode 100644 index 00000000..b6634f53 --- /dev/null +++ b/LMLExplore/EValues/ConstraintNull/Admissible.lean @@ -0,0 +1,281 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import LMLExplore.EValues.Admissible +public import LMLExplore.EValues.ConstraintNull.CompleteClass +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas +import Mathlib.Topology.Algebra.Module.FiniteDimension + +/-! +# Admissible e-variables for finitely many constraints + +Let `g i`, for `i` in a finite type, be measurable real constraints on a measurable space `𝓧`. By +the complete class theorem (`LMLExplore.EValues.ConstraintNull.CompleteClass`), every e-variable +for the null `constraintNull (range g)` is dominated by a bet `1 + ∑ i, π i * g i`, almost surely +under every member of the null. This file describes the admissible e-variables. + +* Every admissible e-variable is a bet, almost surely under every member of the null + [LRR26, Corollary 3.3]. +* A bet is admissible exactly when no bet dominates it strictly, almost surely under every member + of the null. Under the constraint qualification of [LRR26, Corollary 3.3], which asks that a + nonnegative combination of the constraints dominated by another one is equal to it, almost + surely under every member of the null, every bet is admissible, and the admissible e-variables + are the measurable functions equal to a bet almost surely under every member of the null. +* Every e-variable is dominated by an admissible bet, with no constraint qualification. With + [LRR26, Lemma 6.2], this says that the admissible bets form a minimal complete class, which + [LRR26, Theorem 6.5] proves under the constraint qualification and [LRR26, Section 6] + conjectures in general. + +The last statement is proved on a measurable set `Y` that carries the null and on which the +constraints admit no arbitrage. Every point of such a set is an atom of a finitely supported +member of the null, so a property holds almost surely under every member of the null exactly when +it holds on `Y`. Among the weights that dominate a given e-variable on `Y`, keep a bet +nonnegative on `Y` and have a nonredundant support, which form a compact set +[LRR26, Lemma 7.2], a maximizer of the sum of the combinations at finitely many points of `Y` +that detect the combinations vanishing on `Y` gives an admissible bet. + +## Main statements + +* `ProbabilityTheory.isCompact_nonredundantWeights_inter_nonneg`: without arbitrage on `Y`, the + nonredundant weights `π` with `1 + ∑ i, π i * a i` nonnegative on `Y` form a compact set + [LRR26, Lemma 7.2]. +* `ProbabilityTheory.forall_ae_iff_of_noArbitrageOn`: on a set without arbitrage that carries the + null, a property holds almost surely under every member of the null exactly when it holds on + the set. +* `ProbabilityTheory.IsAdmissibleEVar.exists_mem_constraintBets_ae_eq`: every admissible + e-variable is a bet [LRR26, Corollary 3.3]. +* `ProbabilityTheory.isAdmissibleEVar_ofReal_one_add_iff`: a bet is admissible exactly when no + bet dominates it strictly. +* `ProbabilityTheory.isAdmissibleEVar_ofReal_one_add_of_mem_constraintBets`, + `ProbabilityTheory.isAdmissibleEVar_constraintNull_iff`: under the constraint qualification, the + admissible e-variables are the bets [LRR26, Corollary 3.3]. +* `ProbabilityTheory.IsEVar.exists_mem_constraintBets_isAdmissibleEVar_ae_le`: every e-variable + is dominated by an admissible bet. + +## References + +* [LRR26] M. Larsson, A. Ramdas and J. Ruf, *Testing hypotheses generated by constraints*, Math. + Oper. Res. (2026), arXiv:2504.02974v5. +-/ + +public section + +open MeasureTheory Set LMLExplore +open scoped ENNReal NNReal + +namespace ProbabilityTheory + +variable {𝓧 ι : Type*} [Fintype ι] {a : ι → 𝓧 → ℝ} {Y : Set 𝓧} + +/-! ### The nonredundant weights of the bets -/ + +/-- Finitely many points of `Y` detect the combinations of the functions `a i` that vanish on +`Y`. -/ +theorem exists_finset_forall_sum_mul_eq_zero (a : ι → 𝓧 → ℝ) (Y : Set 𝓧) : + ∃ F : Finset 𝓧, ↑F ⊆ Y ∧ ∀ ρ : ι → ℝ, (∀ x ∈ F, ∑ i, ρ i * a i x = 0) → + ∀ x ∈ Y, ∑ i, ρ i * a i x = 0 := by + classical + set v : 𝓧 → ι → ℝ := fun x i ↦ a i x + obtain ⟨b, hbY, hspan, hli⟩ := exists_linearIndependent ℝ (v '' Y) + have hbfin : b.Finite := hli.set_finite_of_isNoetherian + obtain ⟨F, hFY, hFb⟩ := Finset.subset_set_image_iff.1 + (show ↑hbfin.toFinset ⊆ v '' Y by simpa using hbY) + refine ⟨F, hFY, fun ρ hρ x hx ↦ ?_⟩ + let ℓ : (ι → ℝ) →ₗ[ℝ] ℝ := Fintype.linearCombination ℝ ρ + have hℓ : ∀ y, ℓ (v y) = ∑ i, ρ i * a i y := fun y ↦ by + simp [ℓ, Fintype.linearCombination_apply, v, mul_comm] + have hb : b ⊆ LinearMap.ker ℓ := by + intro w hw + have : w ∈ F.image v := by simpa [hFb] using hw + obtain ⟨y, hy, rfl⟩ := Finset.mem_image.1 this + simp [LinearMap.mem_ker, hℓ, hρ y hy] + have h1 : v x ∈ Submodule.span ℝ b := hspan ▸ Submodule.subset_span ⟨x, hx, rfl⟩ + have := Submodule.span_le.2 hb h1 + simpa [LinearMap.mem_ker, hℓ] using this + +/-- Without arbitrage on `Y`, the nonredundant weights `π` for which `1 + ∑ i, π i * a i` is +nonnegative on `Y` form a compact set [LRR26, Lemma 7.2]. -/ +theorem isCompact_nonredundantWeights_inter_nonneg (h : NoArbitrageOn a Y) : + IsCompact (nonredundantWeights a Y ∩ {π | ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i * a i x}) := by + obtain ⟨F₀, hF₀, R, -, hbound⟩ := exists_finset_sum_le_of_noArbitrageOn h + refine isCompact_nonredundantWeights_inter ?_ (c := R * 1) fun π hπ ↦ + hbound π hπ.1 1 zero_le_one fun x hx ↦ by linarith [hπ.2 x (hF₀ hx)] + simp only [ofPred_forall] + exact isClosed_biInter fun x _ ↦ isClosed_le continuous_const (by fun_prop) + +/-! ### Properties that hold under every member of the null -/ + +variable [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞} {π : ι → ℝ≥0} + +/-- Without arbitrage on `Y`, every point of `Y` is an atom of a member of the null. -/ +theorem exists_mem_constraintNull_measure_singleton_ne_zero (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) {x₀ : 𝓧} (hx₀ : x₀ ∈ Y) : + ∃ μ ∈ constraintNull (range g), μ {x₀} ≠ 0 := by + obtain ⟨α, _, x, w, -, hw, hwg, k, hk, hwk⟩ := exists_charging_family_of_noArbitrageOn hY hx₀ + rw [mem_simplex_iff] at hw + refine ⟨∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k), + (sum_smul_dirac_mem_constraintNull_iff (forall_mem_range.2 hg) hw.1).2 + ⟨hw.2, forall_mem_range.2 hwg⟩, fun h0 ↦ ?_⟩ + have h1 : ENNReal.ofReal (w k) * Measure.dirac (x k) {x₀} ≤ + (∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k)) {x₀} := by + rw [sum_apply] + exact Finset.single_le_sum + (f := fun j ↦ (ENNReal.ofReal (w j) • Measure.dirac (x j)) {x₀}) (fun _ _ ↦ zero_le) + (Finset.mem_univ k) + rw [h0, hk, Measure.dirac_apply_of_mem (mem_singleton x₀), mul_one, nonpos_iff_eq_zero, + ENNReal.ofReal_eq_zero] at h1 + exact hwk.not_ge h1 + +/-- On a set `Y` without arbitrage that carries the null, a property holds almost surely under +every member of the null exactly when it holds on `Y`. -/ +theorem forall_ae_iff_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) + (hYμ : ∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) {p : 𝓧 → Prop} : + (∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, p x) ↔ ∀ x ∈ Y, p x := by + refine ⟨fun h x hx ↦ ?_, fun h μ hμ ↦ Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) h⟩ + by_contra hpx + obtain ⟨μ, hμ, hμx⟩ := exists_mem_constraintNull_measure_singleton_ne_zero hg hY hx + exact hμx (measure_mono_null (singleton_subset_iff.2 hpx) (ae_iff.1 (h μ hμ))) + +/-! ### Admissible e-variables -/ + +/-- **Every admissible e-variable is a bet** [LRR26, Corollary 3.3]: an admissible e-variable for +the null generated by finitely many measurable constraints `g i` is equal to a bet +`1 + ∑ i, π i * g i`, almost surely under every member of the null. -/ +theorem IsAdmissibleEVar.exists_mem_constraintBets_ae_eq (hg : ∀ i, Measurable (g i)) + (hE : IsAdmissibleEVar E (constraintNull (range g))) : + ∃ π ∈ constraintBets g, ∀ μ ∈ constraintNull (range g), + E =ᵐ[μ] fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) := by + obtain ⟨π, hπ, h⟩ := hE.toIsEVar.exists_mem_constraintBets_ae_le hg + exact ⟨π, hπ, fun μ hμ ↦ + (hE.ae_eq (isEVar_ofReal_one_add_of_mem_constraintBets hg hπ) h hμ).symm⟩ + +/-- A bet on finitely many measurable constraints is admissible exactly when no bet dominates it +strictly: every bet whose combination of the constraints is at least its own, almost surely under +every member of the null, has a combination at most its own, almost surely under every member of +the null. -/ +theorem isAdmissibleEVar_ofReal_one_add_iff (hg : ∀ i, Measurable (g i)) + (hπ : π ∈ constraintBets g) : + IsAdmissibleEVar (fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) + (constraintNull (range g)) ↔ + ∀ π' ∈ constraintBets g, + (∀ μ ∈ constraintNull (range g), + ∀ᵐ x ∂μ, ∑ i, (π i : ℝ) * g i x ≤ ∑ i, (π' i : ℝ) * g i x) → + ∀ μ ∈ constraintNull (range g), + ∀ᵐ x ∂μ, ∑ i, (π' i : ℝ) * g i x ≤ ∑ i, (π i : ℝ) * g i x := by + refine ⟨fun h π' hπ' hle μ hμ ↦ ?_, fun h ↦ + ⟨isEVar_ofReal_one_add_of_mem_constraintBets hg hπ, fun F hF hEF μ hμ ↦ ?_⟩⟩ + · have h1 := h.ae_le (isEVar_ofReal_one_add_of_mem_constraintBets hg hπ') + (fun ν hν ↦ (hle ν hν).mono fun x hx ↦ ENNReal.ofReal_le_ofReal (by linarith)) hμ + filter_upwards [h1, mem_constraintBets_iff.1 hπ μ hμ] with x hx hx0 + linarith [(ENNReal.ofReal_le_ofReal_iff hx0).1 hx] + · -- an e-variable above the bet is below another bet, which is then equal to it + obtain ⟨π', hπ', hFπ'⟩ := hF.exists_mem_constraintBets_ae_le hg + have hle : ∀ ν ∈ constraintNull (range g), + ∀ᵐ x ∂ν, ∑ i, (π i : ℝ) * g i x ≤ ∑ i, (π' i : ℝ) * g i x := fun ν hν ↦ by + filter_upwards [hEF ν hν, hFπ' ν hν, mem_constraintBets_iff.1 hπ' ν hν] with x h1 h2 h3 + linarith [(ENNReal.ofReal_le_ofReal_iff h3).1 (h1.trans h2)] + filter_upwards [hFπ' μ hμ, h π' hπ' hle μ hμ] with x h1 h2 + exact h1.trans (ENNReal.ofReal_le_ofReal (by linarith)) + +/-- **Under the constraint qualification, every bet is admissible** [LRR26, Corollary 3.3]: if a +nonnegative combination of finitely many measurable constraints that is at most another one, +almost surely under every member of the null, is equal to it almost surely under every member of +the null, then every bet is an admissible e-variable. -/ +theorem isAdmissibleEVar_ofReal_one_add_of_mem_constraintBets (hg : ∀ i, Measurable (g i)) + (hcq : ∀ ρ ρ' : ι → ℝ≥0, + (∀ μ ∈ constraintNull (range g), + ∀ᵐ x ∂μ, ∑ i, (ρ i : ℝ) * g i x ≤ ∑ i, (ρ' i : ℝ) * g i x) → + ∀ μ ∈ constraintNull (range g), + ∀ᵐ x ∂μ, ∑ i, (ρ' i : ℝ) * g i x ≤ ∑ i, (ρ i : ℝ) * g i x) + (hπ : π ∈ constraintBets g) : + IsAdmissibleEVar (fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) + (constraintNull (range g)) := + (isAdmissibleEVar_ofReal_one_add_iff hg hπ).2 fun π' _ h ↦ hcq π π' h + +/-- **The admissible e-variables under the constraint qualification** [LRR26, Corollary 3.3]: if +a nonnegative combination of finitely many measurable constraints that is at most another one, +almost surely under every member of the null, is equal to it almost surely under every member of +the null, then the admissible e-variables are the measurable functions equal to a bet +`1 + ∑ i, π i * g i`, almost surely under every member of the null. -/ +theorem isAdmissibleEVar_constraintNull_iff (hg : ∀ i, Measurable (g i)) + (hcq : ∀ ρ ρ' : ι → ℝ≥0, + (∀ μ ∈ constraintNull (range g), + ∀ᵐ x ∂μ, ∑ i, (ρ i : ℝ) * g i x ≤ ∑ i, (ρ' i : ℝ) * g i x) → + ∀ μ ∈ constraintNull (range g), + ∀ᵐ x ∂μ, ∑ i, (ρ' i : ℝ) * g i x ≤ ∑ i, (ρ i : ℝ) * g i x) : + IsAdmissibleEVar E (constraintNull (range g)) ↔ Measurable E ∧ ∃ π ∈ constraintBets g, + ∀ μ ∈ constraintNull (range g), E =ᵐ[μ] fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) := + ⟨fun hE ↦ ⟨hE.measurable, hE.exists_mem_constraintBets_ae_eq hg⟩, fun ⟨hEm, _, hπ, hEπ⟩ ↦ + (isAdmissibleEVar_ofReal_one_add_of_mem_constraintBets hg hcq hπ).congr hEm + fun μ hμ ↦ (hEπ μ hμ).symm⟩ + +/-- **Every e-variable is dominated by an admissible bet**: for the null generated by finitely +many measurable constraints `g i`, with no constraint qualification, every e-variable is at most +an admissible bet `1 + ∑ i, π i * g i`, almost surely under every member of the null. So the +admissible bets form a complete class, which is then minimal [LRR26, Lemma 6.2]; under the +constraint qualification this is [LRR26, Theorem 6.5]. -/ +theorem IsEVar.exists_mem_constraintBets_isAdmissibleEVar_ae_le (hg : ∀ i, Measurable (g i)) + (hE : IsEVar E (constraintNull (range g))) : + ∃ π ∈ constraintBets g, + IsAdmissibleEVar (fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) + (constraintNull (range g)) ∧ + ∀ μ ∈ constraintNull (range g), + E ≤ᵐ[μ] fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) := by + obtain ⟨Y, -, hYμ, hY⟩ := exists_measurableSet_noArbitrageOn hg + obtain ⟨π₀, hπ₀K, hπ₀⟩ := exists_mem_nonredundantWeights_toReal_le_of_isEVar hg hY hE + obtain ⟨F, hFY, hF⟩ := exists_finset_forall_sum_mul_eq_zero g Y + -- among the nonredundant weights of the bets that dominate `π₀` on `Y`, maximize the sum of the + -- combinations at finitely many points that detect the combinations vanishing on `Y` + set U := nonredundantWeights g Y ∩ {π | ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i * g i x} ∩ + {π | ∀ x ∈ Y, ∑ i, π₀ i * g i x ≤ ∑ i, π i * g i x} with hU_def + have hU : IsCompact U := by + refine (isCompact_nonredundantWeights_inter_nonneg hY).inter_right ?_ + simp only [ofPred_forall] + exact isClosed_biInter fun x _ ↦ isClosed_le (by fun_prop) (by fun_prop) + have hπ₀U : π₀ ∈ U := + ⟨⟨hπ₀K, fun x hx ↦ ENNReal.toReal_nonneg.trans (hπ₀ x hx)⟩, fun x hx ↦ le_rfl⟩ + obtain ⟨π, ⟨⟨hπK, hπ1⟩, hπ0⟩, hπmax⟩ := hU.exists_isMaxOn ⟨π₀, hπ₀U⟩ + (f := fun π ↦ ∑ x ∈ F, ∑ i, π i * g i x) (by fun_prop : Continuous _).continuousOn + have hcoe : ∀ i, ((π i).toNNReal : ℝ) = π i := fun i ↦ + Real.coe_toNNReal _ ((mem_nonredundantWeights_iff.1 hπK).1 i) + have hbet : (fun i ↦ (π i).toNNReal) ∈ constraintBets g := + mem_constraintBets_iff.2 ((forall_ae_iff_of_noArbitrageOn hg hY hYμ).2 fun x hx ↦ by + simpa only [hcoe] using hπ1 x hx) + refine ⟨_, hbet, (isAdmissibleEVar_ofReal_one_add_iff hg hbet).2 fun π' hπ' hle ↦ ?_, + fun μ hμ ↦ Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ ?_⟩ + · -- a bet that dominates on `Y` has, on `Y`, a combination with weights in `U`; by maximality + -- the two combinations agree at the detecting points, hence on `Y` + have hleY : ∀ x ∈ Y, ∑ i, π i * g i x ≤ ∑ i, (π' i : ℝ) * g i x := by + simpa only [hcoe] using (forall_ae_iff_of_noArbitrageOn hg hY hYμ).1 hle + have hπ'Y : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, (π' i : ℝ) * g i x := + (forall_ae_iff_of_noArbitrageOn hg hY hYμ).1 (mem_constraintBets_iff.1 hπ') + obtain ⟨π'', hπ''K, hπ''⟩ := exists_mem_nonredundantWeights_sum_mul_eq (a := g) (Y := Y) + fun i ↦ (π' i).coe_nonneg + have h1 : ∀ x ∈ Y, ∑ i, π i * g i x ≤ ∑ i, π'' i * g i x := fun x hx ↦ + (hleY x hx).trans_eq (hπ'' x hx).symm + have hπ''U : π'' ∈ U := ⟨⟨hπ''K, fun x hx ↦ by rw [hπ'' x hx]; exact hπ'Y x hx⟩, + fun x hx ↦ (hπ0 x hx).trans (h1 x hx)⟩ + have h2 : ∑ x ∈ F, ∑ i, π'' i * g i x ≤ ∑ x ∈ F, ∑ i, π i * g i x := hπmax hπ''U + have hsum : ∑ x ∈ F, (∑ i, π'' i * g i x - ∑ i, π i * g i x) = 0 := by + refine le_antisymm ?_ (Finset.sum_nonneg fun x hx ↦ sub_nonneg.2 (h1 x (hFY hx))) + rw [Finset.sum_sub_distrib] + linarith + have h3 : ∀ x ∈ F, ∑ i, (π'' i - π i) * g i x = 0 := by + intro x hx + have := (Finset.sum_eq_zero_iff_of_nonneg + (fun y hy ↦ sub_nonneg.2 (h1 y (hFY hy)))).1 hsum x hx + simpa only [sub_mul, Finset.sum_sub_distrib] using this + refine (forall_ae_iff_of_noArbitrageOn hg hY hYμ).2 fun x hx ↦ ?_ + have h4 := hF _ h3 x hx + simp only [sub_mul, Finset.sum_sub_distrib, sub_eq_zero] at h4 + simp only [hcoe] + rw [← hπ'' x hx, h4] + · simp only [hcoe] + rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hE hx).ne] + exact ENNReal.ofReal_le_ofReal ((hπ₀ x hx).trans (by linarith [hπ0 x hx])) + +end ProbabilityTheory From e6ca76397d4f732ffcc75837e570dad3d54ee238 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 13:03:09 +0100 Subject: [PATCH 2/4] refactor: move supporting lemmas of the admissibility file to their homes Move exists_finset_forall_sum_mul_eq_zero, generalised to a field and reproved with Submodule.exists_finset_span_eq_linearIndepOn, to the new LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean, together with the new forall_sum_mul_eq_of_forall_le_of_sum_le factored out of the domination proof. Move isCompact_nonredundantWeights_inter_nonneg, exists_mem_constraintNull_measure_singleton_ne_zero and forall_ae_iff_of_noArbitrageOn to CompleteClass.lean, and use forall_ae_iff_of_noArbitrageOn for the domination bullet. Co-Authored-By: Claude Code --- .../EValues/ConstraintNull/Admissible.lean | 98 ++----------------- .../EValues/ConstraintNull/CompleteClass.lean | 48 ++++++++- .../FiniteDimensional/Lemmas.lean | 78 +++++++++++++++ 3 files changed, 131 insertions(+), 93 deletions(-) create mode 100644 LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean diff --git a/LMLExplore/EValues/ConstraintNull/Admissible.lean b/LMLExplore/EValues/ConstraintNull/Admissible.lean index b6634f53..122ef545 100644 --- a/LMLExplore/EValues/ConstraintNull/Admissible.lean +++ b/LMLExplore/EValues/ConstraintNull/Admissible.lean @@ -7,8 +7,7 @@ module public import LMLExplore.EValues.Admissible public import LMLExplore.EValues.ConstraintNull.CompleteClass -import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas -import Mathlib.Topology.Algebra.Module.FiniteDimension +import LMLExplore.LinearAlgebra.FiniteDimensional.Lemmas /-! # Admissible e-variables for finitely many constraints @@ -40,12 +39,6 @@ that detect the combinations vanishing on `Y` gives an admissible bet. ## Main statements -* `ProbabilityTheory.isCompact_nonredundantWeights_inter_nonneg`: without arbitrage on `Y`, the - nonredundant weights `π` with `1 + ∑ i, π i * a i` nonnegative on `Y` form a compact set - [LRR26, Lemma 7.2]. -* `ProbabilityTheory.forall_ae_iff_of_noArbitrageOn`: on a set without arbitrage that carries the - null, a property holds almost surely under every member of the null exactly when it holds on - the set. * `ProbabilityTheory.IsAdmissibleEVar.exists_mem_constraintBets_ae_eq`: every admissible e-variable is a bet [LRR26, Corollary 3.3]. * `ProbabilityTheory.isAdmissibleEVar_ofReal_one_add_iff`: a bet is admissible exactly when no @@ -69,76 +62,8 @@ open scoped ENNReal NNReal namespace ProbabilityTheory -variable {𝓧 ι : Type*} [Fintype ι] {a : ι → 𝓧 → ℝ} {Y : Set 𝓧} - -/-! ### The nonredundant weights of the bets -/ - -/-- Finitely many points of `Y` detect the combinations of the functions `a i` that vanish on -`Y`. -/ -theorem exists_finset_forall_sum_mul_eq_zero (a : ι → 𝓧 → ℝ) (Y : Set 𝓧) : - ∃ F : Finset 𝓧, ↑F ⊆ Y ∧ ∀ ρ : ι → ℝ, (∀ x ∈ F, ∑ i, ρ i * a i x = 0) → - ∀ x ∈ Y, ∑ i, ρ i * a i x = 0 := by - classical - set v : 𝓧 → ι → ℝ := fun x i ↦ a i x - obtain ⟨b, hbY, hspan, hli⟩ := exists_linearIndependent ℝ (v '' Y) - have hbfin : b.Finite := hli.set_finite_of_isNoetherian - obtain ⟨F, hFY, hFb⟩ := Finset.subset_set_image_iff.1 - (show ↑hbfin.toFinset ⊆ v '' Y by simpa using hbY) - refine ⟨F, hFY, fun ρ hρ x hx ↦ ?_⟩ - let ℓ : (ι → ℝ) →ₗ[ℝ] ℝ := Fintype.linearCombination ℝ ρ - have hℓ : ∀ y, ℓ (v y) = ∑ i, ρ i * a i y := fun y ↦ by - simp [ℓ, Fintype.linearCombination_apply, v, mul_comm] - have hb : b ⊆ LinearMap.ker ℓ := by - intro w hw - have : w ∈ F.image v := by simpa [hFb] using hw - obtain ⟨y, hy, rfl⟩ := Finset.mem_image.1 this - simp [LinearMap.mem_ker, hℓ, hρ y hy] - have h1 : v x ∈ Submodule.span ℝ b := hspan ▸ Submodule.subset_span ⟨x, hx, rfl⟩ - have := Submodule.span_le.2 hb h1 - simpa [LinearMap.mem_ker, hℓ] using this - -/-- Without arbitrage on `Y`, the nonredundant weights `π` for which `1 + ∑ i, π i * a i` is -nonnegative on `Y` form a compact set [LRR26, Lemma 7.2]. -/ -theorem isCompact_nonredundantWeights_inter_nonneg (h : NoArbitrageOn a Y) : - IsCompact (nonredundantWeights a Y ∩ {π | ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i * a i x}) := by - obtain ⟨F₀, hF₀, R, -, hbound⟩ := exists_finset_sum_le_of_noArbitrageOn h - refine isCompact_nonredundantWeights_inter ?_ (c := R * 1) fun π hπ ↦ - hbound π hπ.1 1 zero_le_one fun x hx ↦ by linarith [hπ.2 x (hF₀ hx)] - simp only [ofPred_forall] - exact isClosed_biInter fun x _ ↦ isClosed_le continuous_const (by fun_prop) - -/-! ### Properties that hold under every member of the null -/ - -variable [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞} {π : ι → ℝ≥0} - -/-- Without arbitrage on `Y`, every point of `Y` is an atom of a member of the null. -/ -theorem exists_mem_constraintNull_measure_singleton_ne_zero (hg : ∀ i, Measurable (g i)) - (hY : NoArbitrageOn g Y) {x₀ : 𝓧} (hx₀ : x₀ ∈ Y) : - ∃ μ ∈ constraintNull (range g), μ {x₀} ≠ 0 := by - obtain ⟨α, _, x, w, -, hw, hwg, k, hk, hwk⟩ := exists_charging_family_of_noArbitrageOn hY hx₀ - rw [mem_simplex_iff] at hw - refine ⟨∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k), - (sum_smul_dirac_mem_constraintNull_iff (forall_mem_range.2 hg) hw.1).2 - ⟨hw.2, forall_mem_range.2 hwg⟩, fun h0 ↦ ?_⟩ - have h1 : ENNReal.ofReal (w k) * Measure.dirac (x k) {x₀} ≤ - (∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k)) {x₀} := by - rw [sum_apply] - exact Finset.single_le_sum - (f := fun j ↦ (ENNReal.ofReal (w j) • Measure.dirac (x j)) {x₀}) (fun _ _ ↦ zero_le) - (Finset.mem_univ k) - rw [h0, hk, Measure.dirac_apply_of_mem (mem_singleton x₀), mul_one, nonpos_iff_eq_zero, - ENNReal.ofReal_eq_zero] at h1 - exact hwk.not_ge h1 - -/-- On a set `Y` without arbitrage that carries the null, a property holds almost surely under -every member of the null exactly when it holds on `Y`. -/ -theorem forall_ae_iff_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) - (hYμ : ∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) {p : 𝓧 → Prop} : - (∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, p x) ↔ ∀ x ∈ Y, p x := by - refine ⟨fun h x hx ↦ ?_, fun h μ hμ ↦ Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) h⟩ - by_contra hpx - obtain ⟨μ, hμ, hμx⟩ := exists_mem_constraintNull_measure_singleton_ne_zero hg hY hx - exact hμx (measure_mono_null (singleton_subset_iff.2 hpx) (ae_iff.1 (h μ hμ))) +variable {𝓧 ι : Type*} [Fintype ι] [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {E : 𝓧 → ℝ≥0∞} + {π : ι → ℝ≥0} /-! ### Admissible e-variables -/ @@ -246,7 +171,7 @@ theorem IsEVar.exists_mem_constraintBets_isAdmissibleEVar_ae_le (hg : ∀ i, Mea mem_constraintBets_iff.2 ((forall_ae_iff_of_noArbitrageOn hg hY hYμ).2 fun x hx ↦ by simpa only [hcoe] using hπ1 x hx) refine ⟨_, hbet, (isAdmissibleEVar_ofReal_one_add_iff hg hbet).2 fun π' hπ' hle ↦ ?_, - fun μ hμ ↦ Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ ?_⟩ + (forall_ae_iff_of_noArbitrageOn hg hY hYμ).2 fun x hx ↦ ?_⟩ · -- a bet that dominates on `Y` has, on `Y`, a combination with weights in `U`; by maximality -- the two combinations agree at the detecting points, hence on `Y` have hleY : ∀ x ∈ Y, ∑ i, π i * g i x ≤ ∑ i, (π' i : ℝ) * g i x := by @@ -259,21 +184,10 @@ theorem IsEVar.exists_mem_constraintBets_isAdmissibleEVar_ae_le (hg : ∀ i, Mea (hleY x hx).trans_eq (hπ'' x hx).symm have hπ''U : π'' ∈ U := ⟨⟨hπ''K, fun x hx ↦ by rw [hπ'' x hx]; exact hπ'Y x hx⟩, fun x hx ↦ (hπ0 x hx).trans (h1 x hx)⟩ - have h2 : ∑ x ∈ F, ∑ i, π'' i * g i x ≤ ∑ x ∈ F, ∑ i, π i * g i x := hπmax hπ''U - have hsum : ∑ x ∈ F, (∑ i, π'' i * g i x - ∑ i, π i * g i x) = 0 := by - refine le_antisymm ?_ (Finset.sum_nonneg fun x hx ↦ sub_nonneg.2 (h1 x (hFY hx))) - rw [Finset.sum_sub_distrib] - linarith - have h3 : ∀ x ∈ F, ∑ i, (π'' i - π i) * g i x = 0 := by - intro x hx - have := (Finset.sum_eq_zero_iff_of_nonneg - (fun y hy ↦ sub_nonneg.2 (h1 y (hFY hy)))).1 hsum x hx - simpa only [sub_mul, Finset.sum_sub_distrib] using this + have h2 := forall_sum_mul_eq_of_forall_le_of_sum_le hFY hF h1 (hπmax hπ''U) refine (forall_ae_iff_of_noArbitrageOn hg hY hYμ).2 fun x hx ↦ ?_ - have h4 := hF _ h3 x hx - simp only [sub_mul, Finset.sum_sub_distrib, sub_eq_zero] at h4 simp only [hcoe] - rw [← hπ'' x hx, h4] + rw [← hπ'' x hx, h2 x hx] · simp only [hcoe] rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hE hx).ne] exact ENNReal.ofReal_le_ofReal ((hπ₀ x hx).trans (by linarith [hπ0 x hx])) diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean index cc72149e..0fe9a560 100644 --- a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean +++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean @@ -44,7 +44,8 @@ The proof here is finite-dimensional, in three steps. The finite-dimensional theorem only uses the finitely supported members of the null. Applied to multiples of the indicator of a point, it shows that every point of `Y` is charged by a finitely -supported member of the null, so that e-variables are finite on `Y`. +supported member of the null, so that e-variables are finite on `Y`, and that a property holds +almost surely under every member of the null exactly when it holds on `Y`. ## Main definitions @@ -59,12 +60,18 @@ supported member of the null, so that e-variables are finite on `Y`. on `Y`, a combination with nonredundant weights [LRR26, Lemma 3.2]. * `ProbabilityTheory.exists_finset_sum_le_of_noArbitrageOn`: without arbitrage, the total mass of nonredundant weights is controlled at finitely many points [LRR26, proof of Lemma 7.2]. +* `ProbabilityTheory.isCompact_nonredundantWeights_inter_nonneg`: without arbitrage on `Y`, the + nonredundant weights `π` with `1 + ∑ i, π i * a i` nonnegative on `Y` form a compact set + [LRR26, Lemma 7.2]. * `ProbabilityTheory.exists_mem_nonredundantWeights_le_of_noArbitrageOn`: the complete class theorem in finite-dimensional form, on a set without arbitrage. * `ProbabilityTheory.exists_measurableSet_noArbitrageOn`: a measurable set carrying the null, on which the constraints admit no arbitrage. * `ProbabilityTheory.lt_top_of_isEVar_of_noArbitrageOn`: e-variables are finite on a set without arbitrage. +* `ProbabilityTheory.forall_ae_iff_of_noArbitrageOn`: on a set without arbitrage that carries the + null, a property holds almost surely under every member of the null exactly when it holds on + the set. * `ProbabilityTheory.forall_integral_nonpos_iff_exists_ae_le`: **the complete class theorem** [LRR26, Theorem 3.1]. * `ProbabilityTheory.IsEVar.exists_mem_constraintBets_ae_le`, @@ -261,6 +268,16 @@ theorem exists_finset_sum_le_of_noArbitrageOn (h : NoArbitrageOn a Y) : rw [mul_one_div, div_lt_iff₀ (by positivity)] at this linarith +/-- Without arbitrage on `Y`, the nonredundant weights `π` for which `1 + ∑ i, π i * a i` is +nonnegative on `Y` form a compact set [LRR26, Lemma 7.2]. -/ +theorem isCompact_nonredundantWeights_inter_nonneg (h : NoArbitrageOn a Y) : + IsCompact (nonredundantWeights a Y ∩ {π | ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i * a i x}) := by + obtain ⟨F₀, hF₀, R, -, hbound⟩ := exists_finset_sum_le_of_noArbitrageOn h + refine isCompact_nonredundantWeights_inter ?_ (c := R * 1) fun π hπ ↦ + hbound π hπ.1 1 zero_le_one fun x hx ↦ by linarith [hπ.2 x (hF₀ hx)] + simp only [ofPred_forall] + exact isClosed_biInter fun x _ ↦ isClosed_le continuous_const (by fun_prop) + /-- The finite step of the complete class theorem, up to `δ`: if `f` has a nonpositive mean under every finitely supported law on `Y` under which the functions `a i` have nonpositive means, then on a finite subset of `Y` it is at most `δ` plus a nonnegative combination of the `a i`. The proof @@ -515,6 +532,35 @@ theorem lt_top_of_isEVar_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : N rw [htop, ENNReal.mul_top (by simpa using hwk)] at h2 exact ENNReal.one_ne_top (top_le_iff.1 h2) +/-- Without arbitrage on `Y`, every point of `Y` is an atom of a member of the null. -/ +theorem exists_mem_constraintNull_measure_singleton_ne_zero (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) {x₀ : 𝓧} (hx₀ : x₀ ∈ Y) : + ∃ μ ∈ constraintNull (range g), μ {x₀} ≠ 0 := by + obtain ⟨α, _, x, w, -, hw, hwg, k, hk, hwk⟩ := exists_charging_family_of_noArbitrageOn hY hx₀ + rw [mem_simplex_iff] at hw + refine ⟨∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k), + (sum_smul_dirac_mem_constraintNull_iff (forall_mem_range.2 hg) hw.1).2 + ⟨hw.2, forall_mem_range.2 hwg⟩, fun h0 ↦ ?_⟩ + have h1 : ENNReal.ofReal (w k) * Measure.dirac (x k) {x₀} ≤ + (∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k)) {x₀} := by + rw [sum_apply] + exact Finset.single_le_sum + (f := fun j ↦ (ENNReal.ofReal (w j) • Measure.dirac (x j)) {x₀}) (fun _ _ ↦ zero_le) + (Finset.mem_univ k) + rw [h0, hk, Measure.dirac_apply_of_mem (mem_singleton x₀), mul_one, nonpos_iff_eq_zero, + ENNReal.ofReal_eq_zero] at h1 + exact hwk.not_ge h1 + +/-- On a set `Y` without arbitrage that carries the null, a property holds almost surely under +every member of the null exactly when it holds on `Y`. -/ +theorem forall_ae_iff_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) + (hYμ : ∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) {p : 𝓧 → Prop} : + (∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, p x) ↔ ∀ x ∈ Y, p x := by + refine ⟨fun h x hx ↦ ?_, fun h μ hμ ↦ Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) h⟩ + by_contra hpx + obtain ⟨μ, hμ, hμx⟩ := exists_mem_constraintNull_measure_singleton_ne_zero hg hY hx + exact hμx (measure_mono_null (singleton_subset_iff.2 hpx) (ae_iff.1 (h μ hμ))) + /-! ### The complete class theorem -/ /-- **The complete class theorem on a set without arbitrage**: a measurable `f` with a nonpositive diff --git a/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean b/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean new file mode 100644 index 00000000..aa24956d --- /dev/null +++ b/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean @@ -0,0 +1,78 @@ +/- +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.Field.Basic +public import Mathlib.Data.Fintype.BigOperators +import Mathlib.LinearAlgebra.Dimension.StrongRankCondition +import Mathlib.LinearAlgebra.FiniteDimensional.Defs +import Mathlib.LinearAlgebra.Finsupp.LinearCombination + +/-! +# Finitely many points detect the combinations vanishing on a set + +Let `a i : 𝓧 → K`, for `i` in a finite type, be functions on a type `𝓧` with values in a field +`K`, and let `Y` be a set in `𝓧`. The vectors `(a i x)_i`, for `x ∈ Y`, span a finite-dimensional +subspace of `ι → K`, so finitely many of them already span it: a combination `∑ i, ρ i * a i` +vanishing at finitely many well chosen points of `Y` vanishes on `Y`. + +In a linearly ordered field, two combinations, one at most the other on `Y`, whose sums over these +finitely many points are in the opposite order, are then equal on `Y`. + +## Main statements + +* `exists_finset_forall_sum_mul_eq_zero`: finitely many points of `Y` detect the combinations of + the functions `a i` that vanish on `Y`. +* `forall_sum_mul_eq_of_forall_le_of_sum_le`: two combinations, one at most the other on `Y`, with + sums over the detecting points in the opposite order, are equal on `Y`. +-/ + +public section + +variable {𝓧 ι K : Type*} [Fintype ι] {a : ι → 𝓧 → K} {Y : Set 𝓧} + +/-- Finitely many points of `Y` detect the combinations of the functions `a i` that vanish on +`Y`. -/ +theorem exists_finset_forall_sum_mul_eq_zero [Field K] (a : ι → 𝓧 → K) (Y : Set 𝓧) : + ∃ F : Finset 𝓧, ↑F ⊆ Y ∧ ∀ ρ : ι → K, (∀ x ∈ F, ∑ i, ρ i * a i x = 0) → + ∀ x ∈ Y, ∑ i, ρ i * a i x = 0 := by + classical + set v : 𝓧 → ι → K := fun x i ↦ a i x + obtain ⟨t, htY, -, hspan, -⟩ := Submodule.exists_finset_span_eq_linearIndepOn K (v '' Y) + obtain ⟨F, hFY, rfl⟩ := Finset.subset_set_image_iff.1 htY + refine ⟨F, hFY, fun ρ hρ x hx ↦ ?_⟩ + let ℓ : (ι → K) →ₗ[K] K := Fintype.linearCombination K ρ + have hℓ : ∀ y, ℓ (v y) = ∑ i, ρ i * a i y := fun y ↦ by + simp [ℓ, Fintype.linearCombination_apply, v, mul_comm] + have hb : ↑(F.image v) ⊆ (LinearMap.ker ℓ : Set (ι → K)) := by + intro w hw + obtain ⟨y, hy, rfl⟩ := Finset.mem_image.1 hw + simp [LinearMap.mem_ker, hℓ, hρ y hy] + have h1 : v x ∈ Submodule.span K (↑(F.image v) : Set (ι → K)) := + hspan ▸ Submodule.subset_span ⟨x, hx, rfl⟩ + simpa [LinearMap.mem_ker, hℓ] using Submodule.span_le.2 hb h1 + +/-- If finitely many points `F ⊆ Y` detect the combinations of the functions `a i` that vanish on +`Y`, then two combinations, one at most the other on `Y`, whose sums over `F` are in the opposite +order, are equal on `Y`. -/ +theorem forall_sum_mul_eq_of_forall_le_of_sum_le [Field K] [LinearOrder K] + [IsStrictOrderedRing K] {F : Finset 𝓧} (hFY : ↑F ⊆ Y) + (hF : ∀ ρ : ι → K, (∀ x ∈ F, ∑ i, ρ i * a i x = 0) → ∀ x ∈ Y, ∑ i, ρ i * a i x = 0) + {ρ ρ' : ι → K} (hle : ∀ x ∈ Y, ∑ i, ρ i * a i x ≤ ∑ i, ρ' i * a i x) + (hsum : ∑ x ∈ F, ∑ i, ρ' i * a i x ≤ ∑ x ∈ F, ∑ i, ρ i * a i x) : + ∀ x ∈ Y, ∑ i, ρ i * a i x = ∑ i, ρ' i * a i x := by + -- the nonnegative differences on `F` have a nonpositive sum, so they vanish on `F` + have h0 : ∑ x ∈ F, (∑ i, ρ' i * a i x - ∑ i, ρ i * a i x) = 0 := by + refine le_antisymm ?_ (Finset.sum_nonneg fun x hx ↦ sub_nonneg.2 (hle x (hFY hx))) + rw [Finset.sum_sub_distrib] + exact sub_nonpos.2 hsum + have hF0 : ∀ x ∈ F, ∑ i, (ρ' i - ρ i) * a i x = 0 := fun x hx ↦ by + simpa only [sub_mul, Finset.sum_sub_distrib] using (Finset.sum_eq_zero_iff_of_nonneg + (fun y hy ↦ sub_nonneg.2 (hle y (hFY hy)))).1 h0 x hx + intro x hx + have := hF _ hF0 x hx + simp only [sub_mul, Finset.sum_sub_distrib, sub_eq_zero] at this + exact this.symm From 292ee4bca82d6016d886b3d20f4d625acf10710b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 13:31:26 +0100 Subject: [PATCH 3/4] refactor: use Finset.sum_eq_sum_iff_of_le in forall_sum_mul_eq_of_forall_le_of_sum_le Co-Authored-By: Claude Code --- .../LinearAlgebra/FiniteDimensional/Lemmas.lean | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean b/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean index aa24956d..64d6f9c4 100644 --- a/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean +++ b/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean @@ -64,15 +64,11 @@ theorem forall_sum_mul_eq_of_forall_le_of_sum_le [Field K] [LinearOrder K] {ρ ρ' : ι → K} (hle : ∀ x ∈ Y, ∑ i, ρ i * a i x ≤ ∑ i, ρ' i * a i x) (hsum : ∑ x ∈ F, ∑ i, ρ' i * a i x ≤ ∑ x ∈ F, ∑ i, ρ i * a i x) : ∀ x ∈ Y, ∑ i, ρ i * a i x = ∑ i, ρ' i * a i x := by - -- the nonnegative differences on `F` have a nonpositive sum, so they vanish on `F` - have h0 : ∑ x ∈ F, (∑ i, ρ' i * a i x - ∑ i, ρ i * a i x) = 0 := by - refine le_antisymm ?_ (Finset.sum_nonneg fun x hx ↦ sub_nonneg.2 (hle x (hFY hx))) - rw [Finset.sum_sub_distrib] - exact sub_nonpos.2 hsum - have hF0 : ∀ x ∈ F, ∑ i, (ρ' i - ρ i) * a i x = 0 := fun x hx ↦ by - simpa only [sub_mul, Finset.sum_sub_distrib] using (Finset.sum_eq_zero_iff_of_nonneg - (fun y hy ↦ sub_nonneg.2 (hle y (hFY hy)))).1 h0 x hx + -- the sums over `F` are equal, so the two combinations agree on `F` + have hF0 := (Finset.sum_eq_sum_iff_of_le fun x hx ↦ hle x (hFY hx)).1 + (le_antisymm (Finset.sum_le_sum fun x hx ↦ hle x (hFY hx)) hsum) intro x hx - have := hF _ hF0 x hx - simp only [sub_mul, Finset.sum_sub_distrib, sub_eq_zero] at this + have := hF (ρ' - ρ) (fun y hy ↦ by + simp [sub_mul, Finset.sum_sub_distrib, hF0 y hy]) x hx + simp only [Pi.sub_apply, sub_mul, Finset.sum_sub_distrib, sub_eq_zero] at this exact this.symm From 2ae5b9ca897774462f98d25bf4b6def6fcf5ef6a Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:00:50 +0100 Subject: [PATCH 4/4] refactor: weaken assumptions and namespace the finite-detection lemmas Generalise forall_sum_mul_eq_of_forall_le_of_sum_le from a linearly ordered field to an ordered ring, and move both lemmas of LinearAlgebra/FiniteDimensional/Lemmas.lean into namespace LMLExplore. Co-Authored-By: Claude Code --- LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean b/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean index 64d6f9c4..2fd71b86 100644 --- a/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean +++ b/LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean @@ -19,7 +19,7 @@ Let `a i : 𝓧 → K`, for `i` in a finite type, be functions on a type `𝓧` subspace of `ι → K`, so finitely many of them already span it: a combination `∑ i, ρ i * a i` vanishing at finitely many well chosen points of `Y` vanishes on `Y`. -In a linearly ordered field, two combinations, one at most the other on `Y`, whose sums over these +In an ordered ring, two combinations, one at most the other on `Y`, whose sums over these finitely many points are in the opposite order, are then equal on `Y`. ## Main statements @@ -32,6 +32,8 @@ finitely many points are in the opposite order, are then equal on `Y`. public section +namespace LMLExplore + variable {𝓧 ι K : Type*} [Fintype ι] {a : ι → 𝓧 → K} {Y : Set 𝓧} /-- Finitely many points of `Y` detect the combinations of the functions `a i` that vanish on @@ -58,8 +60,8 @@ theorem exists_finset_forall_sum_mul_eq_zero [Field K] (a : ι → 𝓧 → K) ( /-- If finitely many points `F ⊆ Y` detect the combinations of the functions `a i` that vanish on `Y`, then two combinations, one at most the other on `Y`, whose sums over `F` are in the opposite order, are equal on `Y`. -/ -theorem forall_sum_mul_eq_of_forall_le_of_sum_le [Field K] [LinearOrder K] - [IsStrictOrderedRing K] {F : Finset 𝓧} (hFY : ↑F ⊆ Y) +theorem forall_sum_mul_eq_of_forall_le_of_sum_le [Ring K] [PartialOrder K] + [IsOrderedAddMonoid K] {F : Finset 𝓧} (hFY : ↑F ⊆ Y) (hF : ∀ ρ : ι → K, (∀ x ∈ F, ∑ i, ρ i * a i x = 0) → ∀ x ∈ Y, ∑ i, ρ i * a i x = 0) {ρ ρ' : ι → K} (hle : ∀ x ∈ Y, ∑ i, ρ i * a i x ≤ ∑ i, ρ' i * a i x) (hsum : ∑ x ∈ F, ∑ i, ρ' i * a i x ≤ ∑ x ∈ F, ∑ i, ρ i * a i x) : @@ -72,3 +74,5 @@ theorem forall_sum_mul_eq_of_forall_le_of_sum_le [Field K] [LinearOrder K] simp [sub_mul, Finset.sum_sub_distrib, hF0 y hy]) x hx simp only [Pi.sub_apply, sub_mul, Finset.sum_sub_distrib, sub_eq_zero] at this exact this.symm + +end LMLExplore