Theorem Truthfulness From DSIC

✓ theorem proved

#

Lean declarations

theorem Mechanism.IsDSIC.truthful_isNash EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBasic
If a mechanism is DSIC, then truthful reporting is a Nash equilibrium.
```
theorem IsDSIC.truthful_isNash [Preorder U]
    (hdsic : M.IsDSIC u) (v : ∀ i, T i) :
    IsNashEquilibrium (M.toStrategicGame u v) v
```

Modules: EconCSLib.MechanismDesign.Auction.MechBasic

Truthfulness From DSIC

In a direct mechanism, if truthful reporting is dominant-strategy incentive compatible, then the truthful reporting profile is a Nash equilibrium of the induced strategic game.

References

[AGT, Chapter 9, Def. 9.15] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Truthfulness as dominant-strategy incentive compatibility.
[AGT, Chapter 9, Prop. 9.25] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Truthful direct mechanisms obtained from equilibrium behavior in induced mechanisms.

Provenance

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

Also in