Re: [isabelle] Left and right limits

On Fri, Nov 12, 2010 at 9:03 AM, grechukbogdan <grechukbogdan at> 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

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

> 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.

- Brian

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