Zulip Chat Archive

Stream: Is there code for X?

Topic: real.log_ne_zero_iff?


view this post on Zulip 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)

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:29):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Feb 01 2021 at 16:45):

Isn't this just injectivity of log?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 01 2021 at 16:55):

injectivity of log is the same as functionality of exp

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 16:55):

functionality := ?

view this post on Zulip Mario Carneiro (Feb 01 2021 at 16:56):

being a function

view this post on Zulip Mario Carneiro (Feb 01 2021 at 16:56):

exp is a function

view this post on Zulip Yakov Pechersky (Feb 01 2021 at 16:56):

log x = y \iff x = exp y

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 16:56):

Ah, right

view this post on Zulip Mario Carneiro (Feb 01 2021 at 16:56):

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

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 16:56):

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

view this post on Zulip Yakov Pechersky (Feb 01 2021 at 16:58):

real.exp isn't injective?!

view this post on Zulip Yakov Pechersky (Feb 01 2021 at 16:59):

docs#real.exp_injective

view this post on Zulip Mario Carneiro (Feb 01 2021 at 16:59):

ah, good point

view this post on Zulip Mario Carneiro (Feb 01 2021 at 16:59):

I was thinking of complex.exp

view this post on Zulip Yakov Pechersky (Feb 01 2021 at 17:00):

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

view this post on Zulip Yakov Pechersky (Feb 01 2021 at 17:01):

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

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 03:58):

Note that we have docs#real.strict_mono_incr_on_log

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (Feb 02 2021 at 12:25):

Thanks!

view this post on Zulip Eric Wieser (Feb 02 2021 at 12:29):

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

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 13:23):

docs#real.exp_order_iso


Last updated: May 07 2021 at 18:19 UTC