Re: [isabelle] Extended real line and epigraph
Am 17.07.2010 18:30, schrieb grechukbogdan:
There is a datatype pinfreal for non-negative real numbers and infinity.
The latest (quite unstable) version is
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...
If you want to formalize the extended real line this theory might be a
good starting point.
We are using pinfreal only in the context of measure theory. There are
no definitions or lemmas concerning convexity.
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.
The instantiation can be found here:
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and