Email Gateway (Aug 18 2022 at 15:40): Email Gateway (Aug 18 2022 at 15:40):From: grechukbogdan <grechukbogdan@yandex.ru>
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...
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.
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?
Sincerely,
Bogdan Grechuk.
Email Gateway (Aug 18 2022 at 15:41):From: Robert Himmelmann <himmelma@in.tum.de>
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
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
Last updated: Apr 19 2024 at 08:19 UTC