2^n >= n^m

Stream: Is there code for X?

[Pascal Schoppenhauer]

Ok guys I have given up... Does someone want to help me write a maths proof and formalize it in lean? example : ∀ (m n : nat), m^2 ≤ n → 4 ≤ m → n^m ≤ 2^n := sorry I will credit you in my paper.

[Yaël Dillies]

Relayed it on Discord.

[Pascal Schoppenhauer]

what discord?

[Yaël Dillies]

The Xena Discord server. Kevin Buzzard's lair.

[Yaël Dillies]

You might want to have a look at #2784, #8002, #9890, #9925

[Yaël Dillies]

They are lemmas about Bertrand's postulate, which has the same flavor as your problem.

[Kevin Buzzard]

Right now the only maths proof I have is pretty horrible (it involves logs).

[Yakov Pechersky]

Kevin, docs#nat.log or lifting to reals?

[Kevin Buzzard]

I only wrote a pen and paper proof and I used regular log, this was why I didn't formalise my proof

[Kevin Buzzard]

I needed log(n)^2<n(log(2))^2 for n>=16

[Bhavik Mehta]

I think I have a proof which I can formalise, writing it down now

[Bolton Bailey]

Ah yes, this is one of those problems that might depend on showing that log x / x is decreasing. The recently added lemma docs#real.log_div_self_antitone_on could be helpful.

[Bolton Bailey]

basically
n^m ≤ 2^n ↔ m log n ≤ n log 2 ↔ (log n) / n ≤ (log 2) / m
which follows from (log m^2) / m^2 ≤ log 2 / m, since log x / x is decreasing for large enough n.

[Bhavik Mehta]

Yeah that's essentially what I'm doing, using your new lemma!

[Bhavik Mehta]

import analysis.special_functions.log
import analysis.special_functions.pow
import data.complex.exponential_bounds

lemma sq_le_two_pow {m : ℕ} (hm : 4 ≤ m) : m ^ 2 ≤ 2 ^ m :=
begin
  refine nat.le_rec_on' hm _ (by norm_num),
  intros k hk ih,
  rw [pow_succ 2, add_sq, mul_one, one_pow, add_assoc],
  apply le_trans _ (nat.mul_le_mul_left 2 ih),
  rw [two_mul (k ^ 2), add_le_add_iff_left, sq],
  nlinarith,
end

lemma real.pow_le_pow_swap {x y : ℝ} (hx : real.exp 1 ≤ x) (hy : x ≤ y) :
  y ^ x ≤ x ^ y :=
begin
  have hx' := (real.exp_pos 1).trans_le hx,
  rw [←real.log_le_log (real.rpow_pos_of_pos (hx'.trans_le hy) _) (real.rpow_pos_of_pos hx' _),
    real.log_rpow (hx'.trans_le hy), real.log_rpow hx', mul_comm x, mul_comm y,
    ←div_le_div_iff (hx'.trans_le hy) hx'],
  exact real.log_div_self_antitone_on hx (hx.trans hy) hy,
end

lemma pow_le_pow_swap {m n : ℕ} (hm : 3 ≤ m) (hn : m ≤ n) :
  n ^ m ≤ m ^ n :=
begin
  rw [←@nat.cast_le ℝ, nat.cast_pow, nat.cast_pow, ←real.rpow_nat_cast, ←real.rpow_nat_cast],
  exact real.pow_le_pow_swap
    (real.exp_one_lt_d9.le.trans (le_trans (by norm_num) (nat.cast_le.2 hm))) (nat.cast_le.2 hn),
end

example : ∀ (m n : nat), m^2 ≤ n → 4 ≤ m → n^m ≤ 2^n :=
begin
  intros m n h₁ h₂,
  refine (nat.pow_le_iff_le_left ((show 1 ≤ 4, by norm_num1).trans h₂)).1 _,
  have h₃ : n^(m^2) ≤ (m^2)^n,
  { exact pow_le_pow_swap ((by norm_num1 : _ ≤ _).trans (nat.pow_le_pow_of_le_left h₂ 2)) h₁ },
  rw [←pow_mul, ←sq, pow_right_comm _ n],
  apply h₃.trans,
  apply nat.pow_le_pow_of_le_left (sq_le_two_pow h₂),
end

[Bhavik Mehta]

I think some of the hypotheses can be slightly generalised, but here's your original question!

[Bolton Bailey]

Interestingly, the log x / x decreasing proof doesn't actually depend on calculus, you can see it here: #10985. (Credit to Mario for this proof).

[Bhavik Mehta]

It vitally uses add_one_le_exp, which I think goes via the Taylor series for the exponential?

[Kevin Buzzard]

In some sense log depends on calculus, because the base e is a limit. I bet natural log didn't exist before calculus

[Yakov Pechersky]

I use log all the time without calculus, I just count the number of digits in my number.

[Kevin Buzzard]

Sure but that's not the right log here

[Bolton Bailey]

I guess I should say that the proof depends on limits, but not on differentiation.

[Pascal Schoppenhauer]

This is awesome guys I love you all. :kiss_with_blush:

[Yaël Dillies]

Congrats to @Yevhenii Diomidov for getting it without the reals! https://gist.github.com/diomidov/d328e181d196bf4c1517beb27ae5f0ca

[Pascal Schoppenhauer]

Ok thanks again, but I have a few questions:

1. What does linarith/nlinarith do? They "solve (non-) linear arithmetic problems", but how?
2. I understand @Bhavik Mehta's approach. I don't see why they are switching to ℝ and why we want to try to avoid this.
3. I don't fully understand @Yevhenii Diomidov's approach, but the code looks very different from what I have seen so far. It feels like they are writing down "where" they want to go and not just "how". How is this style of code called / where can I read more about this?
4. What does .trans do? It's used a lot, but I can't seem to find out what it does.
5. Everyone seems to be very confident using abbreviations. Is there a naming convention I can look at? Because sometimes it isn't intuitive. (Especially because english isn't my first language...)

[Kevin Buzzard]

1. I think linarith etc uses Fourier-Motzkin elimination? Why do you want to know? I have no idea how it works, I just use it.

2. y^x<=x^y for e<=x<=y is not so hard to prove over the reals, but seems harder to prove over the naturals.

3. x.trans depends on the type of x. For example if x : a = b then x.trans means eq.trans x, and eq.trans is the theorem that if a=b and b=c then a=c.

4. #naming

[Pascal Schoppenhauer]

Thanks a lot. I really appreciate it.

1. I just wanted to know how it's called so that I can reference it. Thanks!
2. yeah but why exactly?
   (My question 3 is unanswered)

[Ruben Van de Velde]

nat.log exists, but returns a natural number, so essentially a rounded version of the "actual" logarithm. That means it doesn't have quite the same properties

[Pascal Schoppenhauer]

Ok, that makes sense. Is it taboo to switch to a different number set to prove something?

[Ruben Van de Velde]

Not taboo, but it can be interesting to see if you can get there in a more "low-tech" way

[Kevin Buzzard]

If you "view source" of my message you can see I wrote "1,2,4,5" but Zulip is rendering them as "1,2,3,4". Surprising!

[Julian Berman]

You can thank markdown.

[Eric Rodriguez]

yeah, that's been an annoyance with markdown forever. always great when someone asks sth like "how old are you?" and someone answers:

[Eric Rodriguez]

21. I am that age years old

[Eric Rodriguez]

Oh, it doesn't seem to happen for single-item lists here. It does on Reddit

[Julian Berman]

1\. This
2\. Maybe
7\. Works
Experiment failed.

[Pascal Schoppenhauer]

Ok guys I am still confused about this:
after line 39 of @Bhavik Mehta's code the proof state looks like this:

h₃: n ^ m ^ 2 ≤ (m ^ 2) ^ n          -- A ≤ B
⊢ n ^ m ^ 2 ≤ (2 ^ m) ^ n            -- A ≤ C

And after applying h3.trans the proof state looks like this:

h₃: n ^ m ^ 2 ≤ (m ^ 2) ^ n          -- A ≤ B
⊢ (m ^ 2) ^ n ≤ (2 ^ m) ^ n         -- B ≤ C

If it was an equality it would make sense to me, but with the < sign I can't comprehend it.

[Kevin Buzzard]

Do you understand it the other way? If the goal is X and you apply a tactic and the goal changes to Y, then lean is saying that from Y and the hypotheses it can deduce X. Do you see how?

[Pascal Schoppenhauer]

yes now I see it xD. But it is confusing tho. Because just from looking at the first state proof there might be cases where B > C

[Yaël Dillies]

We're changing the goal, not what we proved. So it might still be the case that C < B. It's just that we went from trying to prove A ≤ C to trying to prove B ≤ C.

[Reid Barton]

Pascal Schoppenhauer said:

Because just from looking at the first state proof there might be cases where B > C

If so then tough luck and we won't be able to finish the proof this way, and we'll have to try something else instead of using h3.trans.

[Pascal Schoppenhauer]

Math is mindblowing :hurt: I feel like I would need ages to figure this stuff out

[Pascal Schoppenhauer]

Thanks tho I get it now

[Pascal Schoppenhauer]

I have another question: in line 38 what do the { } do?
And what's norm_num1?

[Kevin Buzzard]

Maybe work through the tutorial? https://github.com/leanprover-community/tutorials

[Pascal Schoppenhauer]

Thanks, I'll try this.

[Patrick Johnson]

off-topic:

͏1͏. one
͏2͏. two
͏4͏. four
͏5͏. five
͏7͏. seven

[Patrick Johnson]

Numbering works as expected.