Lean declarations

def CoalitionalGame.AreSymmetric EconCSLib @ cef01c7, EconCSLib.GameTheory.CoalitionalGame.ShapleyValue
Two players are symmetric if swapping them doesn't change any coalition's worth.
```
def AreSymmetric (i j : N) : Prop :=
  ∀ S : Finset N, i ∉ S → j ∉ S → G.v (insert i S) = G.v (insert j S)
```
def CoalitionalGame.IsNullPlayer EconCSLib @ cef01c7, EconCSLib.GameTheory.CoalitionalGame.ShapleyValue
A player is a null player if they add nothing to any coalition. [MSZ 18.6]
```
def IsNullPlayer (i : N) : Prop :=
  ∀ S : Finset N, i ∉ S → G.v (insert i S) = G.v S
```
def CoalitionalGame.SatisfiesEfficiency EconCSLib @ cef01c7, EconCSLib.GameTheory.CoalitionalGame.ShapleyValue
A solution concept `φ` satisfies efficiency if payoffs sum to `v(N)`. [MSZ 18.2]
```
def SatisfiesEfficiency (φ : CoalitionalGame N ℝ → N → ℝ) : Prop :=
  ∀ G : CoalitionalGame N ℝ, ∑ i : N, φ G i = G.v Finset.univ
```

def CoalitionalGame.SatisfiesSymmetry EconCSLib @ cef01c7, EconCSLib.GameTheory.CoalitionalGame.ShapleyValue

A solution concept satisfies symmetry. [MSZ 18.4]

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

def CoalitionalGame.SatisfiesNullPlayer EconCSLib @ cef01c7, EconCSLib.GameTheory.CoalitionalGame.ShapleyValue
A solution concept satisfies the null player property. [MSZ 18.7]
```
def SatisfiesNullPlayer (φ : CoalitionalGame N ℝ → N → ℝ) : Prop :=
  ∀ (G : CoalitionalGame N ℝ) (i : N), G.IsNullPlayer i → φ G i = 0
```

def CoalitionalGame.SatisfiesAdditivity EconCSLib @ cef01c7, EconCSLib.GameTheory.CoalitionalGame.ShapleyValue

A solution concept satisfies additivity. [MSZ 18.8]

def SatisfiesAdditivity (φ : CoalitionalGame N ℝ → N → ℝ) : Prop :=
  ∀ (G H : CoalitionalGame N ℝ) (i : N),
    φ ⟨fun S => G.v S + H.v S, by simp [G.empty_zero, H.empty_zero]⟩ i = φ G i + φ H i

Modules: EconCSLib.GameTheory.CoalitionalGame.ShapleyValue

Shapley Axioms

The Shapley-value characterization uses four axioms for a single-valued solution concept $\varphi$ assigning each game a payoff vector:

Efficiency: $\sum_{i \in N} \varphi_i(v)=v(N)$.
Symmetry: symmetric players receive equal payoffs.
Null player: a player who never changes any coalition's worth receives payoff zero.
Additivity: $\varphi(v+w)=\varphi(v)+\varphi(w)$.

Lean also defines the supporting predicates for symmetric players and null players. These are the hypotheses of Shapley's uniqueness theorem ([[game_theory.cooperative_game.shapley_uniqueness]]).

References

[MSZ Ch.18, Def 18.2, Def 18.4, Def 18.6, Def 18.8] Maschler, Solan, Zamir, Game Theory.

Shapley Axioms

References

Used by

Also in