Shapley Value

The Shapley value assigns to each player their average marginal contribution over all possible orders in which the grand coalition can form. Equivalently, $$ \operatorname{Sh}_i(v) = \sum_{S \subseteq N\setminus\{i\}} \frac{|S|!(|N|-|S|-1)!}{|N|!} \bigl(v(S \cup \{i\})-v(S)\bigr). $$

The factorial coefficient is the probability that exactly the players in $S$ precede $i$ in a uniformly random ordering of $N$.

Lean Status

Lean defines this formula as CoalitionalGame.shapleyValue. The main properties of the formula are separate theorem nodes: efficiency, uniqueness, and convex-core membership.

References

• [MSZ Ch.18, Def 18.14 and Thm 18.17] Maschler, Solan, Zamir, Game Theory.