## Stream: general

### Topic: definition of real log

#### 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?

#### Scott Morrison (Apr 28 2020 at 07:56):

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

#### 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?

#### 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)

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

#### Johan Commelin (Apr 28 2020 at 08:07):

@[irreducible] def junk := 37


#### Johan Commelin (Apr 28 2020 at 08:11):

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


#### 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?

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

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

#### 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)

#### Mario Carneiro (Apr 28 2020 at 08:34):

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

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

#### Kenny Lau (Apr 28 2020 at 08:37):

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

#### Mario Carneiro (Apr 28 2020 at 08:37):

I think the only reasonable choices are 0 and 2

#### Kenny Lau (Apr 28 2020 at 08:37):

well -2 would keep the monotonic property

#### 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: Dec 20 2023 at 11:08 UTC