# Zulip Chat Archive

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