Theorem Shapley Value Is Efficient
theorem staged

Shapley Value Is Efficient

Theorem. The Shapley value distributes the worth of the grand coalition: $$ \sum_{i \in N} \operatorname{Sh}_i(v)=v(N). $$

Proof

Sketch

Expand the Shapley formula and exchange the sums over players and predecessor coalitions. Each coalition marginal contribution appears with the number of orders in which it is the relevant predecessor set. The resulting telescoping over permutations leaves exactly $v(N)-v(\varnothing)=v(N)$.

Lean Status

The Lean module defines the Shapley value. Efficiency remains a blueprint target with a combinatorial proof route.

References

  • [MSZ Ch.18, Thm 18.18] Maschler, Solan, Zamir, Game Theory.

Also in