• Basic Auction Formats
• Ordered-Bid Utilities
• Mechanisms With Transfers

• def Auction.SecondPrice.winner EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  noncomputable def winner (b : I → U) : I := Auction.argmaxBid b

• def Auction.SecondPrice.secondPrice EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  The second price: the highest bid among all bidders other than the winner.

  noncomputable def secondPrice (b : I → U) : U := Auction.maxBidExcluding b (winner b)

• lemma Auction.SecondPrice.secondPrice_le_bid_winner EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  The winner's bid is at least the second price.

  lemma secondPrice_le_bid_winner (b : I → U) : secondPrice b ≤ b (winner b)

• def Auction.SecondPrice.utility EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  noncomputable def utility (v b : I → U) (i : I) : U :=
    if i = winner b then v i - secondPrice b else 0

• lemma Auction.SecondPrice.utility_winner EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  If `i` is the winner, utility is `v i − secondPrice b`.

  lemma utility_winner {b : I → U} {i : I} (h : i = winner b) :
      utility v b i = v i - secondPrice b

• lemma Auction.SecondPrice.utility_loser EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  If `i` is not the winner, utility is `0`.

  lemma utility_loser {b : I → U} {i : I} (h : i ≠ winner b) :
      utility v b i = 0

• lemma Auction.SecondPrice.utility_nonneg EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  Truthful bidding yields nonneg utility.

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

• def Auction.SecondPrice.mechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  noncomputable def mechanism : MechanismWithTransfers I (fun _ => U) I U where
    allocationRule b := winner b
    paymentRule b i := if i = winner b then secondPrice b else 0

• def Auction.SecondPrice.game EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

  noncomputable def game (v : I → U) : StrategicGame I U where
    strategy := fun _ => U
    payoff b i := utility v b i

• lemma Auction.SecondPrice.game_eq_toStrategicGame EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Vickrey

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

Modules: EconCSLib.MechanismDesign.Auction.Vickrey