(*
Auction Theory Toolbox (http://formare.github.io/auctions/)
Authors:
* Manfred Kerber
* Christoph Lange
* Colin Rowat
* Makarius Wenzel
Dually licenced under
* Creative Commons Attribution (CC-BY) 3.0
* ISC License (1-clause BSD License)
See LICENSE file for details
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)
header {* Vickrey's Theorem *}
theory Vickrey
imports SecondPriceAuction SingleGoodAuctionProperties
begin
subsection {* Introduction *}
text{*
In second price (or Vickrey) auctions, bidders submit sealed bids;
the highest bidder wins, and pays the highest bid of the \emph{remaining} bids; the losers pay nothing.
(See \url{http://en.wikipedia.org/wiki/Vickrey_auction} for more information, including a discussion of variants used by eBay, Google and Yahoo!.)
Vickrey proved that `truth-telling' (i.e. submitting a bid equal to one's actual valuation of the good) was a weakly dominant strategy.
This means that no bidder could do strictly better by bidding above or below its valuation \emph{whatever} the other bidders did.
Thus, the auction is also efficient, awarding the item to the bidder with the highest valuation.
Vickrey was awarded Economics' Nobel prize in 1996 for his work.
High level versions of his theorem, and 12 others, were collected in Eric Maskin's 2004 review of Paul Milgrom's influential book on auction theory
(``The unity of auction theory: Milgrom's master class'', Journal of Economic Literature, 42(4), pp. 1102--1115).
Maskin himself won the Nobel in 2007.
*}
subsection {* Vickrey's Theorem *}
subsection {* Part 1: A second-price auction supports an equilibrium in weakly dominant
strategies if all participants bid their valuation. *}
theorem vickreyA:
fixes N :: "participant set" and v :: valuations and A :: single_good_auction
assumes val: "valuations N v"
defines "b \ v"
assumes spa: "second_price_auction A"
and card_N: "card N > 1"
shows "equilibrium_weakly_dominant_strategy N v b A"
proof -
have defined: "maximum_defined N" using card_N
unfolding maximum_defined_def by (auto simp: card_ge_0_finite)
then have finite: "finite N" by (metis card_N card_infinite less_nat_zero_code)
from val have bids: "bids N b"
unfolding b_def by (rule valuation_is_bid)
{
fix i :: participant
assume i_range: "i \ N"
let ?M = "N - {i}"
have defined': "maximum_defined ?M"
using card_N i_range unfolding maximum_defined_def
by (simp add: card_ge_0_finite card_Diff_singleton)
fix whatever_bid :: bids
assume alternative_is_bid: "bids N whatever_bid"
(* TOOD CL: also assume "whatever_bid i \ b i"? *)
let ?b = "whatever_bid(i := b i)"
have is_bid: "bids N ?b"
using bids alternative_is_bid
unfolding bids_def non_negative_def le_def zero_def by simp
let ?b_max = "maximum N ?b"
let ?b_max' = "maximum ?M ?b"
fix x :: allocation and x' :: allocation and p :: payments and p' :: payments
assume outcome: "((N, whatever_bid), (x, p)) \ A"
and outcome': "((N, ?b), (x', p')) \ A"
from spa outcome have spa_pred: "spa_pred N whatever_bid x p"
unfolding second_price_auction_def rel_sat_sga_pred_def by blast
from spa outcome' have spa_pred': "spa_pred N ?b x' p'"
unfolding second_price_auction_def rel_sat_sga_pred_def by blast
from spa_pred finite have allocation: "allocation N x" using spa_allocates by blast
from spa_pred' finite have allocation': "allocation N x'" using spa_allocates by blast
from spa_pred card_N have pay: "vickrey_payment N p" using spa_vickrey_payment by blast
from spa_pred' card_N have pay': "vickrey_payment N p'" using spa_vickrey_payment by blast
have weak_dominance:
"payoff (v i) (x' i) (p' i) \ payoff (v i) (x i) (p i)"
proof cases
assume alloc: "x' i = 1"
with spa_pred' i_range
have winner: "second_price_auction_winner N ?b x' p' i"
by (rule allocated_implies_spa_winner)
from winner have "?b i = ?b_max"
unfolding second_price_auction_winner_def arg_max_def by simp
with defined' have "?b i \ ?b_max'"
by (rule maximum_remaining_maximum)
from winner have "p' i = ?b_max'"
unfolding second_price_auction_winner_def second_price_auction_winner_outcome_def
by simp
have winner_payoff: "payoff (v i) (x' i) (p' i) = v i - ?b_max'"
using defined spa_pred' i_range alloc
by (rule second_price_auction_winner_payoff)
have non_negative_payoff: "payoff (v i) (x' i) (p' i) \ 0"
proof -
from `?b i \ ?b_max'` have "?b i - ?b_max' \ 0" by simp
with winner_payoff show ?thesis unfolding b_def by simp
qed
show ?thesis
proof cases -- {* case 1a of the short proof *}
assume "x i = 1"
with defined spa_pred alternative_is_bid i_range
have "payoff (v i) (x i) (p i) = v i - ?b_max'"
using winners_payoff_on_deviation_from_valuation unfolding b_def by simp
also have "\ = payoff (v i) (x' i) (p' i)" using winner_payoff ..
finally show ?thesis by (rule eq_refl)
next -- {* case 1b of the short proof *}
assume "x i \ 1"
(* CL: TODO I'm sure one can use spa_allocates_binary at the top level of the
case distinction, to get rid of having to do this step for each case distinction. *)
with spa_pred alternative_is_bid i_range have "x i = 0"
using spa_allocates_binary by blast
with spa_pred i_range
have "payoff (v i) (x i) (p i) = 0"
by (rule second_price_auction_loser_payoff)
also have "\ \ payoff (v i) (x' i) (p' i)" using non_negative_payoff .
finally show ?thesis .
qed
next -- {* case 2 of the short proof *}
assume non_alloc: "x' i \ 1"
(* CL: TODO I'm sure one can use spa_allocates_binary at the top level of the
case distinction, to get rid of having to do this step for each case distinction. *)
with spa_pred' i_range have "x' i = 0"
using spa_allocates_binary by blast
with spa_pred' i_range
have loser_payoff: "payoff (v i) (x' i) (p' i) = 0"
by (rule second_price_auction_loser_payoff)
have i_bid_at_most_second: "?b i \ ?b_max'"
proof (rule ccontr)
assume "\ ?thesis"
then have "?b i > ?b_max'" by simp
with defined spa_pred' i_range
have "second_price_auction_winner N ?b x' p' i"
using only_max_bidder_wins by simp
with non_alloc show False unfolding second_price_auction_winner_def second_price_auction_winner_outcome_def by fast
qed
show ?thesis
proof cases -- {* case 2a of the short proof *}
assume "x i = 1"
with defined spa_pred i_range
have "payoff (v i) (x i) (p i) = ?b i - ?b_max'"
using winners_payoff_on_deviation_from_valuation unfolding b_def by simp
also have "\ \ 0" using i_bid_at_most_second by simp
also have "\ = payoff (v i) (x' i) (p' i)" using loser_payoff ..
finally show ?thesis .
next -- {* case 2b of the short proof *}
assume "x i \ 1"
(* CL: TODO I'm sure one can use spa_allocates_binary at the top level of the
case distinction, to get rid of having to do this step for each case distinction. *)
with spa_pred alternative_is_bid i_range have "x i = 0"
using spa_allocates_binary by blast
with spa_pred i_range
have "payoff (v i) (x i) (p i) = 0"
by (rule second_price_auction_loser_payoff)
also have "\ = payoff (v i) (x' i) (p' i)" using loser_payoff ..
finally show ?thesis by (rule eq_refl)
qed
qed
}
with spa val bids show ?thesis
using spa_is_sga
unfolding equilibrium_weakly_dominant_strategy_def
by auto
qed
subsection {* Part 2: A second-price auction is efficient if all participants bid their valuation. *}
theorem vickreyB:
fixes N :: "participant set" and v :: valuations and A :: single_good_auction
assumes val: "valuations N v"
assumes spa: "second_price_auction A"
defines "b \ v"
shows "efficient N v b A"
proof -
from val have bids: "bids N v" by (rule valuation_is_bid)
{
fix k :: participant and x :: allocation and p :: payments
(* TODO CL: We actually don't need p; is there a way to do without naming it? *)
assume range: "k \ N" and outcome: "((N, v), (x, p)) \ A" and wins: "x k = 1"
from outcome spa have "spa_pred N v x p"
unfolding second_price_auction_def rel_sat_sga_pred_def
by blast
with range and wins have "k \ arg_max N v"
using allocated_implies_spa_winner
unfolding second_price_auction_winner_def by blast
}
with bids spa show ?thesis
using val unfolding b_def efficient_def using spa_is_sga by blast
qed
end