El límite de uₙ es a syss el de uₙ-a es 0
Demostrar con Lean4 que el límite de \(uₙ\) es \(a\) si, y sólo si, el de \(uₙ-a\) es \(0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a c x : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by sorry |
1. Demostración en lenguaje natural
Se prueba por la siguiente cadena de equivalencias
\begin{align}
&\text{el límite de \(uₙ\) es \(a\)} \\
&↔ (∀ε>0)(∃N)(∀n≥N)[|u(n) – a| < ε] \\
&↔ (∀ε>0)(∃N)(∀n≥N)[|(u(n) – a) – 0| < ε] \\
&↔ \text{el límite de \(uₙ-a\) es \(0\)}
\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 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} variable {a c x : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by rw [iff_eq_eq] calc limite u a = ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε := rfl _ = ∀ ε > 0, ∃ N, ∀ n ≥ N, |(u n - a) - 0| < ε := by simp _ = limite (fun i ↦ u i - a) 0 := rfl -- 2ª demostración -- =============== example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by constructor . -- ⊢ limite u a → limite (fun i => u i - a) 0 intros h ε hε -- h : limite u a -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun i => u i - a) n - 0| < ε convert h ε hε using 2 -- x : ℕ -- ⊢ (∀ (n : ℕ), n ≥ x → |(fun i => u i - a) n - 0| < ε) ↔ ∀ (n : ℕ), n ≥ x → |u n - a| < ε norm_num . -- ⊢ limite (fun i => u i - a) 0 → limite u a intros h ε hε -- h : limite (fun i => u i - a) 0 -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε convert h ε hε using 2 -- x : ℕ -- ⊢ (∀ (n : ℕ), n ≥ x → |u n - a| < ε) ↔ ∀ (n : ℕ), n ≥ x → |(fun i => u i - a) n - 0| < ε norm_num -- 3ª demostración -- =============== example : limite u a ↔ limite (fun i ↦ u i - a) 0 := by constructor <;> { intros h ε hε convert h ε hε using 2 norm_num } -- 4ª demostración -- =============== lemma limite_con_suma (c : ℝ) (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := fun ε hε ↦ (by convert h ε hε using 2; norm_num) lemma CNS_limite_con_suma (c : ℝ) : limite u a ↔ limite (fun i ↦ u i + c) (a + c) := by constructor . -- ⊢ limite u a → limite (fun i => u i + c) (a + c) apply limite_con_suma . -- ⊢ limite (fun i => u i + c) (a + c) → limite u a intro h -- h : limite (fun i => u i + c) (a + c) -- ⊢ limite u a convert limite_con_suma (-c) h using 2 . -- ⊢ u x = u x + c + -c simp . -- ⊢ a = a + c + -c simp example (u : ℕ → ℝ) (a : ℝ) : limite u a ↔ limite (fun i ↦ u i - a) 0 := by convert CNS_limite_con_suma (-a) using 2 -- ⊢ 0 = a + -a simp -- Lemas usados -- ============ -- variable (p q : Prop) -- #check (iff_eq_eq : (p ↔ q) = (p = q)) |
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 37 38 39 40 41 42 43 44 45 |
theory "El_limite_de_u_es_a_syss_el_de_u-a_es_0" imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" (* 1ª demostración *) lemma "limite u a ⟷ limite (λ i. u i - a) 0" proof - have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)" by (rule limite_def) also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)" by simp also have "… ⟷ limite (λ i. u i - a) 0" by (rule limite_def[symmetric]) finally show "limite u a ⟷ limite (λ i. u i - a) 0" by this qed (* 2ª demostración *) lemma "limite u a ⟷ limite (λ i. u i - a) 0" proof - have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)" by (simp only: limite_def) also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)" by simp also have "… ⟷ limite (λ i. u i - a) 0" by (simp only: limite_def) finally show "limite u a ⟷ limite (λ i. u i - a) 0" by this qed (* 3ª demostración *) lemma "limite u a ⟷ limite (λ i. u i - a) 0" using limite_def by simp end |
