Theorem Shapley Uniqueness Theorem
theorem staged

Shapley Uniqueness Theorem

Theorem. The Shapley value is the unique single-valued solution concept that satisfies efficiency, symmetry, the null-player property, and additivity.

Proof

Sketch

The usual proof expands arbitrary games in a basis of unanimity games. The four axioms determine the value uniquely on unanimity games: players in the winning coalition receive equal shares and players outside it are null. Additivity then extends the determination to every game.

Lean Status

The Lean module defines the Shapley value and its axioms. Uniqueness remains a blueprint target with the unanimity-game proof route.

References

  • [MSZ Ch.18, Thm 18.13 and Thm 18.15] Maschler, Solan, Zamir, Game Theory.

Also in