Lean declarations

def MultipleParameterMechanism.welfareWithout EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG
Reported social welfare of all agents except `i`.
```
def welfareWithout (v : ∀ _ : I, Valuation A ℝ) (i : I) (a : A) : ℝ :=
  (Finset.univ.erase i).sum fun j => v j a
```

lemma MultipleParameterMechanism.socialWelfare_eq_value_add_welfareWithout EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

lemma socialWelfare_eq_value_add_welfareWithout
    (v : ∀ _ : I, Valuation A ℝ) (i : I) (a : A) :
    socialWelfare v a = v i a + welfareWithout v i a

lemma MultipleParameterMechanism.welfareWithout_le_socialWelfare EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

lemma welfareWithout_le_socialWelfare
    (v : ∀ _ : I, Valuation A ℝ)
    (hnonneg : ∀ i : I, ∀ a : A, 0 ≤ v i a)
    (i : I) (a : A) :
    welfareWithout v i a ≤ socialWelfare v a

lemma MultipleParameterMechanism.welfareWithout_le_socialWelfare_of_nonneg_i EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

lemma welfareWithout_le_socialWelfare_of_nonneg_i
    (v : ∀ _ : I, Valuation A ℝ)
    (i : I) (hi_nonneg : ∀ a : A, 0 ≤ v i a) (a : A) :
    welfareWithout v i a ≤ socialWelfare v a

lemma MultipleParameterMechanism.welfareWithout_update_self EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

lemma welfareWithout_update_self
    (v : ∀ _ : I, Valuation A ℝ) (i : I) (report : Valuation A ℝ) (a : A) :
    welfareWithout (Function.update v i report) i a = welfareWithout v i a

def MultipleParameterMechanism.maxWelfareWithout EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG
The maximum reported welfare of agents other than `i`.
```
noncomputable def maxWelfareWithout (v : ∀ _ : I, Valuation A ℝ) (i : I) : ℝ :=
  Finset.sup' Finset.univ Finset.univ_nonempty (welfareWithout v i)
```

lemma MultipleParameterMechanism.maxWelfareWithout_update_self EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

lemma maxWelfareWithout_update_self
    (v : ∀ _ : I, Valuation A ℝ) (i : I) (report : Valuation A ℝ) :
    maxWelfareWithout (Function.update v i report) i = maxWelfareWithout v i

lemma MultipleParameterMechanism.exists_withoutAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

lemma exists_withoutAllocation (v : ∀ _ : I, Valuation A ℝ) (i : I) :
    ∃ a : A, ∀ b : A, welfareWithout v i b ≤ welfareWithout v i a

def MultipleParameterMechanism.withoutAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG
A welfare-maximizing allocation for agents other than `i`.
```
noncomputable def withoutAllocation (v : ∀ _ : I, Valuation A ℝ) (i : I) : A :=
  Classical.choose (exists_withoutAllocation v i)
```

lemma MultipleParameterMechanism.withoutAllocation_isOptimal EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

lemma withoutAllocation_isOptimal (v : ∀ _ : I, Valuation A ℝ) (i : I) (a : A) :
    welfareWithout v i a ≤ welfareWithout v i (withoutAllocation v i)

Modules: EconCSLib.MechanismDesign.Auction.VCG

VCG Welfare Without Agent i

The "welfare-without-$i$" construction strips agent $i$'s own value contribution from the social welfare functional, retaining only the other agents' valuations at the same allocation: $$ W_{-i}(v, a) \;=\; \sum_{j \neq i} v_j(a). $$

Together with maxWelfareWithout v i := \max_a W_{-i}(v, a) it underpins the Clarke-pivot payment $p_i(v) = \max_a W_{-i}(v, a) - W_{-i}(v, a^*)$ (see [[mechanism_design.vcg.payment_identity]]).

Core identities and bounds

Decomposition (socialWelfare_eq_value_add_welfareWithout): $W(v, a) = v_i(a) + W_{-i}(v, a)$ for every agent $i$ and allocation $a$.
Monotonicity (welfareWithout_le_socialWelfare): $W_{-i}(v, a) \le W(v, a)$ when $v_i(a) \ge 0$, with a non-negativity variant welfareWithout_le_socialWelfare_of_nonneg_i.
Report independence (welfareWithout_update_self, maxWelfareWithout_update_self): replacing agent $i$'s reported valuation does not change $W_{-i}$ or its max — by construction, agent $i$'s report is the one term excluded from the sum. This is the strategic core of the Clarke pivot: agent $i$ cannot influence $\max_a W_{-i}$.
Existence and choice (exists_withoutAllocation, withoutAllocation, withoutAllocation_isOptimal): a welfare- without-$i$-maximising allocation always exists for finite $A$ and is selected noncomputably via choice.

References

[AGT Chapter 9, §9.3.4, Def 9.19] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Clarke-pivot payments.

VCG Welfare Without Agent i

Core identities and bounds

References

Used by

Also in