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/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
