Si la sucesión u converge a a y la v a b, entonces u+v converge a a+b
Demostrar con Lean4 que si la sucesión \(u\) converge a \(a\) y la \(v\) a \(b\), entonces \(u+v\) converge a \(a+b\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {s t : ℕ → ℝ} {a b c : ℝ} def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by sorry
1. Demostración en lenguaje natural
En la demostración usaremos los siguientes lemas \begin{align} &(∀ a ∈ ℝ)\left[a > 0 → \frac{a}{2} > 0\right] \tag{L1} \newline &(∀ a, b, c ∈ ℝ)[\max(a, b) ≤ c → a ≤ c] \tag{L2} \newline &(∀ a, b, c ∈ ℝ)[\max(a, b) ≤ c → b ≤ c] \tag{L3} \newline &(∀ a, b ∈ ℝ)[|a + b| ≤ |a| + |b|] \tag{L4} \newline &(∀ a ∈ ℝ)\left[\frac{a}{2} + \frac{a}{2} = a\right] \tag{L5} \end{align}
Tenemos que probar que para todo \(ε ∈ ℝ\), si \[ ε > 0 \tag{1} \] entonces \[ (∃N ∈ ℕ)(∀n ∈ ℕ)[n ≥ N → |(u + v)(n) - (a + b)| < ε] \tag{2} \]
Por (1) y el lema L1, se tiene que \[ \frac{ε}{2} > 0 \tag{3} \] Por (3) y porque el límite de \(u\) es \(a\), se tiene que \[ (∃N ∈ ℕ)(∀n ∈ ℕ)\left[n ≥ N → |u(n) - a| < \frac{ε}{2}\right] \] Sea \(N₁ ∈ ℕ\) tal que \[ (∀n ∈ ℕ)\left[n ≥ N₁ → |u(n) - a| < \frac{ε}{2}\right] \tag{4} \] Por (3) y porque el límite de \(v\) es \(b\), se tiene que \[ (∃N ∈ ℕ)(∀n ∈ ℕ)\left[n ≥ N → |v(n) - b| < \frac{ε}{2}\right] \] Sea \(N₂ ∈ ℕ\) tal que \[ (∀n ∈ ℕ)\left[n ≥ N₂ → |v(n) - b| < \frac{ε}{2}\right] \tag{5} \] Sea \(N = \max(N₁, N₂)\). Veamos que verifica la condición (1). Para ello, sea \(n ∈ ℕ\) tal que \(n ≥ N\). Entonces, \(n ≥ N₁\) (por L2) y \(n ≥ N₂\) (por L3). Por tanto, usando las propiedades (4) y (5) se tiene que \begin{align} |u(n) - a| &< \frac{ε}{2} \tag{6} \newline |v(n) - b| &< \frac{ε}{2} \tag{7} \end{align} Finalmente, \begin{align} |(u + v)(n) - (a + b)| &= |(u(n) + v(n)) - (a + b)| \newline &= |(u(n) - a) + (v(n) - b)| \newline &≤ |u(n) - a| + |v(n) - b| &&\text{[por L4]}\newline &< \frac{ε}{2} + \frac{ε}{2} &&\text{[por (6) y (7)]}\newline &= ε &&\text{[por L5]} \end{align}
2. Demostraciones con Lean4
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {s t : ℕ → ℝ} {a b c : ℝ} def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε -- 1ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u + v) n - (a + b)| < ε have hε2 : 0 < ε / 2 := half_pos hε cases' hu (ε / 2) hε2 with Nu hNu -- Nu : ℕ -- hNu : ∀ (n : ℕ), n ≥ Nu → |u n - a| < ε / 2 cases' hv (ε / 2) hε2 with Nv hNv -- Nv : ℕ -- hNv : ∀ (n : ℕ), n ≥ Nv → |v n - b| < ε / 2 clear hu hv hε2 hε let N := max Nu Nv use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(s + t) n - (a + b)| < ε intros n hn -- n : ℕ -- hn : n ≥ N have nNu : n ≥ Nu := le_of_max_le_left hn specialize hNu n nNu -- hNu : |u n - a| < ε / 2 have nNv : n ≥ Nv := le_of_max_le_right hn specialize hNv n nNv -- hNv : |v n - b| < ε / 2 clear hn nNu nNv calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε / 2 + ε / 2 := by linarith [hNu, hNv] _ = ε := by apply add_halves -- 2ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε cases' hu (ε/2) (by linarith) with Nu hNu cases' hv (ε/2) (by linarith) with Nv hNv use max Nu Nv intros n hn have hn₁ : n ≥ Nu := le_of_max_le_left hn specialize hNu n hn₁ have hn₂ : n ≥ Nv := le_of_max_le_right hn specialize hNv n hn₂ calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by {congr; ring} _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε / 2 + ε / 2 := by linarith _ = ε := by apply add_halves -- 3ª demostración -- =============== lemma max_ge_iff {α : Type _} [LinearOrder α] {p q r : α} : r ≥ max p q ↔ r ≥ p ∧ r ≥ q := max_le_iff example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε cases' hu (ε/2) (by linarith) with Nu hNu cases' hv (ε/2) (by linarith) with Nv hNv use max Nu Nv intros n hn cases' max_ge_iff.mp hn with hn₁ hn₂ have cota₁ : |u n - a| < ε/2 := hNu n hn₁ have cota₂ : |v n - b| < ε/2 := hNv n hn₂ calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε := by linarith -- 4ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε cases' hu (ε/2) (by linarith) with Nu hNu cases' hv (ε/2) (by linarith) with Nv hNv use max Nu Nv intros n hn cases' max_ge_iff.mp hn with hn₁ hn₂ calc |(u + v) n - (a + b)| = |u n + v n - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε/2 + ε/2 := add_lt_add (hNu n hn₁) (hNv n hn₂) _ = ε := by simp -- 5ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε cases' hu (ε/2) (by linarith) with Nu hNu cases' hv (ε/2) (by linarith) with Nv hNv use max Nu Nv intros n hn rw [max_ge_iff] at hn calc |(u + v) n - (a + b)| = |u n + v n - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε := by linarith [hNu n (by linarith), hNv n (by linarith)] -- 6ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε Hε cases' hu (ε/2) (by linarith) with L HL cases' hv (ε/2) (by linarith) with M HM set N := max L M with _hN use N have HLN : N ≥ L := le_max_left _ _ have HMN : N ≥ M := le_max_right _ _ intros n Hn have H3 : |u n - a| < ε/2 := HL n (by linarith) have H4 : |v n - b| < ε/2 := HM n (by linarith) calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := by rfl _ = |(u n - a) + (v n - b)| := by {congr; ring } _ ≤ |(u n - a)| + |(v n - b)| := by apply abs_add _ < ε/2 + ε/2 := by linarith _ = ε := by ring -- Lemas usados -- ============ -- variable (d : ℝ) -- #check (abs_add a b : |a + b| ≤ |a| + |b|) -- #check (add_halves a : a / 2 + a / 2 = a) -- #check (add_lt_add : a < b → c < d → a + c < b + d) -- #check (half_pos : a > 0 → a / 2 > 0) -- #check (le_max_left a b : a ≤ max a b) -- #check (le_max_right a b : b ≤ max a b) -- #check (le_of_max_le_left : max a b ≤ c → a ≤ c) -- #check (le_of_max_le_right : max a b ≤ c → b ≤ c) -- #check (max_le_iff : max a b ≤ c ↔ a ≤ c ∧ b ≤ c)
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
theory Convergencia_de_la_suma 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 assumes "limite u a" "limite v b" shows "limite (λ n. u n + v n) (a + b)" proof (unfold limite_def) show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" then have "0 < ε/2" by simp then have "∃k. ∀n≥k. ¦u n - a¦ < ε/2" using assms(1) limite_def by blast then obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2" by (rule exE) then have "∃k. ∀n≥k. ¦v n - b¦ < ε/2" using ‹0 < ε/2› assms(2) limite_def by blast then obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2" by (rule exE) have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε" proof (intro allI impI) fix n :: nat assume "n ≥ max Nu Nv" have "¦(u n + v n) - (a + b)¦ = ¦(u n - a) + (v n - b)¦" by simp also have "… ≤ ¦u n - a¦ + ¦v n - b¦" by simp also have "… < ε/2 + ε/2" using hNu hNv ‹max Nu Nv ≤ n› by fastforce finally show "¦(u n + v n) - (a + b)¦ < ε" by simp qed then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε " by (rule exI) qed qed (* 2ª demostración *) lemma assumes "limite u a" "limite v b" shows "limite (λ n. u n + v n) (a + b)" proof (unfold limite_def) show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" then have "0 < ε/2" by simp obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2" using ‹0 < ε/2› assms(1) limite_def by blast obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2" using ‹0 < ε/2› assms(2) limite_def by blast have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε" using hNu hNv by (smt (verit, ccfv_threshold) field_sum_of_halves max.boundedE) then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε " by blast qed qed end