Reto 14: Para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴
Demostrar que, 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
Publicaciones sobre Lean4 (publicaciones antiguas, página 1)
Reto 13: Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|
Demostrar la desigualdad triangular inversa; es decir, que para cualesquiera números reales \(x\) e \(y\), se cumple la siguiente relación: \[ ||x| - |y|| ≤ |x - y| \]
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (x y : ℝ) example : |(|x| - |y|)| ≤ |x - y| := by sorry
Reto 12: Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ
Demostrar que si las sucesiones \(a_n\) y \(b_n\) convergen a \(L\) y \(M\), respectivamente, con \(L < M\), entonces eventualmente \(a_n < b_n\); es decir, que existe un \(k ∈ \mathbb{N}\) tal que, para todo \(n ≥ k\), \(a_n < b_n\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a b : ℕ → ℝ} variable {L M : ℝ} example (ha : SeqLim a L) (hb : SeqLim b M) (hLM : L < M) : ∃ k, ∀ n ≥ k, a n < b n := by sorry
Reto 11: Si aₙ converge a L, entonces |aₙ| converge a |L|
Demostrar que si la sucesión \(a_n\) converge a \(L\), entonces \(|a_n|\) converge a \(|L|\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a b : ℕ → ℝ} variable {L : ℝ} example (ha : SeqLim a L) (hb : ∀ n, b n = |a n|) : SeqLim b |L| := by sorry
Reto 10: Si aₙ → L con L ≠ 0, entonces |aₙ| ≥ |L|/2 eventualmente
Demostrar que si una sucesión converge a un límite no nulo, entonces sus términos están eventualmente acotados inferiormente por la mitad del valor absoluto del límite; es decir, si una sucesión \(a_n\) converge a \(L\) con \(L ≠ 0\), entonces existe \(k\) tal que para todo \(n ≥ k\) se tiene que \(|aₙ| ≥ \dfrac{|L|}{2}\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a : ℕ → ℝ} variable {L : ℝ} example (ha : SeqLim a L) (hL : L ≠ 0) : ∃ k, ∀ n ≥ k, |a n| ≥ |L| / 2 := by sorry
Reto 9: Unicidad del límite
El reto de esta semana consiste en demostrar en Lean 4 que si una sucesión \(aₙ\) converge tanto a \(L\) como a \(M\), entonces \(L = M\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a : ℕ → ℝ} variable {L M : ℝ} example (hL : SeqLim a L) (hM : SeqLim a M) : L = M := by sorry
Reto 8: Sucesiones con infinitos términos grandes no convergen a límites pequeños
Demostrar que una sucesión que posee infinitos términos con valor absoluto superior a 10 no puede converger a un límite cuyo valor absoluto sea menor que 5.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a : ℕ → ℝ} variable {L : ℝ} example (ha : ∀ k, ∃ n ≥ k, |a n| > 10) : ¬ ∃ L, SeqLim a L ∧ |L| < 5 := by sorry
Reto 7: La composición de funciones inyectivas es inyectiva
Demostrar que la composición de funciones inyectivas es inyectiva.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by sorry
Reto 6: Si aₙ y cₙ convergen a L y aₙ ≤ bₙ ≤ cₙ para todo n, entonces bₙ converge a L
Demostrar el teorema del emparedado; es decir que si \(a_n\) y \(c_n\) convergen a \(L\) y \(a_n ≤ b_n \leq c_n\) para todo \(n\), entonces \(b_n\) converge a \(L\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a b c : ℕ → ℝ} variable {L : ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) (hc : SeqLim c L) (hab : ∀ n, a n ≤ b n) (hbc : ∀ n, b n ≤ c n) : SeqLim b L := by sorry
Reto 5: 5²ⁿ - 2³ⁿ es divisible por 17
Demostrar en Lean 4 que, 5²ⁿ - 2³ⁿ es divisible por 17 para todo número natural n.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Nat.Basic import Mathlib.Tactic variable (n : ℕ) open Nat example : 17 ∣ 5^(2 * n) - 2^(3 * n) := by sorry