EconCSLib.GameTheory.CoalitionalGame.ShapleyValue

The Shapley value: the unique single-valued solution concept satisfying efficiency, symmetry, the null player property, and additivity.

Main definitions

• marginalContribution — player i's marginal contribution given a permutation
• shapleyValue — the Shapley value of each player [MSZ 18.14]
• Axioms: Efficiency, Symmetry, NullPlayer, Additivity

References

• [MSZ] Chapter 18

Marginal contribution

def CoalitionalGame.marginalContrib {N : Type u_1} [DecidableEq N] (G : CoalitionalGame N ℝ) (i : N) (S : Finset N) : ℝ

The marginal contribution of player i to coalition S (where i ∉ S).

Equations

• G.marginalContrib i S = G.v (insert i S) - G.v S

def CoalitionalGame.AreSymmetric {N : Type u_1} [DecidableEq N] (G : CoalitionalGame N ℝ) (i j : N) : Prop

Two players are symmetric if swapping them doesn't change any coalition's worth.

Equations

• G.AreSymmetric i j = ∀ (S : Finset N), i ∉ S → j ∉ S → G.v (insert i S) = G.v (insert j S)

def CoalitionalGame.IsNullPlayer {N : Type u_1} [DecidableEq N] (G : CoalitionalGame N ℝ) (i : N) : Prop

A player is a null player if they add nothing to any coalition. [MSZ 18.6]

Equations

• G.IsNullPlayer i = ∀ (S : Finset N), i ∉ S → G.v (insert i S) = G.v S

Shapley value

noncomputable def CoalitionalGame.shapleyValue {N : Type u_1} [DecidableEq N] [Fintype N] (G : CoalitionalGame N ℝ) (i : N) : ℝ

The Shapley value of player i. [MSZ 18.14, 18.17]

φᵢ(v) = ∑_{S ⊆ N\{i}} |S|!(|N|-|S|-1)!/|N|! · (v(S∪{i}) - v(S))

Equations

• G.shapleyValue i = ∑ S : Finset N with i ∉ S, ↑S.card.factorial * ↑(Fintype.card N - S.card - 1).factorial / ↑(Fintype.card N).factorial * G.marginalContrib i S

Axioms for solution concepts

def CoalitionalGame.SatisfiesEfficiency {N : Type u_1} [DecidableEq N] [Fintype N] (φ : CoalitionalGame N ℝ → N → ℝ) : Prop

A solution concept φ satisfies efficiency if payoffs sum to v(N). [MSZ 18.2]

Equations

• CoalitionalGame.SatisfiesEfficiency φ = ∀ (G : CoalitionalGame N ℝ), ∑ i : N, φ G i = G.v Finset.univ

def CoalitionalGame.SatisfiesSymmetry {N : Type u_1} [DecidableEq N] (φ : CoalitionalGame N ℝ → N → ℝ) : Prop

A solution concept satisfies symmetry. [MSZ 18.4]

Equations

• CoalitionalGame.SatisfiesSymmetry φ = ∀ (G : CoalitionalGame N ℝ) (i j : N), G.AreSymmetric i j → φ G i = φ G j

def CoalitionalGame.SatisfiesNullPlayer {N : Type u_1} [DecidableEq N] (φ : CoalitionalGame N ℝ → N → ℝ) : Prop

A solution concept satisfies the null player property. [MSZ 18.7]

Equations

• CoalitionalGame.SatisfiesNullPlayer φ = ∀ (G : CoalitionalGame N ℝ) (i : N), G.IsNullPlayer i → φ G i = 0

def CoalitionalGame.SatisfiesAdditivity {N : Type u_1} [DecidableEq N] (φ : CoalitionalGame N ℝ → N → ℝ) : Prop

A solution concept satisfies additivity. [MSZ 18.8]

Equations

• CoalitionalGame.SatisfiesAdditivity φ = ∀ (G H : CoalitionalGame N ℝ) (i : N), φ { v := fun (S : Finset N) => G.v S + H.v S, empty_zero := ⋯ } i = φ G i + φ H i