EconCSLib.SocialChoice.FairDivision.Indivisible.Basic

Foundational definitions for indivisible goods allocation.

Main definitions

• Allocation N G — a function assigning each agent a bundle (Finset of goods)
• IsAllocation — predicate that an allocation partitions all goods

Design

Allocation is a plain function type alias; the partition predicate IsAllocation is kept separate so that algorithms can manipulate raw allocations before proving correctness. [Fintype N] and [DecidableEq G] are required only by IsAllocation (where Finset.univ and Finset.biUnion need them), not by the type alias itself.

References

• Nisan et al., Algorithmic Game Theory, Chapter 11

Allocation type

def SocialChoice.FairDivision.Indivisible.Allocation (N : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

An allocation assigns each agent i : N a bundle (a finite subset of goods G).

This is a plain function type alias. The partition property is stated separately in IsAllocation, keeping structure and assumptions decoupled.

Equations

• SocialChoice.FairDivision.Indivisible.Allocation N G = (N → Finset G)

Complete allocation (partition)

structure SocialChoice.FairDivision.Indivisible.IsAllocation {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] (allGoods : Finset G) (A : Allocation N G) : Prop

A complete allocation partitions all goods among agents.

• disjoint: distinct agents receive disjoint bundles.
• complete: every good in allGoods is allocated to some agent.

[Fintype N] is required for Finset.univ in the completeness condition. [DecidableEq G] is required for Finset.biUnion and Disjoint.

[AGT Ch.11]

• disjoint (i j : N) : i ≠ j → Disjoint (A i) (A j)

  Distinct agents receive disjoint bundles.

• complete : allGoods = Finset.univ.biUnion A

  Every good in allGoods is allocated to some agent.

theorem SocialChoice.FairDivision.Indivisible.IsAllocation.mem_biUnion {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq G] {allGoods : Finset G} {A : Allocation N G} (h : IsAllocation allGoods A) (g : G) (hg : g ∈ allGoods) : ∃ (i : N), g ∈ A i

Every good in allGoods belongs to the bundle of some agent.