EconCSLib.MechanismDesign.Auction.Vickrey

Second-price (Vickrey) auction: the winner pays the second-highest bid.

Position in the hierarchy

MechanismWithTransfers I (fun _ => U) I U        -- scalar bids, winner allocation, scalar payments
  └─ SecondPrice.mechanism                       -- winner + second-price payment rule
       └─ SecondPrice.game v                     -- induced StrategicGame at true values v

The auction is formalized as a MechanismWithTransfers (from MechanismDesign.Auction.Transfer). DSIC is stated as mechanism.isDSIC auctionUtility, inheriting the general definition.

Typeclass design

The bid/utility type U requires (following Mathlib's unbundled style):

• [AddCommGroup U] — subtraction for utility = valuation − payment
• [LinearOrder U] — comparing bids, selecting winner
• [IsOrderedAddMonoid U] — compatibility: a ≤ b → a + c ≤ b + c, sub_nonneg, etc.

This is the unbundled equivalent of the former LinearOrderedAddCommGroup. No multiplication is needed — Vickrey payoff is v_i − price, pure additive. Satisfied by ℤ, ℚ, ℝ, and any LinearOrderedField.

Main definitions

• Auction.SecondPrice.winner — the highest bidder (uses Auction.argmaxBid from Basic)
• Auction.SecondPrice.secondPrice — highest bid excluding the winner
• Auction.SecondPrice.mechanism — second-price auction as a MechanismWithTransfers
• Auction.SecondPrice.utility — concrete utility formula (winner gets v i − secondPrice, losers get 0)
• Auction.SecondPrice.game — second-price auction as a StrategicGame, equal to mechanism.toStrategicGame (fun w pay v i => if i = w then v i - pay i else 0) v

Main results

• Auction.SecondPrice.game_eq_toStrategicGame — game v equals the mechanism-induced game
• Auction.SecondPrice.mechanism_isDSIC — DSIC at the MechanismWithTransfers level
• Auction.SecondPrice.utility_nonneg — truthful bidding yields nonneg utility
• Auction.SecondPrice.valuation_is_dominant — truthful bidding dominates any other bid
• Auction.SecondPrice.truthful_weakly_dominant — IsWeaklyDominant wrapper

References

• [Roughgarden, Twenty Lectures on Algorithmic Game Theory, Lecture 3]
• [Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, 1961]
• Ma Jiajun, Wang Haocheng — original formalization in math-xmum/gametheory

Winner and second price

In the second-price auction, the winner is the highest bidder (Auction.argmaxBid). The price paid by the winner is the second-highest bid (highest bid excluding the winner).

noncomputable def Auction.SecondPrice.winner {I : Type u_1} [Fintype I] [Nontrivial I] {U : Type u_2} [LinearOrder U] (b : I → U) : I

The winner of the second-price auction: the bidder with the highest bid. Uses Auction.argmaxBid from MechanismDesign.Auction.AuctionBasic.

Equations

• Auction.SecondPrice.winner b = Auction.argmaxBid b

noncomputable def Auction.SecondPrice.secondPrice {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [LinearOrder U] (b : I → U) : U

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

Equations

• Auction.SecondPrice.secondPrice b = Auction.maxBidExcluding b (Auction.SecondPrice.winner b)

Bridge lemmas

These restate key facts about winner and secondPrice using local names, so the proofs below do not need to spell out Auction.argmaxBid everywhere.

theorem Auction.SecondPrice.secondPrice_le_bid_winner {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [LinearOrder U] (b : I → U) : secondPrice b ≤ b (winner b)

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

noncomputable def Auction.SecondPrice.utility {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] (v b : I → U) (i : I) : U

Utility of bidder i in a second-price auction: winner gets v i − secondPrice b, losers get 0.

Equations

• Auction.SecondPrice.utility v b i = if i = Auction.SecondPrice.winner b then v i - Auction.SecondPrice.secondPrice b else 0

theorem Auction.SecondPrice.utility_winner {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] {v b : I → U} {i : I} (h : i = winner b) : utility v b i = v i - secondPrice b

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

theorem Auction.SecondPrice.utility_loser {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] {v b : I → U} {i : I} (h : i ≠ winner b) : utility v b i = 0

If i is not the winner, utility is 0.

theorem Auction.SecondPrice.utility_nonneg {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] {v b : I → U} {i : I} (htruth : b i = v i) : 0 ≤ utility v b i

Truthful bidding yields nonneg utility.

theorem Auction.SecondPrice.valuation_is_dominant {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] (v : I → U) (i : I) (b : I → U) : utility v b i ≤ utility v (Function.update b i (v i)) i

Vickrey's Theorem (core form): Truthful bidding dominates any other bid.

For any bid profile b, replacing i's bid with v i does not decrease i's utility.

noncomputable def Auction.SecondPrice.game {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] (v : I → U) : StrategicGame I U

Second-price auction as a strategic game.

This is also the game induced by mechanism via MechanismWithTransfers.toStrategicGame; see game_eq_toStrategicGame.

Equations

• Auction.SecondPrice.game v = { strategy := fun (x : I) => U, payoff := fun (b : I → U) (i : I) => Auction.SecondPrice.utility v b i }

theorem Auction.SecondPrice.truthful_weakly_dominant {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] (v : I → U) (i : I) : IsWeaklyDominant (game v) i (v i)

Vickrey's Theorem (strategic game form): Truthful bidding is a weakly dominant strategy in the second-price auction.

Mechanism design formulation

noncomputable def Auction.SecondPrice.mechanism {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] : MechanismWithTransfers I (fun (x : I) => U) I U

The second-price auction as a MechanismWithTransfers.

Agents report bids in U (their type space is homogeneous: T i = U).

• Allocation: the winner index (element of I)
• Payments: the winner pays secondPrice b; all losers pay 0.

This is the canonical MechanismWithTransfers instance from which the strategic game and DSIC statement are derived. [AGT Ch. 9]

Equations

• One or more equations did not get rendered due to their size.

theorem Auction.SecondPrice.game_eq_toStrategicGame {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] (v : I → U) : game v = mechanism.toStrategicGame (fun (w : I) (pay vals : I → U) (i : I) => if i = w then vals i - pay i else 0) v

game v equals the strategic game induced by mechanism.

The payoffs agree because paymentRule b i = if i = winner b then secondPrice b else 0, so (fun w pay v i => if i = w then v i - pay i else 0) (winner b) (paymentRule b) v i = utility v b i.

theorem Auction.SecondPrice.mechanism_isDSIC {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] : mechanism.isDSIC fun (w : I) (pay vals : I → U) (i : I) => if i = w then vals i - pay i else 0

Vickrey's Theorem (mechanism design form): The second-price auction satisfies dominant-strategy incentive compatibility.

This is mechanism.isDSIC (fun w pay v i => if i = w then v i - pay i else 0), the general DSIC predicate from MechanismDesign.Auction.Transfer applied to the second-price mechanism. Proof follows from truthful_weakly_dominant via game_eq_toStrategicGame.