# [isabelle] ln on negative numbers

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

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