Re: [isabelle] Extended real line and epigraph



Am 17.07.2010 18:30, schrieb grechukbogdan:
Dear Isabelle Users

In context of my convex analysis formalization I need to work with function from Euclidean Space to extended real line - namely Real together with TWO points -\infty and +\infty.

1) Is such extended real line defined in Isabelle? I will need basic operations like a * +\infty = +\infty for a>0, etc. I am not sure how to say that +\infty - (+\infty) is undefined...
There is a datatype pinfreal for non-negative real numbers and infinity. The latest (quite unstable) version is

http://isabelle.in.tum.de/~himmelma/cgi-bin/repos.cgi/mnt/tmp/himmelma/repos/isabelle/file/5efa68013118/src/HOL/Probability/Positive_Infinite_Real.thy

If you want to formalize the extended real line this theory might be a good starting point.

2) If so, are such functions from Euclidean Space to extended real line defined in Isabelle? What about convexity definition? I just do not want to define the same again.
We are using pinfreal only in the context of measure theory. There are no definitions or lemmas concerning convexity.

3) I will need a fact that epigraph of such a function is also a set in an Euclidean Space. Actually, epigaph is defined in Convex_Euclidean_Space.thy as a pair (x,y), or, in other words, subset of direct sum of Euclidean Space and Real.  This is connected with my previous question about direct sum of sets in R^n and R^m. I was told that there exists an instantiation

instantiation * :: (euclidean_space, euclidean_space) euclidean_space

which would be very useful. I have istalled latest repository version, but I do not see something like this. Is this instantiation  already done in repository version? If so, in which theory I can look at it, and can I use this for the purposes described above?
The instantiation can be found here: http://isabelle.in.tum.de/repos/isabelle/file/c26f9d06e82c/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy

Sincerely, Robert





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.