Email Gateway (Aug 18 2022 at 16:27): Email Gateway (Aug 18 2022 at 16:27):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users
Is there a notion of left and right limits defined in Isabelle?
For example, is there a notation to formulate a lemma that function f(x)=x/|x| at 0 has limit -1 if x tend to 0 from the left and +1, if x tend to 0 from the right?
If not, I need to define this for my formalization. Clearly, such limits are important far more than in convex analysis, in particular they are needed to introduce left and right derivatives, etc. Do you have any suggestions how to define this properly and which notation is better to use (maybe, consistent with some other formalizations, etc) ?
Sincerely,
Bogdan
Email Gateway (Aug 18 2022 at 16:27):From: Brian Huffman <brianh@cs.pdx.edu>
On Fri, Nov 12, 2010 at 9:03 AM, grechukbogdan <grechukbogdan@yandex.ru> wrote:
Dear Isabelle Users
Is there a notion of left and right limits defined in Isabelle?
For example, is there a notation to formulate a lemma that function f(x)=x/|x| at 0 has limit -1 if x tend to 0 from the left and +1, if x tend to 0 from the right?
There is a "within" operation that can be used to restrict limits to a
specific set of inputs. Left and right limits are a special case. For
example, you can express the limits of your function f at zero like
this:
definition f :: "real => real" where "f x = x / abs x"
term "(f ---> 1) (at 0 within {0..})"
term "(f ---> -1) (at 0 within {..0})"
The "within" operator is defined in src/HOL/Limits.thy. It was based
on a similar operation in John Harrison's formalization of
multivariate analysis in HOL-Light.
I don't know if there are very many useful lemmas for reasoning about
"within"; you might find some more in the HOL/Multivariate_Analysis
directory.
If not, I need to define this for my formalization. Clearly, such limits are important far more than in convex analysis, in particular they are needed to introduce left and right derivatives, etc. Do you have any suggestions how to define this properly and which notation is better to use (maybe, consistent with some other formalizations, etc) ?
The "has_derivative" predicate in
src/HOL/Multivariate_Analysis/Derivative.thy also works with the
"within" operator. Again, I believe this is also based on Harrison's
HOL-Light theories, and uses similar notation.
Last updated: Nov 21 2024 at 12:39 UTC