Zulip Chat Archive

Stream: general

Topic: definition of real log


view this post on Zulip Sebastien Gouezel (Apr 28 2020 at 07:46):

I have a controversial question (Kevin, close your eyes): how should we define the real logarithm of x when x < 0. Currently, it is 0, but I wonder if using log |x| would not be better, as it would satisfy the formulas log(xy) = log x + log y for all nonzero x and y, and log' = 1/x away from 0. Given that proving that something is nonzero is often easier than checking its positivity, this would make these statements easier to apply. Any thoughts?

view this post on Zulip Scott Morrison (Apr 28 2020 at 07:56):

That would also make it equal to the real part of our complex log.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 07:57):

Ha ha I am over all this now. I remember Chris having problems with junk inputs with this definition but I can't remember the details. Isn't log|x| actually a useful function in fact? Isn't it the indefinite integral of 1/x for example?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 07:58):

I think we had a similar discussion about the output of sqrt many years ago when I was learning this stuff (I wrote real.sqrt before there was one in mathlib because I needed it for my undergraduate problem sheets)

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 07:59):

I think Chris' observation was that exp (log (junk)) was not the traditional junk value of 0 but was actually 1

view this post on Zulip Johan Commelin (Apr 28 2020 at 08:07):

@[irreducible] def junk := 37

view this post on Zulip Johan Commelin (Apr 28 2020 at 08:11):

example :  p, irregular_prime := by use junk; exact dec_trivial

view this post on Zulip Johan Commelin (Apr 28 2020 at 08:12):

Sorry for trolling...
@Sebastien Gouezel I think this is a great idea! I think this is even sometimes done in "real" maths, isn't it?

view this post on Zulip Johan Commelin (Apr 28 2020 at 08:13):

As in, people write ln x, and they actually mean ln |x|, and this only gets corrected after a while

view this post on Zulip Scott Morrison (Apr 28 2020 at 08:14):

One day there are going to be theses written about how 37 became the world's default junk value.

view this post on Zulip Mario Carneiro (Apr 28 2020 at 08:33):

I think this is a good idea as well. Two arguments in favor are the use of ln |x| in intro calc and the fact that log |x| = Re (log x) (both mentioned above)

view this post on Zulip Mario Carneiro (Apr 28 2020 at 08:34):

Less clear is whether real.sqrt should do the same thing

view this post on Zulip Kenny Lau (Apr 28 2020 at 08:36):

when you said "intro calc" my first thought was the two tactics by intro and by calc... Lean syndrome

view this post on Zulip Kenny Lau (Apr 28 2020 at 08:37):

should real.sqrt (-4) be -2 or 2?

view this post on Zulip Mario Carneiro (Apr 28 2020 at 08:37):

I think the only reasonable choices are 0 and 2

view this post on Zulip Kenny Lau (Apr 28 2020 at 08:37):

well -2 would keep the monotonic property

view this post on Zulip Patrick Massot (Apr 28 2020 at 09:15):

Kenny Lau said:

when you said "intro calc" my first thought was the two tactics by intro and by calc... Lean syndrome

It got me stuck for a couple of seconds too.


Last updated: May 08 2021 at 18:17 UTC