EconCSLib.GameTheory.CoalitionalGame.Basic

Coalitional games with transferable utility (TU games).

Design

CoalitionalGame N U is parameterized by both the player type N and the utility type U. Assumptions are added at usage sites:

• [Fintype N] where grand coalition Finset.univ is needed (e.g., IsEfficient)
• U = ℝ only where real arithmetic is genuinely required (Shapley value, Bondareva-Shapley)

The structure requires [AddZeroClass U] (not just [Zero U]) to ensure a single canonical Zero instance across the namespace, avoiding typeclass diamond issues when theorems add [AddCommMonoid U] or stronger constraints.

Main definitions

• CoalitionalGame — (N; v) where v : Finset N → U with v ∅ = 0
• PayoffVector — payoff assignment N → U
• coalitionPayoff — total payoff of a coalition
• IsEfficient, IsIndividuallyRational, IsImputation
• IsSuperadditive, IsMonotonic, IsConvex, IsSimple, IsAdditive

References

• [MSZ] Maschler, Solan, Zamir, Game Theory, Chapter 16

Coalitional game structure

structure CoalitionalGame (N : Type u_1) (U : Type u_2) [DecidableEq N] [AddZeroClass U] : Type (max u_1 u_2)

A coalitional game with transferable utility. N is the player type; U is the utility type. v assigns a worth to each coalition, with the empty coalition worth zero. [MSZ 16.1]

No finiteness or concrete number-system assumptions are baked in. Specialize U to ℝ only where real arithmetic is genuinely required.

• v : Finset N → U

  The characteristic function: worth of each coalition.

• empty_zero : self.v ∅ = 0

  The empty coalition is worth zero.

Payoff vectors

@[reducible, inline]

abbrev CoalitionalGame.PayoffVector (N : Type u_3) (U : Type u_4) : Type (max u_3 u_4)

A payoff vector: an assignment of payoffs to players.

Equations

• CoalitionalGame.PayoffVector N U = (N → U)

def CoalitionalGame.coalitionPayoff {N : Type u_1} {U : Type u_2} [AddCommMonoid U] (x : PayoffVector N U) (S : Finset N) : U

The total payoff of a coalition under a payoff vector. Requires [AddCommMonoid U] for the finite sum.

Equations

• CoalitionalGame.coalitionPayoff x S = ∑ i ∈ S, x i

Imputations

def CoalitionalGame.IsEfficient {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [Fintype N] [AddCommMonoid U] (x : PayoffVector N U) : Prop

A payoff vector is efficient if it distributes exactly v(N). [MSZ 16.1] Requires [Fintype N] and [AddCommMonoid U].

Equations

• G.IsEfficient x = (CoalitionalGame.coalitionPayoff x Finset.univ = G.v Finset.univ)

def CoalitionalGame.IsIndividuallyRational {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [LE U] (x : PayoffVector N U) : Prop

A payoff vector is individually rational if each player gets at least their singleton worth. Requires [LE U].

Equations

• G.IsIndividuallyRational x = ∀ (i : N), x i ≥ G.v {i}

def CoalitionalGame.IsImputation {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [Fintype N] [AddCommMonoid U] [LE U] (x : PayoffVector N U) : Prop

An imputation is an efficient and individually rational payoff vector. [MSZ 17.1]

Equations

• G.IsImputation x = (G.IsEfficient x ∧ G.IsIndividuallyRational x)

Game properties

def CoalitionalGame.IsSuperadditive {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [LE U] : Prop

A game is superadditive if the worth of the union of disjoint coalitions is at least the sum of their worths. [MSZ 16.8] Requires [LE U] (addition comes from the [AddZeroClass U] section variable).

Equations

• G.IsSuperadditive = ∀ (S T : Finset N), Disjoint S T → G.v (S ∪ T) ≥ G.v S + G.v T

def CoalitionalGame.IsMonotonic {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [LE U] : Prop

A game is monotonic if larger coalitions are worth at least as much. [MSZ 16.10] Requires [LE U].

Equations

• G.IsMonotonic = ∀ (S T : Finset N), S ⊆ T → G.v S ≤ G.v T

def CoalitionalGame.IsConvex {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [LE U] : Prop

A game is convex if it satisfies the supermodularity condition. [MSZ 17.51] Requires [LE U] (addition comes from [AddZeroClass U]).

Equations

• G.IsConvex = ∀ (S T : Finset N), G.v (S ∪ T) + G.v (S ∩ T) ≥ G.v S + G.v T

def CoalitionalGame.IsSimple {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [Fintype N] [One U] : Prop

A game is simple if every coalition's worth is 0 or 1, and the grand coalition's worth is 1. [MSZ 16.2] Requires [Fintype N] and [One U].

Equations

• G.IsSimple = ((∀ (S : Finset N), G.v S = 0 ∨ G.v S = 1) ∧ G.v Finset.univ = 1)

def CoalitionalGame.IsWinning {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [One U] (S : Finset N) : Prop

A coalition is winning in a simple game if its worth is 1. Requires [One U].

Equations

• G.IsWinning S = (G.v S = 1)

def CoalitionalGame.IsAdditive {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [AddCommMonoid U] : Prop

A game is additive if v(S) = ∑_{i ∈ S} v({i}). [MSZ 17.41] Requires [AddCommMonoid U].

Equations

• G.IsAdditive = ∀ (S : Finset N), G.v S = ∑ i ∈ S, G.v {i}

Basic theorems

theorem CoalitionalGame.IsConvex.isSuperadditive {N : Type u_1} [DecidableEq N] {U : Type u_2} [AddZeroClass U] (G : CoalitionalGame N U) [LE U] (hconv : G.IsConvex) : G.IsSuperadditive

Convexity implies superadditivity. The [LE U] constraint is all that's needed beyond the section's [AddZeroClass U].