Reto 14: Para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴
El reto de esta semana consiste en demostrar en Lean 4, para todo \(n \in ℕ\), \(2n + 9 ≤ 2^{n+4}\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic variable (n : ℕ) example : 2 * n + 9 ≤ 2 ^ (n + 4) := by sorry
1. Demostración en lenguaje natural
Por inducción en \(n\).
Caso base: Para \(n = 0\) se tiene: \[ \begin{array}{ll} 2 \times 0 + 9 &= 9 \\ &≤ 16 \\ &= 2^{0+4} \end{array} \]
Paso inductivo: Suponiendo la hipótesis de inducción \[ 2k + 9 ≤ 2^{k+4} \tag{HI} \] tenemos que demostrar que \[ 2(k+1) + 9 ≤ 2^{(k+1)+4)} \]
Puesto que \(k \geq 0\), se tiene que \[ 2 ≤ 2^{k+4} \tag{1} \] Efectivamente, \[ \begin{array}{ll} 2 &≤ 16 \\ &= 2^{4} \\ &≤ 2^{k+4} \end{array} \]
Finalmente, \[ \begin{array}{llll} 2(k + 1) + 9 &= (2k + 9) + 2 \\ &≤ 2^{k+4} + 2 &&\text{[por HI]} \\ &≤ 2^{k+4} + 2^{k+4} &&\text{[por (1)]} \\ &= 2 \times 2^{k+4} \\ &= 2^{(k+1)+4)} \end{array} \]
2. Demostraciones con Lean 4
import Mathlib.Tactic variable (n : ℕ) -- 1ª demostración -- =============== example : 2 * n + 9 ≤ 2 ^ (n + 4) := by induction n with | zero => -- ⊢ 2 * 0 + 9 ≤ 2 ^ (0 + 4) grind | succ k HI => -- k : ℕ -- HI : 2 * k + 9 ≤ 2 ^ (k + 4) -- ⊢ 2 * (k + 1) + 9 ≤ 2 ^ (k + 1 + 4) grind -- 2ª demostración -- =============== example : 2 * n + 9 ≤ 2 ^ (n + 4) := by induction n <;> grind -- 3ª demostración -- =============== example : 2 * n + 9 ≤ 2 ^ (n + 4) := by induction n with | zero => -- ⊢ 2 * 0 + 9 ≤ 2 ^ (0 + 4) grind | succ k HI => -- k : ℕ -- HI : 2 * k + 9 ≤ 2 ^ (k + 4) -- ⊢ 2 * (k + 1) + 9 ≤ 2 ^ (k + 1 + 4) calc 2 * (k + 1) + 9 = (2 * k + 9) + 2 := by grind _ ≤ 2 ^ (k + 4) + 2 := by grind _ ≤ 2 ^ (k + 4) + 2 ^ (k + 4) := by grind _ = 2 * 2 ^ (k + 4) := by grind _ = 2 ^ (k + 1 + 4) := by grind -- 4ª demostración -- =============== example : 2 * n + 9 ≤ 2 ^ (n + 4) := by induction n with | zero => -- ⊢ 2 * 0 + 9 ≤ 2 ^ (0 + 4) norm_num | succ k HI => -- k : ℕ -- HI : 2 * k + 9 ≤ 2 ^ (k + 4) -- ⊢ 2 * (k + 1) + 9 ≤ 2 ^ (k + 1 + 4) calc 2 * (k + 1) + 9 = (2 * k + 9) + 2 := by ring _ ≤ 2 ^ (k + 4) + 2 := Nat.add_le_add_right HI 2 _ ≤ 2 ^ (k + 4) + 2 ^ (k + 4) := Nat.add_le_add_left (by bound) (2 ^ (k + 4)) _ = 2 * 2 ^ (k + 4) := by ring _ = 2 ^ (k + 1 + 4) := by ring -- 5ª demostración -- =============== example : 2 * n + 9 ≤ 2 ^ (n + 4) := by induction n with | zero => -- ⊢ 2 * 0 + 9 ≤ 2 ^ (0 + 4) calc 2 * 0 + 9 = 9 := by norm_num _ ≤ 16 := by norm_num _ = 2 ^ (0 + 4) := by norm_num | succ k HI => -- k : ℕ -- HI : 2 * k + 9 ≤ 2 ^ (k + 4) -- ⊢ 2 * (k + 1) + 9 ≤ 2 ^ (k + 1 + 4) have h1 : 2 ≤ 2 ^ (k + 4) := by calc 2 ≤ 16 := by norm_num _ = 2 ^ 4 := by norm_num _ ≤ 2 ^ (k + 4) := Nat.pow_le_pow_of_le one_lt_two (Nat.le_add_left 4 k) calc 2 * (k + 1) + 9 = (2 * k + 2) + 9 := congrArg (· + 9) (Nat.mul_succ 2 k) _ = (2 * k + 9) + 2 := Nat.add_right_comm (2 * k) 2 9 _ ≤ 2 ^ (k + 4) + 2 := Nat.add_le_add_right HI 2 _ ≤ 2 ^ (k + 4) + 2 ^ (k + 4) := Nat.add_le_add_left h1 (2 ^ (k + 4)) _ = 2 * 2 ^ (k + 4) := (Nat.two_mul (2 ^ (k + 4))).symm _ = 2 ^ (k + 1 + 4) := Nat.pow_succ'.symm -- Lemas usados -- ============ variable (k m : ℕ) #check (Nat.add_le_add_left : n ≤ m → ∀ k, k + n ≤ k + m) #check (Nat.add_le_add_right : n ≤ m → ∀ k, n + k ≤ m + k) #check (Nat.add_left_inj : m + n = k + n ↔ m = k) #check (Nat.le_add_left n m : n ≤ m + n) #check (Nat.pow_succ' : m ^ n.succ = m * m ^ n) #check (Nat.two_mul n : 2 * n = n + n) #check (one_le_two : 1 ≤ 2) #check (pow_le_pow_right' : 1 ≤ k → n ≤ m → k ^ n ≤ k ^ m)
En el siguiente vídeo se explica paso a paso la construcción de las soluciones:
Es posible consultar, modificar y ejecutar el código de estas demostraciones de forma interactiva en Lean 4 Web.