real.log_ne_zero_iff?

Stream: Is there code for X?

[Ryan Lahfa]

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]

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

[Ryan Lahfa]

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]

Isn't this just injectivity of log?

[Ryan Lahfa]

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]

injectivity of log is the same as functionality of exp

[Ryan Lahfa]

functionality := ?

[Mario Carneiro]

being a function

[Mario Carneiro]

exp is a function

[Yakov Pechersky]

log x = y \iff x = exp y

[Ryan Lahfa]

Ah, right

[Mario Carneiro]

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

[Ryan Lahfa]

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

[Yakov Pechersky]

real.exp isn't injective?!

[Yakov Pechersky]

docs#real.exp_injective

[Mario Carneiro]

ah, good point

[Mario Carneiro]

I was thinking of complex.exp

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yury G. Kudryashov]

Note that we have docs#real.strict_mono_incr_on_log

[Yury G. Kudryashov]

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]

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

[Ryan Lahfa]

Thanks!

[Eric Wieser]

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

[Yury G. Kudryashov]

docs#real.exp_order_iso