definition of real log

Stream: general

[Sebastien Gouezel]

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?

[Scott Morrison]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Johan Commelin]

@[irreducible] def junk := 37

[Johan Commelin]

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

[Johan Commelin]

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?

[Johan Commelin]

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

[Scott Morrison]

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

[Mario Carneiro]

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)

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

I think the only reasonable choices are 0 and 2

[Kenny Lau]

well -2 would keep the monotonic property

[Patrick Massot]

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.