Las sucesiones convergentes están acotadas
Demostrar que si u es una sucesión convergente, entonces está acotada; es decir,
1 |
∃ k b, ∀ n, n ≥ k → |u n| ≤ b |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 |
import data.real.basic variable {u : ℕ → ℝ} variable {a : ℝ} notation `|`x`|` := abs x -- (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 := sorry |
[expand title=»Soluciones con Lean»]
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 |
import data.real.basic variable {u : ℕ → ℝ} variable {a : ℝ} notation `|`x`|` := abs x -- (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 := begin cases h with a ua, cases ua 1 zero_lt_one with k h, use [k, 1 + |a|], intros n hn, specialize h n hn, 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 _ end -- 2ª demostración example (h : convergente u) : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b := begin cases h with a ua, cases ua 1 zero_lt_one with k h, use [k, 1 + |a|], intros n hn, specialize h n hn, calc |u n| = |u n - a + a| : by ring_nf ... ≤ |u n - a| + |a| : abs_add (u n - a) a ... ≤ 1 + |a| : by linarith, end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones 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 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 |
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 (* 2ª 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¦" using hk by fastforce then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b" by auto qed end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]