Struggling with simple Lemma: 3^k > 2^(k+1), k >= 2

Stream: general

[Tristan Stérin]

Hello all :)

I'm quite new to Lean and I'm struggling to prove the following simple lemma:

lemma power_growth
  (k : ℕ) (hk : k ≥ 2) :
  (3 : ℤ)^k > (2 : ℤ)^(k+1)

The proof is simple in theory because the goal amounts to proving $(3/2)^k > 2$ , and $(3/2)^k$ is an increasing function of $k$ and we have $(3/2)^2 = 2.25 > 2$.

Would you have recommendations to help prove this :)

Thank you!

[Etienne Marion]

I think the easiest way is to do induction

[Robin Arnez]

The easiest way is:

theorem power_growth
    (k : Nat) (hk : k ≥ 2) :
    (3 : Int)^k > (2 : Int)^(k+1) := by
  norm_cast
  obtain ⟨a, rfl⟩ := Nat.exists_eq_add_of_le' hk
  simp only [Nat.pow_succ, Nat.mul_assoc, Nat.reduceMul]
  apply Nat.mul_lt_mul_of_le_of_lt
  · apply Nat.pow_le_pow_left
    decide
  · decide
  · apply Nat.pow_pos
    decide

[Robin Arnez]

i.e. instead of what you outlined, the proof is:
We know that k ≥ 2, thus there exists a natural number a such that a + 2 = k. (Nat.exists_eq_add_of_le' hk)
By substituting the equality (rfl), the goal becomes 3 ^ (a + 2) > 2 ^ (k + 3).
3 ^ (a + 2) = 3 ^ a * 9 and 2 ^ (k + 3) = 2 ^ k * 8 (simp only [Nat.pow_succ, Nat.mul_assoc, Nat.reduceMul]) so we only need to prove that 3 ^ a * 9 > 2 ^ k * 8.
This is trivial to solve using monotonicity of * and ^ (apply Nat.mul_lt_mul_of_le_of_lt, apply Nat.pow_le_pow_left).

[Robin Arnez]

If we want to follow your proof more closely:

import Mathlib

theorem power_growth
    (k : Nat) (hk : k ≥ 2) :
    (3 : Int)^k > (2 : Int)^(k+1) := by
  qify
  rw [pow_succ]
  rw [← lt_div_iff₀' (pow_pos two_pos k)]
  rw [← div_pow]
  obtain ⟨a, rfl⟩ := Nat.exists_eq_add_of_le' hk
  rw [pow_add]
  calc
    (2 : ℚ) < 1 * (3 / 2) ^ 2 := by norm_num
    1 * (3 / 2) ^ 2 ≤ (3 / 2) ^ a * (3 / 2) ^ 2 := by grw [one_le_pow₀ (a := 3 / 2) (by norm_num)]

(1. convert the problem to a problem on rational numbers (qify))

2. Rewrite 2 ^ (k + 1) = 2 ^ k * 2 (rw [pow_succ]). The goal is now 2 ^ k * 2 < 3 ^ k.
3. Since we know that 2 ^ k is positive (pow_pos two_pos k), we can move it over to the other side (rw [← lt_div_iff₀' (pow_pos two_pos k)])
4. Rewrite 3 ^ k / 2 ^ k = (3 / 2) ^ k (rw [← div_pow]). The goal is now 2 < (3 / 2) ^ k.
5. Since k >= 2, there exists an a such that k = a + 2. Substitute this equality (obtain ⟨a, rfl⟩ := Nat.exists_eq_add_of_le' hk).
6. Expand out (3 / 2) ^ (a + 2) to (3 / 2) ^ a * (3 / 2) ^ 2 (rw [pow_add]). The goal is now 2 < (3 / 2) ^ a * (3 / 2) ^ 2.
7. Then we apply transitivity of < and ≤. As the first step, we trivially know that 2 < 1 * (3 / 2) ^ 2 (norm_num).
8. Then 1 * (3 / 2) ^ 2 ≤ (3 / 2) ^ a * (3 / 2) ^ 2 holds by monotonicity of * and ^.

[Kevin Buzzard]

Robin Arnez said:

The easiest way is:

This is a way, but are you sure it's the easiest way? We have all these tools like grw and gcongr as of recently (but I'm not at a computer right now)

[Jeremy Tan]

Robin Arnez said:

The easiest way is:

theorem power_growth
    (k : Nat) (hk : k ≥ 2) :
    (3 : Int)^k > (2 : Int)^(k+1) := by
  norm_cast
  obtain ⟨a, rfl⟩ := Nat.exists_eq_add_of_le' hk
  simp only [Nat.pow_succ, Nat.mul_assoc, Nat.reduceMul]
  apply Nat.mul_lt_mul_of_le_of_lt
  · apply Nat.pow_le_pow_left
    decide
  · decide
  · apply Nat.pow_pos
    decide

import Mathlib.Data.Nat.Init

lemma power_growth (k : ℕ) (hk : k ≥ 2) : 3 ^ k > 2 ^ (k + 1) := by
  induction k, hk using Nat.le_induction <;> grind

(grind is a fairly new tactic that works like an extensible hammer for low-level subproofs)

[Kevin Buzzard]

Oh yeah and grind too :-)

[Tristan Stérin]

Thank you all for your answers!!

It really helps me with my understanding of Lean!

@Jeremy Tan : on my machine the code using grind fails with:

`grind` failed
case grind
k n : ℕ
hmn : 2 ≤ n
h : 2 ^ (n + 1) + 1 ≤ 3 ^ n
h_1 : 3 ^ (n + 1) ≤ 2 ^ (n + 2)
⊢ False
(trace)

Maybe it is because of my version of Lean:

lake --version
Lake version 5.0.0-src+6a60de2 (Lean version 4.22.0-rc2)

@Robin Arnez : thank you so much for giving me both proofs which is super helpful for making progress in my understanding.

Thanks to your help I was able to prove the last sorry in order to prove the following lemma (you are likely to find the proof horrendous, sorry):

lemma no_small_circuits
  (k: ℕ)
  (l: ℕ)
  (hk: k > 0)
  (hl: l > 0) :
  ((2 : ℤ)^k - 1)*2^l = (3 : ℤ)^k - 1 -> k = 1 ∧ l = 1 :=

Which is the first step for finishing the proof I'm currently working on, so really thank you again!