# Re: [isabelle] ln on negative numbers

```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.

- Johannes

> 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.
> >
> >  - 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.