Shapley value

StructureCooperative game with transferable utility#✓fully proved

Given a set \(N\) of players, a cooperative game on \(N\) is a function \(v\) that assigns to every coalition \(S \subseteq N\) a real number \(v(S)\), the worth of \(S\), such that \(v(\emptyset) = 0\).

@[ext]
structure CoopGame (Player : Type*) where
  charFun : Set Player → ℝ
  empty : charFun ∅ = 0

Used by 7

Used byBondareva–Shapley theorem · Balanced cooperative game · Core allocation · Efficient value · Null player · Symmetric value · Null player axiom

DefinitionNull player#✓fully proved

Let \(v\) be a cooperative game on a finite set \(N\) of players. A player \(i \in N\) is a null player of \(v\) if \(v(S \cup \{i\}) = v(S)\) for every coalition \(S \subseteq N\) with \(i \notin S\).

def IsNullPlayer (v : CoopGame Player) (i : Player) : Prop :=
  ∀ S : Set Player, i ∉ S → v.charFun (insert i S) = v.charFun S

Uses 1 · Used by 1

Statement usesCooperative game with transferable utility

Used byNull player axiom

DefinitionEfficient value#✓fully proved

Let \(N\) be a finite set of players and \(\varphi\) an \(\mathbb{R}\)-linear map from cooperative games on \(N\) (added and scaled pointwise) to payoff vectors in \(\mathbb{R}^N\). Then \(\varphi\) is efficient if for every game \(v\) the payoffs add up to the worth of the grand coalition: \(\sum_{i \in N} \varphi(v)_i = v(N)\).

def IsEfficient (φ : CoopGame Player →ₗ[ℝ] (Player → ℝ)) : Prop :=
  ∀ v : CoopGame Player, ∑ i : Player, φ v i = v.charFun Set.univ

Uses 1

Statement usesCooperative game with transferable utility

DefinitionSymmetric value#✓fully proved

Let \(N\) be a finite set of players and \(\varphi\) an \(\mathbb{R}\)-linear map from cooperative games on \(N\) (added and scaled pointwise) to payoff vectors in \(\mathbb{R}^N\). Then \(\varphi\) is symmetric if for every game \(v\) and every permutation \(\sigma\) of \(N\) with \(v(\sigma(S)) = v(S)\) for all coalitions \(S \subseteq N\), every player \(i\) satisfies \(\varphi(v)_{\sigma(i)} = \varphi(v)_i\).

def IsSymmetric (φ : CoopGame Player →ₗ[ℝ] (Player → ℝ)) : Prop :=
  ∀ (σ : Equiv.Perm Player) (v : CoopGame Player),
    (∀ S : Set Player, v.charFun (σ '' S) = v.charFun S) →
    ∀ i : Player, φ v (σ i) = φ v i

Uses 1

Statement usesCooperative game with transferable utility

DefinitionNull player axiom#✓fully proved

Let \(N\) be a finite set of players and \(\varphi\) an \(\mathbb{R}\)-linear map from cooperative games on \(N\) (added and scaled pointwise) to payoff vectors in \(\mathbb{R}^N\). Then \(\varphi\) satisfies the null player axiom if \(\varphi(v)_i = 0\) for every game \(v\) and every null player \(i\) of \(v\).

def SatisfiesNullPlayerAxiom (φ : CoopGame Player →ₗ[ℝ] (Player → ℝ)) : Prop :=
  ∀ (v : CoopGame Player) (i : Player), IsNullPlayer v i → φ v i = 0

Uses 2

Statement usesCooperative game with transferable utility · Null player

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.