Challenge 15: There exists k ∈ ℕ such that, for all n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ
Prove that there exists \(k ∈ ℕ\) such that, for all \(n \in ℕ\), \((n + k)^{2} ≤ 2^{n+k}\).
To do so, complete the following Lean 4 theory:
import Mathlib.Tactic example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n + k) := by sorry
1. Proof in natural language
Proof 1
We first prove the following auxiliary lemma: for all \(m \geq 4\), we have \(m^2 ≤ 2^m\). Let \(m \in \mathbb{N}\); we have to prove that \[ m \geq 4 → m^2 ≤ 2^m \] We prove it by induction on \(m\).
Base case: for \(m = 0\) we trivially have \[ 0 \geq 4 → 0^2 ≤ 2^0 \]
Inductive step: let \(n \in \mathbb{N}\) satisfy the induction hypothesis; that is, \[ n \geq 4 → n ^ 2 ≤ 2 ^ n \tag{IH} \] and we have to prove that \[ n + 1 \geq 4 → (n + 1)^2 ≤ 2^{n + 1} \] Assuming that \[ n + 1 \geq 4 \tag{1} \] we have to prove that \[ (n + 1)^2 ≤ 2^{n + 1} \] We proceed by cases on \(4 ≤ n\).
First case: assume that \[ 4 ≤ n \tag{2} \] Then, we prove that \[ 2n + 1 ≤ n^2 \tag{3} \] Indeed, \[ \begin{array}{llll} 2n + 1 &≤ 2n + 8 \\ &≤ 2n + 2n &&\text{[by (2)]} \\ &= 4n \\ &≤ nn &&\text{[by (2)]} \\ &= n ^ 2 \end{array} \] Therefore, \[ \begin{array}{llll} (n + 1) ^ 2 &= n ^ 2 + 2n + 1 \\ &≤ n ^ 2 + n ^ 2 &&\text{[by (3)]} \\ &= 2n ^ 2 \\ &≤ 2 \times 2 ^ n &&\text{[by IH and (2)]} \\ &= 2 ^{n + 1} \end{array} \]
Second case: assume that \[ ¬ (4 ≤ n) \] Then, by (1), we have \[ n = 3 \] and \[ \begin{array}{ll} (n + 1) ^ 2 &= (3 + 1) ^ 2 \\ &= 16 \\ &≤ 2 ^{3 + 1} \\ &= 2 ^{n + 1} \end{array} \]
To conclude the proof of the exercise \[ \exists k, \forall n, (n + k) ^ 2 ≤ 2 ^ {n + k} \] it is enough to take 4 as k, which leaves us with \[ \forall n, (n + 4) ^ 2 ≤ 2 ^ {n + 4} \] and this follows from the auxiliary lemma. Indeed, let \(n \in \mathbb{N}\). Then, \[ n + 4 \geq 4 \] and, by the auxiliary lemma, \[ (n + 4) ^ 2 ≤ 2 ^ {n + 4} \]
Proof 2
We first prove the following auxiliary lemma: for all \(m \geq 4\), we have \(m^2 ≤ 2^m\). Let \(m \in \mathbb{N}\) be such that \[ m \geq 4 \] we have to prove that \[ m ^ 2 ≤ 2 ^ m \] We prove it by generalized induction on \(m\), starting from 4.
Base case: for \(m = 4\) we trivially have \[ 4 ^ 2 ≤ 2 ^ 4 \]
Inductive step: let \(n \in \mathbb{N}\) be such that \[ 4 ≤ n \tag{1} \] and which satisfies the induction hypothesis; that is, \[ n ^ 2 ≤ 2 ^ n \tag{IH} \] and we have to prove that \[ (n + 1) ^ 2 ≤ 2 ^ {n + 1} \] First, we prove that \[ 2n + 1 ≤ n ^ 2 \tag{2} \] Indeed, \[ \begin{array}{llll} 2n + 1 &≤ 2n + 8 \\ &≤ 2n + 2n &&\text{[by (1)]} \\ &= 4n \\ &≤ n \times n &&\text{[by (1)]} \\ &= n ^ 2 \end{array} \] Therefore, \[ \begin{array}{llll} (n + 1) ^ 2 &= n ^ 2 + 2n + 1 \\ &≤ n ^ 2 + n ^ 2 &&\text{[by (2)]} \\ &= 2n ^ 2 \\ &≤ 2 \times 2 ^ n &&\text{[by IH]} \\ &= 2 ^ {n + 1} \end{array} \]
To conclude the proof of the exercise \[ \exists k, \forall n, (n + k) ^ 2 ≤ 2 ^ {n + k} \] it is enough to take \(4\) as \(k\), which leaves us with \[ \forall n, (n + 4) ^ 2 ≤ 2 ^ {n + 4} \] and this follows from the auxiliary lemma. Indeed, let \(n \in \mathbb{N}\). Then, \[ n + 4 \geq 4 \] and, by the auxiliary lemma, \[ (n + 4) ^ 2 ≤ 2 ^ {n + 4} \]
2. Proofs in Lean 4
import Mathlib.Tactic -- Solution 1 -- ========== namespace Solution1 lemma aux : ∀ m ≥ 4, m ^ 2 ≤ 2 ^ m := by intro m -- m : ℕ -- ⊢ m ≥ 4 → m ^ 2 ≤ 2 ^ m induction m with | zero => -- ⊢ 0 ≥ 4 → 0 ^ 2 ≤ 2 ^ 0 grind | succ n hi => -- n : ℕ -- hi : n ≥ 4 → n ^ 2 ≤ 2 ^ n -- ⊢ n + 1 ≥ 4 → (n + 1) ^ 2 ≤ 2 ^ (n + 1) intro hn1 -- hn1 : n + 1 ≥ 4 by_cases hn : 4 ≤ n · -- hn : 4 ≤ n have h1 : 2 * n + 1 ≤ n ^ 2 := by calc 2 * n + 1 ≤ 2 * n + 8 := by grind _ ≤ 2 * n + 2 * n := by grind _ = 4 * n := by grind _ ≤ n * n := by gcongr _ = n ^ 2 := by grind calc (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by grind _ ≤ n ^ 2 + n ^ 2 := Nat.add_le_add_left h1 (n ^ 2) _ = 2 * n ^ 2 := by grind _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 (hi hn) _ = 2 ^ (n + 1) := by ring · -- hn : ¬4 ≤ n have hn3 : n = 3 := by grind subst hn3 -- ⊢ (3 + 1) ^ 2 ≤ 2 ^ (3 + 1) norm_num example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n + k) := by use 4 -- ⊢ ∀ (n : ℕ), (n + 4) ^ 2 ≤ 2 ^ (n + 4) intro n -- ⊢ (n + 4) ^ 2 ≤ 2 ^ (n + 4) exact aux (n + 4) (by grind) end Solution1 -- Solution 2 -- ========== namespace Solution2 lemma aux : ∀ m ≥ 4, m ^ 2 ≤ 2 ^ m := by intro m hm -- m : ℕ -- hm : m ≥ 4 -- ⊢ m ^ 2 ≤ 2 ^ m induction m, hm using Nat.le_induction with | base => -- ⊢ 4 ^ 2 ≤ 2 ^ 4 grind | succ n hn hi => -- n : ℕ -- hn : 4 ≤ n -- hi : n ^ 2 ≤ 2 ^ n -- ⊢ (n + 1) ^ 2 ≤ 2 ^ (n + 1) have h1 : 2 * n + 1 ≤ n ^ 2 := by calc 2 * n + 1 ≤ 2 * n + 8 := by grind _ ≤ 2 * n + 2 * n := by grind _ = 4 * n := by grind _ ≤ n * n := by gcongr _ = n ^ 2 := by grind calc (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by grind _ ≤ n ^ 2 + n ^ 2 := Nat.add_le_add_left h1 (n ^ 2) _ = 2 * n ^ 2 := by grind _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 hi _ = 2 ^ (n + 1) := by ring example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n + k) := by use 4 -- ⊢ ∀ (n : ℕ), (n + 4) ^ 2 ≤ 2 ^ (n + 4) intro n -- ⊢ (n + 4) ^ 2 ≤ 2 ^ (n + 4) exact aux (n + 4) (by grind) end Solution2 -- Solution 3 -- ========== namespace Solution3 lemma aux : ∀ m ≥ 4, m ^ 2 ≤ 2 ^ m := by intro m hm -- m : ℕ -- hm : m ≥ 4 -- ⊢ m ^ 2 ≤ 2 ^ m induction m, hm using Nat.le_induction with | base => -- ⊢ 4 ^ 2 ≤ 2 ^ 4 norm_num | succ n hn hi => -- n : ℕ -- hn : 4 ≤ n -- hi : n ^ 2 ≤ 2 ^ n -- ⊢ (n + 1) ^ 2 ≤ 2 ^ (n + 1) have h1 : 2 * n + 1 ≤ n ^ 2 := by calc 2 * n + 1 ≤ 2 * n + 8 := by omega _ ≤ 2 * n + 2 * n := by omega _ = 4 * n := by ring _ ≤ n * n := by gcongr _ = n ^ 2 := by ring calc (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by ring _ ≤ n ^ 2 + n ^ 2 := Nat.add_le_add_left h1 (n ^ 2) _ = 2 * n ^ 2 := by ring _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 hi _ = 2 ^ (n + 1) := by ring example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n + k) := by use 4 -- ⊢ ∀ (n : ℕ), (n + 4) ^ 2 ≤ 2 ^ (n + 4) intro n -- ⊢ (n + 4) ^ 2 ≤ 2 ^ (n + 4) exact aux (n + 4) (by omega) end Solution3 -- Solution 4 -- ========== namespace Solution4 lemma aux : ∀ m ≥ 4, m ^ 2 ≤ 2 ^ m := by intro m hm -- m : ℕ -- hm : m ≥ 4 -- ⊢ m ^ 2 ≤ 2 ^ m induction m, hm using Nat.le_induction with | base => -- ⊢ 4 ^ 2 ≤ 2 ^ 4 norm_num | succ n hn hi => -- n : ℕ -- hn : 4 ≤ n -- hi : n ^ 2 ≤ 2 ^ n -- ⊢ (n + 1) ^ 2 ≤ 2 ^ (n + 1) have h1 : 2 * n + 1 ≤ n ^ 2 := by calc 2 * n + 1 ≤ 2 * n + 8 := Nat.add_le_add_iff_left.mpr (by norm_num) _ = 2 * n + 2 * 4 := Nat.add_left_inj.mpr rfl _ ≤ 2 * n + 2 * n := Nat.add_le_add_iff_left.mpr (Nat.mul_le_mul_left 2 hn) _ = (2 + 2) * n := (Nat.add_mul 2 2 n).symm _ = 4 * n := congrArg (· * n) (Nat.succ_add 1 2) _ ≤ n * n := Nat.mul_le_mul_right n hn _ = n ^ 2 := (Nat.pow_two n).symm calc (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by ring _ ≤ n ^ 2 + n ^ 2 := Nat.add_le_add_left h1 (n ^ 2) _ = 2 * n ^ 2 := (Nat.two_mul (n ^ 2)).symm _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 hi _ = 2 ^ (n + 1) := Nat.pow_succ'.symm example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n + k) := ⟨4, fun n => aux (n + 4) (by omega)⟩ end Solution4 -- Lemmas used -- =========== variable (n m k : ℕ) #check (Nat.add_le_add_iff_left : n + m ≤ n + k ↔ m ≤ k) #check (Nat.add_le_add_left : n ≤ m → ∀ k, k + n ≤ k + m) #check (Nat.add_left_inj : m + n = k + n ↔ m = k) #check (Nat.add_mul n m k : (n + m) * k = n * k + m * k) #check (Nat.mul_le_mul_left k : n ≤ m → k * n ≤ k * m) #check (Nat.mul_le_mul_right k : n ≤ m → n * k ≤ m * k) #check (Nat.pow_succ' : m ^ n.succ = m * m ^ n) #check (Nat.pow_two n : n ^ 2 = n * n) #check (Nat.succ_add n m : n.succ + m = (n + m).succ) #check (Nat.two_mul n : 2 * n = n + n)
You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.
3. Collaborative solutions
Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:
- Write your proof in live.lean-lang.org and check that it compiles without errors.
- Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean -- your proof ```
Comments