EconCSLib.SocialChoice.FairDivision.Indivisible.Valuation

Cardinal valuations for indivisible goods allocation.

Main definitions

• SocialChoice.FairDivision.Indivisible.Valuation N G — abstract valuation: assigns a real value to each agent-bundle pair
• SocialChoice.FairDivision.Indivisible.AdditiveValuation N G — additive valuation: determined by per-item weights
• SocialChoice.FairDivision.Indivisible.AdditiveValuation.toValuation — lifts an additive valuation to a Valuation

Namespace

All types are scoped under SocialChoice.FairDivision.Indivisible to avoid clashing with Mathlib.RingTheory.Valuation.Basic and to keep the public API under the canonical social-choice hierarchy.

Design

Valuation is real-valued. This keeps the public fair-division API aligned with the bundled cardinal interfaces and avoids carrying avoidable ordered-algebra typeclass parameters through every theorem statement.

AdditiveValuation specializes to the important case v_i(S) = Σ_{g ∈ S} w_i(g).

Note: Indivisible.Valuation N G maps bundles of goods — do not conflate with CoalitionalGame's characteristic function (coalitions of agents) or Mathlib's ring-theoretic Valuation (ring → ordered monoid).

References

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

Abstract valuation

structure SocialChoice.FairDivision.Indivisible.Valuation (N : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

An abstract valuation assigns a real value to each agent-bundle pair.

val i S is the value agent i assigns to bundle S.

Lives in namespace SocialChoice.FairDivision.Indivisible to avoid clash with Mathlib's ring-theoretic Valuation.

• val : N → Finset G → ℝ

  The valuation function: agent × bundle → value.

Additive valuation

structure SocialChoice.FairDivision.Indivisible.AdditiveValuation (N : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

An additive valuation is determined by per-item weights.

weight i g is the value agent i assigns to good g individually. The bundle value is v_i(S) = Σ_{g ∈ S} weight i g.

• weight : N → G → ℝ

  Per-item weight: agent × good → value.

def SocialChoice.FairDivision.Indivisible.AdditiveValuation.toValuation {N : Type u_1} {G : Type u_2} (w : AdditiveValuation N G) : Valuation N G

Lift an additive valuation to an abstract Valuation.

(w.toValuation).val i S = Σ_{g ∈ S} w.weight i g.

Equations

• w.toValuation = { val := fun (i : N) (S : Finset G) => ∑ g ∈ S, w.weight i g }

@[simp]

theorem SocialChoice.FairDivision.Indivisible.AdditiveValuation.toValuation_empty {N : Type u_1} {G : Type u_2} (w : AdditiveValuation N G) (i : N) : w.toValuation.val i ∅ = 0

The value of the empty bundle is zero for additive valuations.

theorem SocialChoice.FairDivision.Indivisible.AdditiveValuation.toValuation_union {N : Type u_1} {G : Type u_2} [DecidableEq G] (w : AdditiveValuation N G) (i : N) (S T : Finset G) (h : Disjoint S T) : w.toValuation.val i (S ∪ T) = w.toValuation.val i S + w.toValuation.val i T

Additive valuation of a union of disjoint bundles splits as a sum.

theorem SocialChoice.FairDivision.Indivisible.AdditiveValuation.toValuation_mono {N : Type u_1} {G : Type u_2} [DecidableEq G] (w : AdditiveValuation N G) (hnn : ∀ (i : N) (g : G), 0 ≤ w.weight i g) (i : N) {S T : Finset G} (h : T ⊆ S) : w.toValuation.val i T ≤ w.toValuation.val i S

Additive valuations with nonnegative weights are monotone: sub-bundles have no greater value than their supersets.