EconCSLib.MechanismDesign.Auction.ReserveVickrey

Reserve Vickrey auction, formalized as a second-price auction with a reserve price.

Position in the hierarchy

MechanismWithTransfers I (fun _ => U) (Option I) U
  └─ ReserveSecondPrice.mechanism reserve         -- reserve allocation + clearing-price payments
       └─ ReserveSecondPrice.game reserve v       -- induced StrategicGame at true values v

SecondPrice.winner / SecondPrice.secondPrice      -- reused Vickrey primitives
  └─ ReserveSecondPrice.allocation reserve

This file follows the organization of Auction.Vickrey and reuses its second-price primitives. The difference is that the item may be withheld: the allocation type is Option I, where none means that the highest bid does not meet the reserve.

As in Auction.Vickrey, the file name records the standard Vickrey terminology, while the declarations use the descriptive namespace ReserveSecondPrice.

The winner, when the reserve is met, is the highest bidder selected by SecondPrice.winner; the winner pays the maximum of the reserve and SecondPrice.secondPrice.

Main definitions

• Auction.SecondPrice.winner - reused highest-bidder rule
• Auction.SecondPrice.secondPrice - reused second-price rule
• Auction.ReserveSecondPrice.clearingPrice - max reserve secondPrice
• Auction.ReserveSecondPrice.allocation - some winner if the reserve is met, otherwise none
• Auction.ReserveSecondPrice.mechanism - the reserve second-price auction as a MechanismWithTransfers
• Auction.ReserveSecondPrice.utility
• Auction.ReserveSecondPrice.game

Main results

• Auction.ReserveSecondPrice.allocation_eq_some_iff
• Auction.ReserveSecondPrice.allocation_eq_none_iff
• Auction.ReserveSecondPrice.clearingPrice_le_bid_of_allocation_eq_some
• Auction.ReserveSecondPrice.mechanism_payment_of_allocation_eq_some
• Auction.ReserveSecondPrice.mechanism_payment_of_allocation_ne_some
• Auction.ReserveSecondPrice.mechanism_payment_le_bid_of_allocation_eq_some
• Auction.ReserveSecondPrice.game_eq_toStrategicGame
• Auction.ReserveSecondPrice.mechanism_isDSIC
• Auction.ReserveSecondPrice.utility_nonneg
• Auction.ReserveSecondPrice.valuation_is_dominant
• Auction.ReserveSecondPrice.truthful_weakly_dominant

References

• [Nisan et al., Algorithmic Game Theory, Ch. 9]
• [Roughgarden, Twenty Lectures on Algorithmic Game Theory, Lecture 3]

Reserve and payment

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

The price paid by the winner: the maximum of the reserve and the second price.

Equations

• Auction.ReserveSecondPrice.clearingPrice reserve b = max reserve (Auction.SecondPrice.secondPrice b)

theorem Auction.ReserveSecondPrice.reserve_le_clearingPrice {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [LinearOrder U] (reserve : U) (b : I → U) : reserve ≤ clearingPrice reserve b

The clearing price is at least the reserve.

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

The clearing price is at least the second price.

noncomputable def Auction.ReserveSecondPrice.allocation {I : Type u_1} [Fintype I] [Nontrivial I] {U : Type u_2} [LinearOrder U] (reserve : U) (b : I → U) : Option I

The item is sold exactly when the winning bid meets the reserve.

Equations

• Auction.ReserveSecondPrice.allocation reserve b = if reserve ≤ b (Auction.SecondPrice.winner b) then some (Auction.SecondPrice.winner b) else none

Reserve bridge lemmas

theorem Auction.ReserveSecondPrice.winner_eq_of_allocation_eq_some {I : Type u_1} [Fintype I] [Nontrivial I] {U : Type u_2} [LinearOrder U] {reserve : U} {b : I → U} {i : I} (halloc : allocation reserve b = some i) : SecondPrice.winner b = i

If bidder i is allocated the item, then i is the second-price winner.

theorem Auction.ReserveSecondPrice.reserve_le_bid_winner_of_allocation_eq_some {I : Type u_1} [Fintype I] [Nontrivial I] {U : Type u_2} [LinearOrder U] {reserve : U} {b : I → U} {i : I} (halloc : allocation reserve b = some i) : reserve ≤ b (SecondPrice.winner b)

If the item is allocated, then the winning bid meets the reserve.

theorem Auction.ReserveSecondPrice.allocation_eq_some_iff {I : Type u_1} [Fintype I] [Nontrivial I] {U : Type u_2} [LinearOrder U] {reserve : U} {b : I → U} {i : I} : allocation reserve b = some i ↔ reserve ≤ b (SecondPrice.winner b) ∧ SecondPrice.winner b = i

The allocation is some i exactly when the reserve is met and i is the second-price winner.

theorem Auction.ReserveSecondPrice.allocation_eq_some_winner_iff {I : Type u_1} [Fintype I] [Nontrivial I] {U : Type u_2} [LinearOrder U] {reserve : U} {b : I → U} : allocation reserve b = some (SecondPrice.winner b) ↔ reserve ≤ b (SecondPrice.winner b)

The allocation is the second-price winner exactly when the winner's bid meets the reserve.

theorem Auction.ReserveSecondPrice.allocation_eq_none_iff {I : Type u_1} [Fintype I] [Nontrivial I] {U : Type u_2} [LinearOrder U] {reserve : U} {b : I → U} : allocation reserve b = none ↔ b (SecondPrice.winner b) < reserve

The item is withheld exactly when the winning bid is below the reserve.

theorem Auction.ReserveSecondPrice.clearingPrice_le_bid_of_allocation_eq_some {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [LinearOrder U] {reserve : U} {b : I → U} {i : I} (halloc : allocation reserve b = some i) : clearingPrice reserve b ≤ b i

When the item is sold, the clearing price is no more than the allocated bidder's bid.

theorem Auction.ReserveSecondPrice.clearingPrice_eq_max_reserve_excluding_of_allocation_eq_some {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [LinearOrder U] {reserve : U} {b : I → U} {i : I} (halloc : allocation reserve b = some i) : clearingPrice reserve b = max reserve (maxBidExcluding b i)

When bidder i receives the item, the clearing price is the maximum of the reserve and the highest bid excluding i.

Utility and strategic-game formulation

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

Utility of bidder i: the allocated bidder receives value minus the clearing price; all others receive 0.

Equations

• Auction.ReserveSecondPrice.utility reserve v b i = if Auction.ReserveSecondPrice.allocation reserve b = some i then v i - Auction.ReserveSecondPrice.clearingPrice reserve b else 0

theorem Auction.ReserveSecondPrice.utility_winner {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] {reserve : U} {v b : I → U} {i : I} (h : allocation reserve b = some i) : utility reserve v b i = v i - clearingPrice reserve b

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

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

Truthful bidding yields nonnegative utility.

theorem Auction.ReserveSecondPrice.valuation_is_dominant {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] [IsOrderedAddMonoid U] (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

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

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

Reserve second-price auction as a strategic game.

Equations

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

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

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

Mechanism design formulation

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

The reserve second-price auction as a MechanismWithTransfers.

Agents report bids in U. The allocation is none when the reserve is not met, and some i when bidder i receives the item.

Equations

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

@[simp]

theorem Auction.ReserveSecondPrice.mechanism_allocationRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] (reserve : U) (b : I → U) : (mechanism reserve).allocationRule b = allocation reserve b

@[simp]

theorem Auction.ReserveSecondPrice.mechanism_paymentRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] (reserve : U) (b : I → U) (i : I) : (mechanism reserve).paymentRule b i = if allocation reserve b = some i then clearingPrice reserve b else 0

theorem Auction.ReserveSecondPrice.mechanism_payment_of_allocation_eq_some {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] {reserve : U} {b : I → U} {i : I} (halloc : allocation reserve b = some i) : (mechanism reserve).paymentRule b i = clearingPrice reserve b

The allocated bidder pays the clearing price.

theorem Auction.ReserveSecondPrice.mechanism_payment_of_allocation_ne_some {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] {reserve : U} {b : I → U} {i : I} (halloc : allocation reserve b ≠ some i) : (mechanism reserve).paymentRule b i = 0

A bidder who is not allocated the item pays zero.

theorem Auction.ReserveSecondPrice.mechanism_payment_eq_zero_of_allocation_eq_none {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] {reserve : U} {b : I → U} {i : I} (halloc : allocation reserve b = none) : (mechanism reserve).paymentRule b i = 0

If the item is withheld, every bidder pays zero.

theorem Auction.ReserveSecondPrice.mechanism_payment_le_bid_of_allocation_eq_some {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] {U : Type u_2} [AddCommGroup U] [LinearOrder U] {reserve : U} {b : I → U} {i : I} (halloc : allocation reserve b = some i) : (mechanism reserve).paymentRule b i ≤ b i

The allocated bidder never pays more than her reported bid.

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

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

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

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