*To*: Larry Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] ln on negative numbers*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 30 Apr 2015 12:05:57 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <7280EAEA-8715-472E-8B9E-6C11AC41F26A@cam.ac.uk>*References*: <5540E488.6070106@in.tum.de> <7280EAEA-8715-472E-8B9E-6C11AC41F26A@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

That would probably also solve my problem.

Cheers, Manuel On 30/04/15 11:44, Larry Paulson wrote:

For real r>0, the complex log (Ln) satisfies Ln(-r) = ln(r) + pi*I So I donât like extending the domain of ln using 0, as opposed to ln(|r|). This would extend the validity of 0 < ?z â Ln (complex_of_real ?z) = complex_of_real (ln ?z) Thereâs still the question of ln(0). Note that Ln(z) is defined for all complex numbers except when z=0. Larry PaulsonOn 29 Apr 2015, at 15:02, Manuel Eberl <eberlm at in.tum.de> wrote: 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:*Larry Paulson

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

**Re: [isabelle] ln on negative numbers***From:*Larry Paulson

- Previous by Date: Re: [isabelle] ln on negative numbers
- Next by Date: Re: [isabelle] libisabelle: Small Scala library to communicate with Isabelle
- 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