Email Gateway (Aug 22 2022 at 09:33): 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
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.
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
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.
- 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 likeO(λ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 havec 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
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
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
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
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: Nov 21 2024 at 12:39 UTC