On Jun 22, 2012 8:01 PM, "Colin Rowat" <[email protected]> wrote:
>
> I am trying to formalise Vickrey's 1961 result on equilibrium in
second-price auctions. (See Maskin's 2004 "The Unity of Auction Theory:
Milgrom's Masterclass", J. Ec. Literature for a concise presentation of
this and other results.)
>
> Doing so involves:
> (a) N = {1, ..., n}, a set of bidders;
> (b) v in R^n_+, a vector of bidders' valuations;
> (c) b in R^n_+, a vector of bids, formed by strategies mapping from
valuations;
> (d) x in bool^n, setting x[i] = T if the auction awards the good to
bidder i, and F otherwise;
> (e) p in R^n, a vector of prices to be paid by the bidders, as specified
by the auction;
> (f) an auction, a map from b, the bids, to x,p.
>
> To establish the result, I wish to define:
> (1) \bar{y} = max_{j in N} y_j for any y in R^n
> (2) \bar{y}_{-i} = max_{j in N\{i}} y_j, also for any y in R^n
> (3) u[i] (b,v,p) = -p[i] if x[i] = F, else v[i]-p[i], bidder i's payoff
>
> In trying to define these, I have encountered two questions:
> (i) is there a straightforward way of extending real_max to define the
first two objects?
I can't understand your definition: what is y_j? Also, how are you
formalising vectors?
If you want to take the maximum of a set of real numbers indexed by some
countable set you can use sup, like this:
sup (IMAGE y s)
where y:ty->real gives you the real number at some index, s:ty set is the
set of indices (e.g. you might want (count n):num set) and ty is the type
of the indices.
sup happens to coincide in this case with "maximum", which you might define
more generally as maximum s = @r. r IN s /\ !x. x IN s ==> x <= r. (It
might be defined already somewhere.)
>
> (ii) how do I specify the role of the Boolean condition in u[i]? My
naïve attempt to just
>
> let payoff = new_definition `(payoff:real^N->real^N->real^N) v p =
lambda i. (if ~(x:bool^N$i) then &0- p$i else v$i - p$i)`;;
>
> yields a "typechecking error (initial type assignment)".
>
> Any help with either of these questions would be gratefully appreciated.
>
> Thank you,
>
> Colin Rowat
> University of Birmingham
>
> p.s. A second-price auction (SPA) allocates the good to the highest
bidder, who pays the bid of the second highest bidder; no bidder other than
the winner pays anything. Vickrey's result is that SPA admit a type of
equilibrium that makes minimal informational assumptions about other
bidders, known as an equilibrium in weakly dominant strategies - such that
each bidder is at least as well off sticking to its bid, whatever else the
other bidders are doing. (Contrast to a [Bayesian] Nash equilibrium: the
bidder is at least as well off with its bid, given particular bids by
others.) The equilibrium bids in an SPA have the following form: bidders
bid their valuations, so that b[i] = v[i], and the auction is efficient
(awarding the good to a bidder valuing it most highly).
>
>
------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
