Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ln on negative numbers


view this post on Zulip Email Gateway (Aug 22 2022 at 09:33):

From: Manuel Eberl <eberlm@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 09:33):

From: Johannes Hölzl <hoelzl@in.tum.de>
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.

view this post on Zulip Email Gateway (Aug 22 2022 at 09:33):

From: Manuel Eberl <eberlm@in.tum.de>
I have no idea what you mean by a carrier set. The definition of O is
currently

O(g) = {f. (∃c>0. eventually (λx. ¦f x¦ ≤ c * ¦g x¦) at_top)}

I don't see how that could be augmented by a carrier set in a useful way.

A generalisation to other filters than at_top would be straightforward,
but I decided not to do that quite yet because I don't need it yet.

Manuel

view this post on Zulip Email Gateway (Aug 22 2022 at 09:33):

From: Johannes Hölzl <hoelzl@in.tum.de>
Am Mittwoch, den 29.04.2015, 19:38 +0200 schrieb Manuel Eberl:

I have no idea what you mean by a carrier set.

For O(g::'a => 'b) a set-based restriction on the type 'a.

The definition of O is currently

`O(g) = {f. (∃c>0. eventually (λx. ¦f x¦ ≤ c * ¦g x¦) at_top)}

I don't see how that could be augmented by a carrier set in a useful way.

Ah I see; I thought the problem was not only related to c but also to x.

A generalisation to other filters than at_top would be straightforward,
but I decided not to do that quite yet because I don't need it yet.

Yup.

On 29/04/15 19:25, Johannes Hölzl wrote:

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.

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

view this post on Zulip Email Gateway (Aug 22 2022 at 09:33):

From: Larry Paulson <lp15@cam.ac.uk>
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 Paulson

view this post on Zulip Email Gateway (Aug 22 2022 at 09:33):

From: Manuel Eberl <eberlm@in.tum.de>
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.

Cheers,

Manuel

view this post on Zulip Email Gateway (Aug 22 2022 at 09:34):

From: Larry Paulson <lp15@cam.ac.uk>
This identity holds for the real parts. For the imaginary parts, there is potentially a difference of 2pii due to the branch cut.

Larry Paulson

view this post on Zulip Email Gateway (Aug 22 2022 at 09:34):

From: Manuel Eberl <eberlm@in.tum.de>
Yes, I meant for all non-zero real x, of course. That would be quite
sufficient.


Last updated: Mar 28 2024 at 12:29 UTC