nat.log is monotonically decreasing on its first argument

Stream: Is there code for X?

[Joanna Choules]

I've been able to write my own proof of

lemma log_le_log_of_left_ge {b c n : ℕ} (hc : c > 1) (hb : b ≥ c) : nat.log b n ≤ nat.log c n

since I couldn't find one in mathlib, but I wanted to check whether it is already there and I just missed it.

[Kevin Buzzard]

We may have (or be close to having) the word antitone to mean this, so that's what to search for (if the PR hit)

[Johan Commelin]

It should be in this file https://github.com/leanprover-community/mathlib/blob/master/src/data/nat/log.lean if it is there.

[Johan Commelin]

Doesn't seem the case, so please PR it!

[Kevin Buzzard]

But to answer your question, we may well not have it. My instinct would be to prove the Galois connection if we don't already have it: b^t <= n iff t <= log_b n: for fixed b, b^ and log_b are a Galois connection

[Johan Commelin]

We do have that: docs#nat.pow_le_iff_le_log

[Kevin Buzzard]

Why "almost" in the docstring? Oh, because 0<y maybe? So it's a Galois connection on pnat :-/

[Johan Commelin]

I guess so

[Joanna Choules]

I did use the Galois connection in my proof, yeah.

[Kevin Buzzard]

Nice!

[Kevin Buzzard]

Are you happy to PR it? If so then the simplest way is for you to do it is to ask for PR access for non-master branches of mathlib, if you don't have it already.

[Joanna Choules]

I am happy to, yeah. I don't think I have such access yet as I've not previously submitted any PRs.

[Johan Commelin]

@Joanna Choules What is your github username?

[Joanna Choules]

It's jchoules

[Johan Commelin]

https://github.com/leanprover-community/mathlib/invitations

[Joanna Choules]

Thank you!

[Kevin Buzzard]

Cheat sheet: https://leanprover-community.github.io/contribute/index.html

[Kevin Buzzard]

Feel free to ask if you have any questions

[Yaël Dillies]

Yeah! I didn't prove that one, so feel free to PR it.

[Joanna Choules]

I need to do some tidying (and prove the analogous lemma for clog while I'm at it - might as well), but I should be able to get it PR'd within the next day or so I think.

[Yaël Dillies]

Feel free to request a review from me then :wink: