EconCSLib.MechanismDesign.Auction.VCG

Multiple-parameter mechanisms for VCG-style mechanism design.

This file builds the VCG mechanism as a specialization of the multiple-parameter transfer-mechanism layer from MechanismDesign.Auction.Transfer.

The transfer layer keeps utility external to the mechanism. A mechanism stores only an allocation rule and a payment rule; quasi-linear DSIC and ex-post IR are then stated through MechanismWithTransfers.isQuasiLinearDSIC and MechanismWithTransfers.isQuasiLinearExPostIR.

In the multiple-parameter VCG setting, agent i's type/report is a valuation function A → ℝ on the allocation space. The VCG allocation maximizes reported social welfare, and the Clarke-pivot payment charges each agent the externality imposed on the other agents.

Structure hierarchy

MechanismWithTransfers I (fun _ => A → ℝ) A ℝ     -- valuation reports over A
  └─ MultipleParameterMechanism I A ℝ ℝ           -- named multiple-parameter layer
       └─ VCGMechanism                            -- efficient allocation + Clarke payments

VCGTransferMechanism                              -- same rule viewed as MechanismWithTransfers

def MultipleParameterMechanism.socialWelfare {I : Type u_1} {A : Type u_2} [Fintype I] (v : I → Valuation A ℝ) (a : A) : ℝ

Reported social welfare of allocation a under a profile of valuations.

Equations

• MultipleParameterMechanism.socialWelfare v a = ∑ i : I, v i a

noncomputable def MultipleParameterMechanism.maxSocialWelfare {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] (v : I → Valuation A ℝ) : ℝ

The maximum reported social welfare over all allocations.

Equations

• MultipleParameterMechanism.maxSocialWelfare v = Finset.univ.sup' ⋯ (MultipleParameterMechanism.socialWelfare v)

theorem MultipleParameterMechanism.exists_efficientAllocation {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] (v : I → Valuation A ℝ) : ∃ (a : A), ∀ (b : A), socialWelfare v b ≤ socialWelfare v a

There exists an allocation maximizing reported social welfare.

noncomputable def MultipleParameterMechanism.efficientAllocation {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] (v : I → Valuation A ℝ) : A

A welfare-maximizing allocation, chosen noncomputably from finite A.

Equations

• MultipleParameterMechanism.efficientAllocation v = Classical.choose ⋯

theorem MultipleParameterMechanism.efficientAllocation_isOptimal {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] (v : I → Valuation A ℝ) (a : A) : socialWelfare v a ≤ socialWelfare v (efficientAllocation v)

The chosen VCG allocation maximizes reported social welfare.

def MultipleParameterMechanism.welfareWithout {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) (a : A) : ℝ

Reported social welfare of all agents except i.

Equations

• MultipleParameterMechanism.welfareWithout v i a = ∑ j ∈ Finset.univ.erase i, v j a

theorem MultipleParameterMechanism.socialWelfare_eq_value_add_welfareWithout {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) (a : A) : socialWelfare v a = v i a + welfareWithout v i a

Social welfare decomposes into agent i's value plus the welfare of the other agents.

theorem MultipleParameterMechanism.welfareWithout_le_socialWelfare {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] (v : I → Valuation A ℝ) (hnonneg : ∀ (i : I) (a : A), 0 ≤ v i a) (i : I) (a : A) : welfareWithout v i a ≤ socialWelfare v a

If all valuations are nonnegative, then the welfare of agents other than i is bounded by total social welfare.

theorem MultipleParameterMechanism.welfareWithout_le_socialWelfare_of_nonneg_i {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) (hi_nonneg : ∀ (a : A), 0 ≤ v i a) (a : A) : welfareWithout v i a ≤ socialWelfare v a

If agent i's valuation is nonnegative, then the welfare of agents other than i is bounded by total social welfare.

theorem MultipleParameterMechanism.welfareWithout_update_self {I : Type u_1} {A : Type u_2} [Fintype I] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) (report : Valuation A ℝ) (a : A) : welfareWithout (Function.update v i report) i a = welfareWithout v i a

Changing agent i's report does not change the welfare of agents other than i.

noncomputable def MultipleParameterMechanism.maxWelfareWithout {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) : ℝ

The maximum reported welfare of agents other than i.

Equations

• MultipleParameterMechanism.maxWelfareWithout v i = Finset.univ.sup' ⋯ (MultipleParameterMechanism.welfareWithout v i)

theorem MultipleParameterMechanism.maxWelfareWithout_update_self {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) (report : Valuation A ℝ) : maxWelfareWithout (Function.update v i report) i = maxWelfareWithout v i

Changing agent i's report does not change the maximum welfare achievable by the other agents.

theorem MultipleParameterMechanism.exists_withoutAllocation {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) : ∃ (a : A), ∀ (b : A), welfareWithout v i b ≤ welfareWithout v i a

There exists an allocation maximizing the reported welfare of agents other than i.

noncomputable def MultipleParameterMechanism.withoutAllocation {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) : A

A welfare-maximizing allocation for agents other than i.

Equations

• MultipleParameterMechanism.withoutAllocation v i = Classical.choose ⋯

theorem MultipleParameterMechanism.withoutAllocation_isOptimal {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) (a : A) : welfareWithout v i a ≤ welfareWithout v i (withoutAllocation v i)

The chosen allocation without agent i maximizes the reported welfare of the other agents.

noncomputable def MultipleParameterMechanism.vcgPayment {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (v : I → Valuation A ℝ) (i : I) : ℝ

The Clarke-pivot VCG payment charged to agent i: the best welfare that the other agents could get without i, minus the other agents' welfare at the efficient allocation chosen from all reports.

Equations

• MultipleParameterMechanism.vcgPayment v i = MultipleParameterMechanism.maxWelfareWithout v i - MultipleParameterMechanism.welfareWithout v i (MultipleParameterMechanism.efficientAllocation v)

noncomputable def MultipleParameterMechanism.VCGMechanism {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] : MultipleParameterMechanism I A ℝ ℝ

The finite-allocation VCG mechanism induced by welfare maximization and Clarke-pivot payments.

Equations

• MultipleParameterMechanism.VCGMechanism = { allocationRule := MultipleParameterMechanism.efficientAllocation, paymentRule := MultipleParameterMechanism.vcgPayment }

noncomputable def MultipleParameterMechanism.VCGTransferMechanism {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] : MechanismWithTransfers I (fun (x : I) => Valuation A ℝ) A ℝ

The underlying transfer mechanism of VCGMechanism.

This is the object to which the generic definitions in Transfer.lean, such as isQuasiLinearDSIC and isQuasiLinearExPostIR, are applied.

Equations

• MultipleParameterMechanism.VCGTransferMechanism = MultipleParameterMechanism.VCGMechanism.toMechanismWithTransfers

theorem MultipleParameterMechanism.VCGMechanism_quasiLinearUtility_eq_socialWelfare_sub_maxWelfareWithout {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (reports trueTypes : I → Valuation A ℝ) (i : I) : VCGTransferMechanism.quasiLinearUtility valueOfAllocation id id reports trueTypes i = socialWelfare (Function.update reports i (trueTypes i)) (efficientAllocation reports) - maxWelfareWithout reports i

VCG utility can be rewritten as total welfare under the profile that uses agent i's true valuation and keeps all other reports fixed, minus the maximal welfare achievable by the other agents alone.

theorem MultipleParameterMechanism.VCGMechanism_truthful_quasiLinearUtility_nonneg {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (v : I → Valuation A ℝ) (hnonneg : ∀ (i : I) (a : A), 0 ≤ v i a) (i : I) (r : I → Valuation A ℝ) : 0 ≤ VCGTransferMechanism.quasiLinearUtility valueOfAllocation id id (Function.update r i (v i)) v i

If agent i reports truthfully in the VCG mechanism, then their quasi-linear utility is nonnegative against arbitrary reports by the other agents, assuming i's true valuation is nonnegative.

theorem MultipleParameterMechanism.VCGMechanism_truthful_profile_quasiLinearUtility_nonneg {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (v : I → Valuation A ℝ) (hnonneg : ∀ (i : I) (a : A), 0 ≤ v i a) (i : I) : 0 ≤ VCGTransferMechanism.quasiLinearUtility valueOfAllocation id id v v i

The same nonnegative-utility result for the fully truthful report profile.

theorem MultipleParameterMechanism.VCGMechanism_isExPostIR_of_all_nonnegative {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] (hnonneg : ∀ (v : I → Valuation A ℝ) (i : I) (a : A), 0 ≤ v i a) : VCGTransferMechanism.isQuasiLinearExPostIR valueOfAllocation id id

VCG satisfies the MechanismWithTransfers.isExPostIR predicate under the ambient assumption that every valuation in the unrestricted type space is nonnegative. For concrete domains, this assumption is usually enforced by choosing a nonnegative valuation subtype.

theorem MultipleParameterMechanism.VCGMechanism_isDSIC {I : Type u_1} {A : Type u_2} [Fintype I] [Fintype A] [Nonempty A] [DecidableEq I] : VCGTransferMechanism.isQuasiLinearDSIC valueOfAllocation id id

The finite-allocation VCG mechanism is dominant-strategy incentive compatible for quasi-linear utilities.

The final arguments id id instantiate the two conversion maps in MechanismWithTransfers.isQuasiLinearDSIC:

• valueToUtility : ℝ → ℝ, converting valuation values to utilities;
• paymentToUtility : ℝ → ℝ, converting payments to utilities.

For VCG, values, payments, and utilities all live in ℝ, so both conversions are the identity map.