Lean declarations

def MultipleParameterMechanism.socialWelfare EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG
Reported social welfare of allocation `a` under a profile of valuations.
```
def socialWelfare (v : ∀ _ : I, Valuation A ℝ) (a : A) : ℝ :=
  ∑ i, v i a
```
def MultipleParameterMechanism.maxSocialWelfare EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG
The maximum reported social welfare over all allocations.
```
noncomputable def maxSocialWelfare (v : ∀ _ : I, Valuation A ℝ) : ℝ :=
  Finset.sup' Finset.univ Finset.univ_nonempty (socialWelfare v)
```
lemma MultipleParameterMechanism.exists_efficientAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG
There exists an allocation maximizing reported social welfare.
```
lemma exists_efficientAllocation (v : ∀ _ : I, Valuation A ℝ) :
    ∃ a : A, ∀ b : A, socialWelfare v b ≤ socialWelfare v a
```
def MultipleParameterMechanism.efficientAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG
A welfare-maximizing allocation, chosen noncomputably from finite `A`.
```
noncomputable def efficientAllocation (v : ∀ _ : I, Valuation A ℝ) : A :=
  Classical.choose (exists_efficientAllocation v)
```
lemma MultipleParameterMechanism.efficientAllocation_isOptimal EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG
The chosen VCG allocation maximizes reported social welfare.
```
lemma efficientAllocation_isOptimal (v : ∀ _ : I, Valuation A ℝ) (a : A) :
    socialWelfare v a ≤ socialWelfare v (efficientAllocation v)
```

Modules: EconCSLib.MechanismDesign.Auction.VCG

VCG Social Welfare

For a multiple-parameter mechanism with valuation profile $v : I \to (A \to \mathbb{R})$, the social welfare of allocation $a \in A$ is $$ W(v, a) \;=\; \sum_{i \in I} v_i(a). $$

maxSocialWelfare v is the supremum of $W(v, \cdot)$ over $A$; for a finite outcome set this maximum is attained, and efficientAllocation v is a chosen welfare-maximiser (noncomputable via choice). The correctness lemma efficientAllocation_isOptimal states $W(v, \mathrm{efficientAllocation}\ v) \ge W(v, a)$ for every $a \in A$.

This is the welfare-maximisation layer that the VCG mechanism's allocation rule and Clarke-pivot payment construction both build on:

The VCG allocation rule simply returns the efficient allocation.
The Clarke-pivot payment for agent $i$ subtracts the "welfare-without-$i$" max ([[mechanism_design.vcg.welfare_without]]) from the realised social welfare, giving the VCG identity ([[mechanism_design.vcg.payment_identity]]).

References

[AGT Chapter 9, §9.3.3, Def 9.16] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Welfare-maximising allocation rules for VCG.

VCG Social Welfare

References

Used by

Also in