(* 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