EconCSLib.Math.Simplex

Generic utilities for working with the standard simplex stdSimplex 𝕜 I.

This module is neutral shared infrastructure: it provides simplex-indexed affine combinations and weighted sums, without any game-specific interpretation. Strategic games, lotteries, and utility theory all build on these lemmas.

Main definitions

• stdSimplex.affineCombination — affine combination using simplex weights
• wsum — weighted sum/dot product: ∑ᵢ xᵢ · f(i) for x : stdSimplex 𝕜 I

Main results

• wsum_const — weighted sum of a constant equals the constant
• wsum_le_wsum — monotonicity: pointwise ≤ implies weighted-sum ≤
• wsum_nonneg — non-negativity: non-negative summands give non-negative total
• wsum_add — weighted sums distribute over addition
• wsum_smul — weighted sums distribute over scalar multiplication
• wsum_wsum_comm — exchange order of iterated weighted sums
• wsum_pure — a point mass evaluates the selected coordinate

Attribution

Adapted from GameTheory/Simplex.lean and helper lemmas in GameTheory/Zerosum.lean from math-xmum/gametheory.

noncomputable def stdSimplex.affineCombination {k : Type u_3} {V : Type u_4} {P : Type u_5} {I : Type u_6} [Ring k] [PartialOrder k] [Fintype I] [AddCommGroup V] [Module k V] [AddTorsor V P] (x : ↑(stdSimplex k I)) (p : I → P) : P

Affine combination of a finite family of points using simplex weights.

This is a thin wrapper around Mathlib's Finset.affineCombination, specialized to weights coming from stdSimplex.

Equations

• stdSimplex.affineCombination x p = (Finset.affineCombination k Finset.univ p) ⇑x

@[simp]

theorem stdSimplex.affineCombination_eq_linearCombination {k : Type u_3} {V : Type u_4} {I : Type u_5} [Ring k] [PartialOrder k] [Fintype I] [AddCommGroup V] [Module k V] (x : ↑(stdSimplex k I)) (p : I → V) : affineCombination x p = (Fintype.linearCombination k p) ⇑x

In a module, simplex affine combinations are Mathlib finite linear combinations.

@[reducible, inline]

abbrev wsum {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} [Fintype I] (x : ↑(stdSimplex 𝕜 I)) (f : I → 𝕜) : 𝕜

Weighted sum of f with weights from a simplex element x. Thin abbrev over Mathlib's finite dot product ⬝ᵥ: definitionally equal, so simp [wsum] (or no unfold at all) switches between the two forms. Kept as a named concept because the simplex-specific lemmas below (wsum_const, wsum_le_wsum, wsum_nonneg, wsum_pure) depend on ∑ x = 1 or x ≥ 0 and have no generic dotProduct analogue.

Equations

• wsum x f = ⇑x ⬝ᵥ f

theorem wsum_const {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (x : ↑(stdSimplex 𝕜 I)) (c : 𝕜) : (wsum x fun (x : I) => c) = c

Weighted sum of a constant equals the constant.

theorem wsum_le_wsum {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (x : ↑(stdSimplex 𝕜 I)) {f g : I → 𝕜} (h : ∀ (i : I), f i ≤ g i) : wsum x f ≤ wsum x g

Weighted sum is monotone: pointwise ≤ implies wsum ≤.

theorem wsum_nonneg {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (x : ↑(stdSimplex 𝕜 I)) {f : I → 𝕜} (h : ∀ (i : I), 0 ≤ f i) : 0 ≤ wsum x f

Weighted sum of non-negative values is non-negative.

theorem wsum_pos {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (x : ↑(stdSimplex 𝕜 I)) {f : I → 𝕜} (hf : ∀ (i : I), 0 < f i) : 0 < wsum x f

Weighted sum of strictly-positive values is strictly positive.

Some coordinate a of any simplex point is strictly positive (since ∑ x = 1), and the corresponding x_a · f a summand is strictly positive while every other summand is non-negative.

theorem wsum_ge_wsum {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (x : ↑(stdSimplex 𝕜 I)) {f g : I → 𝕜} (h : ∀ (i : I), f i ≥ g i) : wsum x f ≥ wsum x g

Weighted sum respects ≥.

theorem wsum_add {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (x : ↑(stdSimplex 𝕜 I)) (f g : I → 𝕜) : wsum x (f + g) = wsum x f + wsum x g

Weighted sum is linear over addition.

theorem wsum_smul {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (x : ↑(stdSimplex 𝕜 I)) (c : 𝕜) (f : I → 𝕜) : wsum x (c • f) = c * wsum x f

Weighted sum commutes with scalar multiplication.

Convex combination of two simplex points (mix)

def stdSimplex.mix {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (α : 𝕜) (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (x y : ↑(stdSimplex 𝕜 I)) : ↑(stdSimplex 𝕜 I)

Convex combination of two simplex points: mix α hα₀ hα₁ x y = α·x + (1-α)·y.

This is the basic vocabulary for compound lotteries and for any inductive argument that interpolates between two mixed strategies (Loomis, Sion, fictitious play). The hypotheses are passed as plain (α : 𝕜) (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) rather than via a unit-interval subtype to match Mathlib idioms and to keep call sites lightweight.

Equations

• stdSimplex.mix α hα₀ hα₁ x y = ⟨fun (i : I) => α * ↑x i + (1 - α) * ↑y i, ⋯⟩

@[simp]

theorem stdSimplex.mix_apply {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (α : 𝕜) (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (x y : ↑(stdSimplex 𝕜 I)) (i : I) : ↑(mix α hα₀ hα₁ x y) i = α * ↑x i + (1 - α) * ↑y i

theorem wsum_mix {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] (α : 𝕜) (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (x y : ↑(stdSimplex 𝕜 I)) (f : I → 𝕜) : wsum (stdSimplex.mix α hα₀ hα₁ x y) f = α * wsum x f + (1 - α) * wsum y f

Bilinearity of wsum over stdSimplex.mix: wsum (mix α x y) f = α · wsum x f + (1-α) · wsum y f.

Ordered-field arithmetic helpers about convex combinations

These work directly on the scalar expression α · x + (1-α) · y without reference to stdSimplex. They are the algebraic ingredients used to derive strict-monotonicity facts about wsum_mix below.

theorem linear_comb_gt_left {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜} (H : x < y) {α : 𝕜} (Hα : α < 1) : x < α * x + (1 - α) * y

If x < y and α < 1, then α·x + (1-α)·y > x.

theorem linear_comb_gt_right {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜} (H : y < x) {α : 𝕜} (Hα : 0 < α) : y < α * x + (1 - α) * y

If y < x and 0 < α, then α·x + (1-α)·y > y.

theorem linear_comb_gt_of_ge_gt {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y c : 𝕜) (H1 : c ≤ x) (H2 : c < y) {α : 𝕜} (hα₀ : 0 ≤ α) (hα₁ : α < 1) : c < α * x + (1 - α) * y

Convex combination of "≥ c" and "> c" stays "> c" (provided α ≥ 0 and α < 1).

theorem linear_comb_lt_of_le_lt {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y c : 𝕜) (H1 : x ≤ c) (H2 : y < c) {α : 𝕜} (hα₀ : 0 ≤ α) (hα₁ : α < 1) : α * x + (1 - α) * y < c

Convex combination of "≤ c" and "< c" stays "< c" (provided α ≥ 0 and α < 1).

Strict monotonicity of wsum_mix

theorem wsum_mix_gt_of_ge_gt {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_3} [Fintype I] (f : I → 𝕜) (x y : ↑(stdSimplex 𝕜 I)) (c : 𝕜) (H1 : c ≤ wsum x f) (H2 : c < wsum y f) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (Ht : t < 1) : c < wsum (stdSimplex.mix t ht₀ ht₁ x y) f

wsum version of linear_comb_gt_of_ge_gt.

theorem wsum_mix_lt_of_le_lt {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_3} [Fintype I] (f : I → 𝕜) (x y : ↑(stdSimplex 𝕜 I)) (c : 𝕜) (H1 : wsum x f ≤ c) (H2 : wsum y f < c) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (Ht : t < 1) : wsum (stdSimplex.mix t ht₀ ht₁ x y) f < c

wsum version of linear_comb_lt_of_le_lt.

Neighborhood existential for convex combinations

If c < x, then there is an interior t ∈ (0,1) with c < t·x + (1-t)·y. Over a general ordered field this is the elementary fact that the segment s ↦ s·x + (1-s)·y from y to x stays above c near s = 1; we pick t explicitly (no continuity), so it holds for any [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]. This is the key ingredient for the Loomis-style inductive step (perturbing the optimiser a little in the y-direction).

theorem mix_gt_of_gt_nbh {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y c : 𝕜) (H : c < x) : ∃ (t : 𝕜), 0 < t ∧ t < 1 ∧ c < t * x + (1 - t) * y

Existence of a strictly interior t keeping t·x + (1-t)·y > c, given c < x. Constructive over any ordered field: pick t just above the crossing threshold (c-y)/(x-y) (clamped to 0) when y < x, or any interior t when x ≤ y.

theorem mix_lt_of_lt_nbh {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y c : 𝕜) (H : x < c) : ∃ (t : 𝕜), 0 < t ∧ t < 1 ∧ t * x + (1 - t) * y < c

Dual: strictly interior t keeping t·x + (1-t)·y < c, given x < c. Obtained from mix_gt_of_gt_nbh by negating x, y, c.

theorem wsum_wsum_comm {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] {J : Type u_3} [Fintype J] (x : ↑(stdSimplex 𝕜 I)) (y : ↑(stdSimplex 𝕜 J)) (A : I → J → 𝕜) : (wsum x fun (i : I) => wsum y (A i)) = wsum y fun (j : J) => wsum x fun (i : I) => A i j

Exchange order of double weighted sums.

def stdSimplex.pure {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] (i₀ : I) : ↑(stdSimplex 𝕜 I)

Point-mass simplex element at i₀.

Equations

• stdSimplex.pure i₀ = ⟨fun (i : I) => if i = i₀ then 1 else 0, ⋯⟩

@[simp]

theorem stdSimplex.pure_apply {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] (i₀ i : I) : ↑(pure i₀) i = if i = i₀ then 1 else 0

@[simp]

theorem wsum_pure_apply {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] (i₀ : I) (f : I → 𝕜) : wsum (stdSimplex.pure i₀) f = f i₀

Weighted sum at a point mass evaluates the chosen coordinate.

theorem wsum_pure {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] (i₀ : I) (f : I → 𝕜) : wsum ⟨fun (i : I) => if i = i₀ then 1 else 0, ⋯⟩ f = f i₀

Weighted sum with point mass at i₀ equals f i₀. Legacy form using the inline anonymous-structure point mass. New code should prefer stdSimplex.pure together with wsum_pure_apply.

Order characterization of wsum ranges

These lemmas turn pointwise bounds on f : I → 𝕜 into bounds on the weighted sum wsum x f over all simplex points x. They are the bridge that lets Loomis-style arguments reduce a quantification over mixed strategies to a quantification over pure responses.

theorem ge_iff_simplex_ge {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] {f : I → 𝕜} {v : 𝕜} : (∀ (i : I), v ≤ f i) ↔ ∀ (x : ↑(stdSimplex 𝕜 I)), v ≤ wsum x f

f ≥ v pointwise iff every simplex weighted sum is ≥ v.

theorem le_iff_simplex_le {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] {f : I → 𝕜} {v : 𝕜} : (∀ (i : I), f i ≤ v) ↔ ∀ (x : ↑(stdSimplex 𝕜 I)), wsum x f ≤ v

f ≤ v pointwise iff every simplex weighted sum is ≤ v.

Continuity (over ℝ)

For the simplified Loomis route we need that x ↦ wsum x f is continuous on stdSimplex ℝ I. The Mathlib instance stdSimplex.instCompactSpace_coe then hands us compactness "for free", which is the workhorse for existence of optimal mixed strategies.

theorem stdSimplex.continuous_coord {I : Type u_3} [Fintype I] (i : I) : Continuous fun (x : ↑(stdSimplex ℝ I)) => ↑x i

The i-th coordinate projection on stdSimplex ℝ I is continuous.

theorem wsum_continuous {I : Type u_3} [Fintype I] (f : I → ℝ) : Continuous fun (x : ↑(stdSimplex ℝ I)) => wsum x f

wsum (·) f is continuous on the standard simplex over ℝ.

Matrix-game expected payoff

expectedPayoffMatrix was previously in StrategicGame.Simplex. It is placed here because it is a purely arithmetic definition (bilinear evaluation on the simplex) with no strategic-game vocabulary.

def expectedPayoffMatrix {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} [Fintype I] {J : Type u_3} (A : I → J → 𝕜) [Fintype J] (x : ↑(stdSimplex 𝕜 I)) (y : ↑(stdSimplex 𝕜 J)) : 𝕜

Expected payoff in a matrix game A : I → J → 𝕜 under mixed strategies.

Equations

• expectedPayoffMatrix A x y = ⇑x ⬝ᵥ fun (i : I) => ⇑y ⬝ᵥ A i

theorem expectedPayoffMatrix_comm {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] {J : Type u_4} [Fintype J] (A : I → J → 𝕜) (x : ↑(stdSimplex 𝕜 I)) (y : ↑(stdSimplex 𝕜 J)) : expectedPayoffMatrix A x y = ⇑y ⬝ᵥ fun (j : J) => ⇑x ⬝ᵥ fun (i : I) => A i j

Expected payoff is commutative in the summation order.