[isabelle] ln on negative numbers


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)


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.



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