*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] ln on negative numbers*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 29 Apr 2015 19:38:15 +0200*In-reply-to*: <1430328335.11504.5.camel@lapnipkow5>*References*: <5540E488.6070106@in.tum.de> <1430328335.11504.5.camel@lapnipkow5>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

I have no idea what you mean by a carrier set. The definition of O is currently O(g) = {f. (âc>0. eventually (Îx. Âf xÂ â c * Âg xÂ) at_top)} I don't see how that could be augmented by a carrier set in a useful way. A generalisation to other filters than at_top would be straightforward, but I decided not to do that quite yet because I don't need it yet. Manuel On 29/04/15 19:25, Johannes HÃlzl wrote: > I don't object to give ln a known value for negative numbers. > > But I also think you need to add a carrier set (like a O_on A f) to your > O-notation! Many definitions in Isabelle/HOL nowadays have it. > Btw: if you integrate filters into your O-notation this is not necessary > any more, as this is taken care of by the "at _ within _" filter. > > - Johannes > > Am Mittwoch, den 29.04.2015, 16:02 +0200 schrieb Manuel Eberl: >> Hallo, >> >> I am currently in the process of writing some automation for Landau >> symbols. One of the problems that I currently have is that I would like >> to rewrite things like >> >> O(Îx. (c*x) powr p) >> >> to >> >> O(Îx. c powr p * x powr p) >> >> However, for c < 0 this is simply not true (well, morally not true). If >> c < 0, and w.l.o.g. x > 0, we have >> >> c powr p = (c*x) powr p = exp (p * THE u. False) >> >> >> I therefore suggest to define the real logarithm as "ln x = (if x â 0 >> then 0 else THE u. exp u = x)". The practical implications of this >> should be small, and it would allow stating a lot of lemmas involving >> "powr" in a much simpler form and allow transformations such as the one >> above. >> >> Cheers, >> >> Manuel >> > >

**Follow-Ups**:**Re: [isabelle] ln on negative numbers***From:*Johannes Hölzl

**References**:**[isabelle] ln on negative numbers***From:*Manuel Eberl

**Re: [isabelle] ln on negative numbers***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] ln on negative numbers
- Next by Date: Re: [isabelle] ln on negative numbers
- Previous by Thread: Re: [isabelle] ln on negative numbers
- Next by Thread: Re: [isabelle] ln on negative numbers
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list