Las sucesiones convergentes están acotadas
Demostrar con Lean4 que si \(u_n\) es una sucesión convergente, entonces está acotada; es decir,
\[ (∃ k ∈ ℕ)(∃ b ∈ ℝ)(∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ b] \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} -- (limite u c) expresa que el límite de u es c. def limite (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε -- (convergente u) expresa que u es convergente. def convergente (u : ℕ → ℝ) := ∃ a, limite u a example (h : convergente u) : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b := by sorry |
1. Demostración en lenguaje natural
Puesto que la sucesión \(u_n\) es convergente, existe un \(a ∈ ℝ\) tal que
\[ \lim(u_n) = a \]
Luego, existe un \(k ∈ ℕ\) tal que
\[ (∀ n ∈ ℕ)[n ≥ k → |u_n – a | < 1] \tag{1} \]
Veamos que
\[ (∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ 1 + |a]] \]
Para ello, sea \(n ∈ ℕ\) tal que
\[ n ≥ k \tag{2} \]
Entonces,
\begin{align}
|u_n| &= |u_n – a + a| \\
&≤ |u_n – a| + |a| \\
&≤ 1 + |a| &&\text{[por (1) y (2)]}
\end{align}
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} -- (limite u c) expresa que el límite de u es c. def limite (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε -- (convergente u) expresa que u es convergente. def convergente (u : ℕ → ℝ) := ∃ a, limite u a -- 1ª demostración -- =============== example (h : convergente u) : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b := by cases' h with a ua -- a : ℝ -- ua : limite u a cases' ua 1 zero_lt_one with k h -- k : ℕ -- h : ∀ (n : ℕ), n ≥ k → |u n - a| ≤ 1 use k, 1 + |a| -- ⊢ ∀ (n : ℕ), n ≥ k → |u n| ≤ 1 + |a| intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |u n| ≤ 1 + |a| specialize h n hn -- ⊢ |u n| ≤ 1 + |a| calc |u n| = |u n - a + a| := congr_arg abs (eq_add_of_sub_eq rfl) _ ≤ |u n - a| + |a| := abs_add (u n - a) a _ ≤ 1 + |a| := add_le_add_right h |a| -- 2ª demostración -- =============== example (h : convergente u) : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b := by cases' h with a ua -- a : ℝ -- ua : limite u a cases' ua 1 zero_lt_one with k h -- k : ℕ -- h : ∀ (n : ℕ), n ≥ k → |u n - a| ≤ 1 use k, 1 + |a| -- ⊢ ∀ (n : ℕ), n ≥ k → |u n| ≤ 1 + |a| intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |u n| ≤ 1 + |a| specialize h n hn -- h : |u n - a| ≤ 1 calc |u n| = |u n - a + a| := by ring_nf _ ≤ |u n - a| + |a| := abs_add (u n - a) a _ ≤ 1 + |a| := by linarith -- Lemas usados -- ============ -- variable (a b c : ℝ) -- #check (abs_add a b : |a + b| ≤ |a| + |b|) -- #check (add_le_add_right : b ≤ c → ∀ a, b + a ≤ c + a) -- #check (eq_add_of_sub_eq : a - c = b → a = b + c) -- #check (zero_lt_one : 0 < 1) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 |
theory Acotacion_de_convergentes imports Main HOL.Real begin (* (limite u c) expresa que el límite de u es c. *) definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)" (* (convergente u) expresa que u es convergente. *) definition convergente :: "(nat ⇒ real) ⇒ bool" where "convergente u ⟷ (∃ a. limite u a)" (* 1ª demostración *) lemma assumes "convergente u" shows "∃ k b. ∀n≥k. ¦u n¦ ≤ b" proof - obtain a where "limite u a" using assms convergente_def by blast then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1" using limite_def zero_less_one by blast have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦" proof (intro allI impI) fix n assume hn : "n ≥ k" have "¦u n¦ = ¦u n - a + a¦" by simp also have "… ≤ ¦u n - a¦ + ¦a¦" by simp also have "… ≤ 1 + ¦a¦" by (simp add: hk hn) finally show "¦u n¦ ≤ 1 + ¦a¦" . qed then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b" by (intro exI) qed end |
