Lean declarations

def MultipleParameterMechanism.vcgPayment EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

noncomputable def vcgPayment (v : ∀ _ : I, Valuation A ℝ) (i : I) : ℝ :=
  maxWelfareWithout v i - welfareWithout v i (efficientAllocation v)

def MultipleParameterMechanism.VCGMechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

noncomputable def VCGMechanism : MultipleParameterMechanism I A ℝ ℝ where
  allocationRule := efficientAllocation
  paymentRule := vcgPayment

def MultipleParameterMechanism.VCGTransferMechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

noncomputable def VCGTransferMechanism :
    MechanismWithTransfers I (fun _ => Valuation A ℝ) A ℝ where
  allocationRule := (VCGMechanism : MultipleParameterMechanism I A ℝ ℝ).allocationRule
  paymentRule := (VCGMechanism : MultipleParameterMechanism I A ℝ ℝ).paymentRule

Modules: EconCSLib.MechanismDesign.Auction.VCG

VCG Welfare And Payments

The VCG interface defines social welfare for reported valuation profiles, efficient allocations, welfare without a given agent, Clarke-pivot payments, and the induced direct and transfer mechanisms.

References

[AGT, Chapter 9, Section 9.3.3, Def. 9.16] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. VCG mechanisms and welfare-maximizing allocation rules.
[AGT, Chapter 9, Section 9.3.4, Def. 9.19] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Clarke-pivot payments.

Provenance

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

Used by

VCG Truthfulness And Individual Rationality

VCG Welfare And Payments

References

Provenance

Used by

Also in