On Jun 22, 2012 8:01 PM, "Colin Rowat" <c.rowat <at> bham.ac.uk> 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 = <at> 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
> hol-info <at> lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

I just realised you're probably using HOL Light... I was thinking in terms of HOL4 which I don't think has any existing theories about real vectors. My answer might not be so useful. I'll have a look at what HOL Light's real_max does and see if I can say something more useful...