Lean declarations

def Auction.ReserveSecondPrice.clearingPrice EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey
The price paid by the winner: the maximum of the reserve and the second price.
```
noncomputable def clearingPrice (reserve : U) (b : I → U) : U :=
  max reserve (SecondPrice.secondPrice b)
```
def Auction.ReserveSecondPrice.allocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey
The item is sold exactly when the winning bid meets the reserve.
```
noncomputable def allocation (reserve : U) (b : I → U) : Option I :=
  if reserve ≤ b (SecondPrice.winner b) then some (SecondPrice.winner b) else none
```

def Auction.ReserveSecondPrice.utility EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

noncomputable def utility (reserve : U) (v b : I → U) (i : I) : U :=
  if allocation reserve b = some i then v i - clearingPrice reserve b else 0

def Auction.ReserveSecondPrice.game EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey
Reserve second-price auction as a strategic game.
```
noncomputable def game (reserve : U) (v : I → U) : StrategicGame I U where
  strategy := fun _ => U
  payoff b i := utility reserve v b i
```

def Auction.ReserveSecondPrice.mechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

noncomputable def mechanism (reserve : U) :
    MechanismWithTransfers I (fun _ => U) (Option I) U where
  allocationRule b := allocation reserve b
  paymentRule b i := if allocation reserve b = some i then clearingPrice reserve b else 0

lemma Auction.ReserveSecondPrice.allocation_eq_some_iff EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

lemma allocation_eq_some_iff {reserve : U} {b : I → U} {i : I} :
    allocation reserve b = some i ↔
      reserve ≤ b (SecondPrice.winner b) ∧ SecondPrice.winner b = i

lemma Auction.ReserveSecondPrice.allocation_eq_none_iff EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey
The item is withheld exactly when the winning bid is below the reserve.
```
lemma allocation_eq_none_iff {reserve : U} {b : I → U} :
    allocation reserve b = none ↔ b (SecondPrice.winner b) < reserve
```

lemma Auction.ReserveSecondPrice.clearingPrice_le_bid_of_allocation_eq_some EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

lemma clearingPrice_le_bid_of_allocation_eq_some {reserve : U} {b : I → U} {i : I}
    (halloc : allocation reserve b = some i) :
    clearingPrice reserve b ≤ b i

lemma Auction.ReserveSecondPrice.mechanism_payment_of_allocation_eq_some EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey

The allocated bidder pays the clearing price.

lemma mechanism_payment_of_allocation_eq_some {reserve : U} {b : I → U} {i : I}
    (halloc : allocation reserve b = some i) :
    (mechanism reserve).paymentRule b i = clearingPrice reserve b

lemma Auction.ReserveSecondPrice.mechanism_payment_of_allocation_ne_some EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.ReserveVickrey
A bidder who is not allocated the item pays zero.
```
lemma mechanism_payment_of_allocation_ne_some {reserve : U} {b : I → U} {i : I}
    (halloc : allocation reserve b ≠ some i) :
    (mechanism reserve).paymentRule b i = 0
```

Modules: EconCSLib.MechanismDesign.Auction.ReserveVickrey

Reserve Second-Price Mechanism

The reserve second-price auction is the Vickrey auction with a seller reserve. The highest bidder receives the item only if the highest bid meets the reserve; otherwise the item is withheld. When the item is sold, the winner pays the maximum of the reserve and the second-highest bid.

Lean objects

The module EconCSLib.MechanismDesign.Auction.ReserveVickrey reuses the second-price primitives from [[mechanism_design.auction.basic.second_price_mechanism]].

clearingPrice reserve b is \(\max(\mathrm{reserve}, \mathrm{secondPrice}(b))\).
allocation reserve b : Option I is some i when bidder i is the selected highest bidder and the reserve is met; it is none when the item is withheld.
utility reserve v b i is the quasi-linear payoff: the allocated bidder gets value minus clearing price, and all other bidders get zero.
mechanism reserve packages the rule as a MechanismWithTransfers with allocation type Option I.

Basic facts

The formalization records the expected case analysis:

allocation_eq_some_iff characterizes the sale case.
allocation_eq_none_iff characterizes the no-sale case.
clearingPrice_le_bid_of_allocation_eq_some shows that the allocated bidder never pays more than her bid.

These facts are the local algebraic core used in the DSIC proof [[mechanism_design.auction.basic.reserve_second_price_dsic]].

References

[AGT, Chapter 9, Section 9.3] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory.
[Krishna, Chapter 2] Vijay Krishna, Auction Theory, 2nd ed..
[MSZ, Chapter 12] Maschler, Solan, and Zamir, Game Theory.

Used by

Reserve Second-Price Truth-Telling Is Dominant

Reserve Second-Price Mechanism

Lean objects

Basic facts

References

Used by

Also in