Re: [isabelle] ln on negative numbers



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
> 






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