Re: [isabelle] ln on negative numbers



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


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.