Lean declarations

structure MultipleParameterMechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

structure MultipleParameterMechanism
    (I : Type*) (A : Type*) (V : Type*) (P : Type*)
    extends MechanismWithTransfers I (fun _ => A → V) A P

namespace MultipleParameterMechanism

variable {I A V : Type*}

/-- The valuation/type space of an agent in a multiple-parameter mechanism. -/

abbrev MultipleParameterMechanism.Valuation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer
The valuation/type space of an agent in a multiple-parameter mechanism.
```
abbrev Valuation (A : Type*) (V : Type*) := A → V
```
def MultipleParameterMechanism.valueOfAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer
```
def valueOfAllocation
    (a : A) (types : ∀ _ : I, Valuation A V) (i : I) : V :=
  types i a
```

Modules: EconCSLib.MechanismDesign.Auction.Transfer

Multiple-Parameter Transfer Layer

In a multiple-parameter mechanism, each agent reports a valuation function over the allocation space. This is the abstract transfer-mechanism layer used by VCG-style constructions.

References

[AGT, Chapter 9, Sections 9.3.2-9.3.3] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Multi-parameter valuation functions, outcomes, and transfer mechanisms.
[AGT, Chapter 12, Section 12.3] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Multidimensional mechanism-design domains in combinatorial-auction settings.

Provenance

Migrated from EconCSLib pull request 27, old blueprint label def:md_multiple_parameter_interface in blueprint/src/content.tex.

Multiple-Parameter Transfer Layer

References

Provenance

Used by

Also in