22 Jun 2012 19:19

## theorem building in economics and finance => newbie questions in R^n

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,


25 Jun 2012 05:15

### Re: theorem building in economics and finance => newbie questions in R^n

Colin, I think I can say something about your 2nd question:

(3) u[i] (b,v,p) = -p[i] if x[i] = F, else v[i]-p[i],

(ii) how do I specify the role of the Boolean condition in u[i]?

Caution: I don't know what R^n_+ means.  Is that R^n with infinity
added on?  I'll pretend it's just R^n.  Then b,v and p are elements of
R^n, and u is a function

u: R^n x R^n x R^n ---> bool^n

with u[i] the i-th coordinate of u, itself a function

u[i]: R^n x R^n x R^n ---> bool

You can see from your definition (3) that u[i] isn't well-defined,
because the x on the right isn't an argument on the left.  So just
make x an argument:

u[i] (b,v,p,x) = - p[i] if x[i] = F, else v[i] - p[i]

--

--
Best,
Bill

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


25 Jun 2012 07:58

### Re: theorem building in economics and finance => newbie questions in R^n

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

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

25 Jun 2012 08:09

### Re: theorem building in economics and finance => newbie questions in R^n

Ramana, thanks for answering Colin's questions, as some expert should.
Yes, Colin is using HOL Light, but you can probably answer his
questions anyway.

what is y_j? Also, how are you formalising vectors?

y is any element of R^N, maybe written real^N.  y_j is its j-th entry.

What you wrote about sup & maximum probably has HOL Light analogues,
but I studied the HOL Light *.ml files and didn't find an exact answer
to Colin's first question, which was how to define this max function

(1) \bar{y} = max_{j in N} y_j for any y in R^n

The obvious way to do this is by recursion, by let rec'.  I still
haven't mastered the syntax, where to put the $s etc, but you can probably write this recursive function right away, so I'll post! -- -- Best, Bill ------------------------------------------------------------------------------ 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/  25 Jun 2012 08:40 ### Re: theorem building in economics and finance => newbie questions in R^n On Jun 25, 2012 7:10 AM, "Bill Richter" <richter <at> math.northwestern.edu> wrote: > > Ramana, thanks for answering Colin's questions, as some expert should. > Yes, Colin is using HOL Light, but you can probably answer his > questions anyway. > > what is y_j? Also, how are you formalising vectors? > > y is any element of R^N, maybe written real^N. y_j is its j-th entry. > > What you wrote about sup & maximum probably has HOL Light analogues, > but I studied the HOL Light *.ml files and didn't find an exact answer > to Colin's first question, which was how to define this max function > > (1) \bar{y} = max_{j in N} y_j for any y in R^n > > The obvious way to do this is by recursion, by let rec'. I still > haven't mastered the syntax, where to put the$s etc, but you can
> probably write this recursive function right away, so I'll post!

you can define maximum either using Hilbert choice (the <at> operator) as I showed in my first reply, or, if it's over the indices 0 to n as in this example you can use recursion as Bill suggests. Either way you'll also have to prove some useful properties about your definition. The definition by recursion might look like this:

(bar 0 m y = m) /\
(bar (SUC n) m y = bar n (real_max m (y n)) y)

where again I'm assuming y is a function taking an (in this case natural number) index and returning a real. modify as appropriate.

>
> --
> Best,
> Bill

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

29 Jun 2012 09:46

### Re: theorem building in economics and finance => newbie questions in R^n

Here's a question Ramana got me thinking about.  Going through the
tutorial, I see functions (p 83) which interpret just fine:

# let fib2 = define
(fib2 0 = 1) /\
(fib2 1 = 1) /\
(fib2 (n + 2) = fib2(n) + fib2(n + 1));;
val fib2 : thm =
|- fib2 0 = 1 /\ fib2 1 = 1 /\ fib2 (n + 2) = fib2 n + fib2 (n + 1)

But how can I use fib2 to calculate Fibonacci numbers?  I suppose if I
was trying to prove something about Fibonacci numbers, HOL Light with
this definition would be great.  But this doesn't get me anything:

# fib2 6;;
val it : term = fib2 6

and here I got an error:

# REAL_ARITH fib2 6;;
Exception: Failure "mk_neg".

Maybe what I'm really asking is how to use HOL Light as a CAS, I see
that at least one person, Cezary Kaliszyk, has done this:
http://cl-informatik.uibk.ac.at/users/cek/holcas.php
I bet a coauthor of Barendregt would do a good job here, but I'd guess
there a way in HOL Light to crank out some numbers from functions.

--

--
Best,
Bill

------------------------------------------------------------------------------
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/

30 Jun 2012 14:08

### Re: theorem building in economics and finance => newbie questions in R^n

bY
On Jun 29, 2012 9:47 AM, "Bill Richter" <richter <at> math.northwestern.edu> wrote:
>
> Here's a question Ramana got me thinking about.  Going through the
> tutorial, I see functions (p 83) which interpret just fine:
>
> # let fib2 = define
> (fib2 0 = 1) /\
> (fib2 1 = 1) /\
> (fib2 (n + 2) = fib2(n) + fib2(n + 1));;
> val fib2 : thm =
>  |- fib2 0 = 1 /\ fib2 1 = 1 /\ fib2 (n + 2) = fib2 n + fib2 (n + 1)
>
> But how can I use fib2 to calculate Fibonacci numbers?  I suppose if I
> was trying to prove something about Fibonacci numbers, HOL Light with
> this definition would be great.  But this doesn't get me anything:
>
> # fib2 6;;
> val it : term = fib2 6
>
> and here I got an error:
>
> # REAL_ARITH fib2 6;;
> Exception: Failure "mk_neg".
>
> Maybe what I'm really asking is how to use HOL Light as a CAS, I see
> that at least one person, Cezary Kaliszyk, has done this:
> http://cl-informatik.uibk.ac.at/users/cek/holcas.php
> I bet a coauthor of Barendregt would do a good job here, but I'd guess
> there a way in HOL Light to crank out some numbers from functions.

In HOL4 this functionality is called computeLib, primarily the EVAL function. I don't know if it exists in HOL Light. You can get some way towards it in either system by just using rewriting rules (e.g., pretend you're trying to prove an equality and call rewriting tactics).

>
> --
> Best,
> Bill
>
> ------------------------------------------------------------------------------
> 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

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

25 Jun 2012 08:02

### Re: theorem building in economics and finance => newbie questions in R^n

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" <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?

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


Gmane