Re: [isabelle] ln on negative numbers
That would probably also solve my problem.
As long as "(a*b) powr c = a powr c * b powr c" holds unconditionally, I
am happy. And if I am not mistaken, that is the case iff "ln (a*b) = ln
a + ln b" holds for all non-zero a,b.
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.
On 29 Apr 2015, at 15:02, Manuel Eberl <eberlm at in.tum.de> wrote:
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