## Stream: Is there code for X?

### Topic: real.log_ne_zero_iff?

#### Ryan Lahfa (Feb 01 2021 at 15:23):

I feel this theorem is missing:

import analysis.special_functions.exp_log

lemma real.log_ne_zero_iff (x: ℝ) (hpos: 0 < x): (real.log x ≠ 0 ↔ x ≠ 1) := sorry


The closest thing to this is log_pos which can help derive it, unsure if it is considered enough? (It seems like the situation is similar for the complex version of exponential)

#### Johan Commelin (Feb 01 2021 at 15:29):

Is it true? What is real.log (-1)?

#### Ryan Lahfa (Feb 01 2021 at 15:31):

I should try to prove first :p but what I meant is:

lemma real.log_ne_zero_of_ne_one (x: ℝ) (hx_pos: 0 < x) (hx: x ≠ 1): real.log x ≠ 0 :=
begin
by_cases (1 < x),
exact ne_of_gt (real.log_pos h),
push_neg at h,
exact ne_of_lt (real.log_neg hx_pos (lt_of_le_of_ne h hx)),
end


#### Yakov Pechersky (Feb 01 2021 at 16:45):

Isn't this just injectivity of log?

#### Ryan Lahfa (Feb 01 2021 at 16:55):

Yakov Pechersky said:

Isn't this just injectivity of log?

I'm not sure I see a proof of the log injectivity in the file, though there is a proof that exp is injective in the same file

#### Mario Carneiro (Feb 01 2021 at 16:55):

injectivity of log is the same as functionality of exp

#### Ryan Lahfa (Feb 01 2021 at 16:55):

functionality := ?

being a function

#### Mario Carneiro (Feb 01 2021 at 16:56):

exp is a function

#### Yakov Pechersky (Feb 01 2021 at 16:56):

log x = y \iff x = exp y

Ah, right

#### Mario Carneiro (Feb 01 2021 at 16:56):

of course, log isn't, really, since exp isn't injective

#### Ryan Lahfa (Feb 01 2021 at 16:56):

log x = 0 iff x = exp 0 = 1, indeed.

#### Yakov Pechersky (Feb 01 2021 at 16:58):

real.exp isn't injective?!

#### Yakov Pechersky (Feb 01 2021 at 16:59):

docs#real.exp_injective

ah, good point

#### Mario Carneiro (Feb 01 2021 at 16:59):

I was thinking of complex.exp

#### Yakov Pechersky (Feb 01 2021 at 17:00):

We have some missing lemmas relating the inverses of real.log and real.exp

#### Yakov Pechersky (Feb 01 2021 at 17:01):

And then "injectivity" of real.log comes out of having an inverse, etc.

#### Yury G. Kudryashov (Feb 02 2021 at 03:58):

Note that we have docs#real.strict_mono_incr_on_log

#### Yury G. Kudryashov (Feb 02 2021 at 04:00):

And docs#strict_mono_incr_on.inj_on
But a PR with (h : x ≠ 0) : log x = y ↔ exp y = abs x and (h : 0 < x) : log x = y ↔ exp y = x is very welcome.

#### Ryan Lahfa (Feb 02 2021 at 12:25):

Yury G. Kudryashov said:

And docs#strict_mono_incr_on.inj_on
But a PR with (h : x ≠ 0) : log x = y ↔ exp y = abs x and (h : 0 < x) : log x = y ↔ exp y = x is very welcome.

Alright, will try to come up with something

Thanks!

#### Eric Wieser (Feb 02 2021 at 12:29):

Is there a bundled exp equiv from real to R+?

#### Yury G. Kudryashov (Feb 02 2021 at 13:23):

docs#real.exp_order_iso

Last updated: May 07 2021 at 18:19 UTC