Lean declarations

theorem MultipleParameterMechanism.VCGMechanism_truthful_quasiLinearUtility_nonneg EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

theorem VCGMechanism_truthful_quasiLinearUtility_nonneg
    (v : ∀ _ : I, Valuation A ℝ)
    (hnonneg : ∀ i : I, ∀ a : A, 0 ≤ v i a)
    (i : I) (r : ∀ _ : I, Valuation A ℝ) :
    0 ≤ MechanismWithTransfers.quasiLinearUtility
      VCGTransferMechanism valueOfAllocation id id (Function.update r i (v i)) v i

theorem MultipleParameterMechanism.VCGMechanism_truthful_profile_quasiLinearUtility_nonneg EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

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

theorem VCGMechanism_truthful_profile_quasiLinearUtility_nonneg
    (v : ∀ _ : I, Valuation A ℝ)
    (hnonneg : ∀ i : I, ∀ a : A, 0 ≤ v i a)
    (i : I) :
    0 ≤ MechanismWithTransfers.quasiLinearUtility
      VCGTransferMechanism valueOfAllocation id id v v i

theorem MultipleParameterMechanism.VCGMechanism_isExPostIR_of_all_nonnegative EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

theorem VCGMechanism_isExPostIR_of_all_nonnegative
    (hnonneg :
      ∀ v : (∀ _ : I, Valuation A ℝ), ∀ i : I, ∀ a : A, 0 ≤ v i a) :
    MechanismWithTransfers.isQuasiLinearExPostIR
      (M := (VCGTransferMechanism :
        MechanismWithTransfers I (fun _ => Valuation A ℝ) A ℝ))
      valueOfAllocation id id

theorem MultipleParameterMechanism.VCGMechanism_isDSIC EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.VCG

theorem VCGMechanism_isDSIC :
    MechanismWithTransfers.isQuasiLinearDSIC
      (M := (VCGTransferMechanism :
        MechanismWithTransfers I (fun _ => Valuation A ℝ) A ℝ))
      valueOfAllocation id id

Modules: EconCSLib.MechanismDesign.Auction.VCG

VCG Truthfulness And Individual Rationality

The VCG mechanism is dominant-strategy incentive compatible (DSIC) unconditionally for quasi-linear utilities, and — under the additional nonnegativity hypothesis on every valuation in the type space — gives every agent nonnegative truthful quasi-linear utility, which yields ex-post individual rationality.

That is: DSIC needs no sign assumption; IR and the nonnegative-utility bound require nonnegative valuations.

References

[AGT, Chapter 9, Thm. 9.17] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. VCG mechanisms are incentive compatible.
[AGT, Chapter 9, Lem. 9.20] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Clarke pivot payments and individual rationality under nonnegative valuations.

Provenance

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

VCG Truthfulness And Individual Rationality

References

Provenance

Also in