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...
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?
>
> (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
