EconCSLib.MechanismDesign.Auction.FirstPrice

First-price auction: the winner pays their own bid.

Position in the hierarchy

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

The auction is formalized as a MechanismWithTransfers (from MechanismDesign.Auction.Transfer). The absence of DSIC is stated as ¬ mechanism.isDSIC auctionUtility.

Typeclass design

Same as Auction.Vickrey:

• [AddCommGroup U] — subtraction for utility
• [LinearOrder U] — comparing bids
• [IsOrderedAddMonoid U] — ordered group compatibility

Additionally, mechanism_not_isDSIC requires the existence of a positive element a : U (to construct distinct bid levels for the counterexample).

Main definitions

• Auction.FirstPrice.winner — the highest bidder (uses Auction.argmaxBid from Basic)
• Auction.FirstPrice.mechanism — first-price auction as a MechanismWithTransfers
• Auction.FirstPrice.utility — concrete utility formula (winner pays own bid)
• Auction.FirstPrice.game — first-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.FirstPrice.game_eq_toStrategicGame — game v equals the mechanism-induced game
• Auction.FirstPrice.mechanism_not_isDSIC — first-price auction fails DSIC
• Auction.FirstPrice.no_dominant_strategy — no strategy is weakly dominant (game form)

References

• [Roughgarden, Twenty Lectures on Algorithmic Game Theory, Lecture 3]
• Ma Jiajun, Wang Haocheng — original formalization in math-xmum/gametheory

Winner

In the first-price auction, the winner is the highest bidder (Auction.argmaxBid).

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

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

Equations

• Auction.FirstPrice.winner b = Auction.argmaxBid b

Bridge lemma

noncomputable def Auction.FirstPrice.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 first-price auction: winner gets v i − b i (pays own bid), losers get 0.

Equations

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

theorem Auction.FirstPrice.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 - b i

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

theorem Auction.FirstPrice.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.

noncomputable def Auction.FirstPrice.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

First-price auction as a strategic game.

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

Equations

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

theorem Auction.FirstPrice.no_dominant_strategy {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) (bi : U) (ha : ∃ (a : U), 0 < a) : ¬IsWeaklyDominant (game v) i bi

No dominant strategy exists in first-price auctions.

For any bidder i and any bid bi, there exists a profile where bidding bi is not optimal for i.

Counterexample (from xmum/gametheory): set all opponents to bid bi − a for some a > 0, then i wins with both bi and bi − a but pays less with bi − a.

Mechanism design formulation

noncomputable def Auction.FirstPrice.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 first-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 their own bid b i; all losers pay 0.

Equations

• Auction.FirstPrice.mechanism = { allocationRule := fun (b : I → U) => Auction.FirstPrice.winner b, paymentRule := fun (b : I → U) (i : I) => if i = Auction.FirstPrice.winner b then b i else 0 }

theorem Auction.FirstPrice.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 b i else 0, so the utility is v i - b i for the winner and 0 for losers.

theorem Auction.FirstPrice.mechanism_not_isDSIC {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] (ha : ∃ (a : U), 0 < a) : ¬mechanism.isDSIC fun (w : I) (pay vals : I → U) (i : I) => if i = w then vals i - pay i else 0

No dominant strategy in first-price auctions (mechanism design form).

The first-price auction does not satisfy DSIC: truthful bidding is not a weakly dominant strategy. This follows from no_dominant_strategy via game_eq_toStrategicGame.

Requires a positive element a : U to construct the counterexample profile.