• Reserve Second-Price Mechanism
• Vickrey Truth-Telling Is Dominant
• DSIC Predicate
• Weakly Dominant Strategy

• lemma Auction.ReserveSecondPrice.utility_nonneg EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

  Truthful bidding yields nonnegative utility.

  lemma utility_nonneg {b : I → U} {i : I} (htruth : b i = v i) :
      0 ≤ utility reserve v b i

• theorem Auction.ReserveSecondPrice.valuation_is_dominant EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

  Truthful bidding dominates any other bid in the reserve second-price auction.

  theorem valuation_is_dominant (reserve : U) (v : I → U) (i : I) (b : I → U) :
      utility reserve v b i ≤ utility reserve v (Function.update b i (v i)) i

• theorem Auction.ReserveSecondPrice.truthful_weakly_dominant EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

  Truthful bidding is a weakly dominant strategy in the reserve second-price auction.

  theorem truthful_weakly_dominant (reserve : U) (v : I → U) (i : I) :
      IsWeaklyDominant (game reserve v) i (v i)

• lemma Auction.ReserveSecondPrice.game_eq_toStrategicGame EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

  `game reserve v` equals the strategic game induced by `mechanism reserve`.

  lemma game_eq_toStrategicGame (reserve : U) (v : I → U) :
      game reserve v =
        (mechanism reserve).toStrategicGame
          (fun (w : Option I) (pay : I → U) (vals : I → U) (i : I) =>
            if w = some i then vals i - pay i else 0)
          v

• theorem Auction.ReserveSecondPrice.mechanism_isDSIC EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

  The reserve second-price auction satisfies dominant-strategy incentive compatibility.

  theorem mechanism_isDSIC (reserve : U) :
      (mechanism reserve).isDSIC
        (fun (w : Option I) (pay : I → U) (vals : I → U) (i : I) =>
          if w = some i then vals i - pay i else 0)

Modules: EconCSLib.MechanismDesign.Auction.ReserveVickrey