EconCSLib.GameTheory.CoalitionalGame.Core

The core of a coalitional game: the set of imputations that no coalition can improve upon.

Main definitions

• Core — the core of a coalitional game [MSZ 17.2]
• IsBalanced — balanced collection of coalitions [MSZ 17.11]

Main results

• core_subset_imputations — every core element is an imputation ✓

References

• [MSZ] Chapter 17

Core definition

def CoalitionalGame.Core {N : Type u_1} [DecidableEq N] [Fintype N] (G : CoalitionalGame N ℝ) : Set (PayoffVector N ℝ)

The core of a coalitional game: payoff vectors where no coalition can improve upon its allocation. [MSZ 17.2]

An element x of the core satisfies:

• Efficiency: ∑ᵢ xᵢ = v(N)
• Coalition stability: ∑_{i ∈ S} xᵢ ≥ v(S) for all S

Equations

• G.Core = {x : CoalitionalGame.PayoffVector N ℝ | G.IsEfficient x ∧ ∀ (S : Finset N), CoalitionalGame.coalitionPayoff x S ≥ G.v S}

theorem CoalitionalGame.core_subset_imputations {N : Type u_1} [DecidableEq N] [Fintype N] (G : CoalitionalGame N ℝ) : G.Core ⊆ {x : PayoffVector N ℝ | G.IsImputation x}

Every element of the core is an imputation.

Balanced collections

def CoalitionalGame.IsBalanced {N : Type u_1} [DecidableEq N] (𝒟 : Finset (Finset N)) : Prop

A collection of coalitions is balanced if there exist positive weights summing to the characteristic vector of N. [MSZ 17.11]

Equations

• CoalitionalGame.IsBalanced 𝒟 = ∃ (δ : Finset N → ℝ), (∀ S ∈ 𝒟, δ S > 0) ∧ ∀ (i : N), ∑ S ∈ 𝒟 with i ∈ S, δ S = 1

def CoalitionalGame.IsBalancedGame {N : Type u_1} [DecidableEq N] [Fintype N] (G : CoalitionalGame N ℝ) : Prop

A game is balanced if every balanced collection satisfies the superadditivity-like condition. [MSZ 17.14 premise]

Equations

• G.IsBalancedGame = ∀ (𝒟 : Finset (Finset N)) (δ : Finset N → ℝ), (∀ S ∈ 𝒟, δ S > 0) → (∀ (i : N), ∑ S ∈ 𝒟 with i ∈ S, δ S = 1) → ∑ S ∈ 𝒟, δ S * G.v S ≤ G.v Finset.univ