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 |
Demostrar con Lean4 que si el límite de la sucesión \(uₙ\) es \(a\) y \(c ∈ ℝ\), entonces el límite de \(cuₙ\) es \(ca\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u v : ℕ → ℝ) variable (a c : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by |
Read More «Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de cuₙ es ca»
Demostrar con Lean4 que si el límite de la sucesión \(uₙ\) es \(a\) y \(c ∈ ℝ\), entonces el límite de \(uₙ+c\) es \(a+c\).
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 : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : limite u a) : limite (fun i ↦ u i + c) (a + c) := by sorry |
Read More «Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de uₙ+c es a+c»
En Lean, una sucesión \(u₀, u₁, u₂, …\) se puede representar mediante una función \((u : ℕ → ℝ)\) de forma que \(u(n)\) es \(uₙ\).
Se define que \(a\) es el límite de la sucesión \(u\), por
|
1 2 |
def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε |
Demostrar con Lean4 que cada sucesión tiene como máximo un límite.
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 variable {u : ℕ → ℝ} variable {a b : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (ha : limite u a) (hb : limite u b) : a = b := by sorry |
Tenemos que demostrar que si \(u\) es una sucesión y \(a\) y \(b\) son límites de \(u\), entonces \(a = b\). Para ello, basta demostrar que \(a ≤ b\) y \(b ≤ a\).
Demostraremos que \(b ≤ a\) por reducción al absurdo. Supongamos que \(b ≰ a\). Sea \(ε = b – a\). Entonces, ε/2 > 0 y, puesto que \(a\) es un límite de \(u\), existe un \(A ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ A → |u(n) – a| < \frac{ε}{2}\right] \tag{1} \]
y, puesto que \(b\) también es un límite de \(u\), existe un \(B ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ B → |u(n) – b| < \frac{ε}{2}\right] \tag{2} \]
Sea \(N = máx(A, B)\). Entonces, \(N ≥ A\) y \(N ≥ B\) y, por (2) y (3), se tiene
\begin{align}
|u(N) – a| &< \frac{ε}{2} \tag{3} \\
|u(N) – b| &< \frac{ε}{2} \tag{4}
\end{align}
Para obtener una contradicción basta probar que \(ε < ε\). Su prueba es
\begin{align}
ε &= b – a \\
&= |b – a| \\
&= |(b – a) + (u(N) – u(N))| \\
&= |(u(N) – a) + (b – u(N))| \\
&≤ |u(N) – a| + |b – u(N)| \\
&= |u(N) – a| + |u(N) – b| \\
&< \frac{ε}{2} + \frac{ε}{2} && \text{[por (3) y (4)]} \\
&= ε
\end{align}
La demostración de \(a ≤ b\) es análoga a la anterior.
|
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 101 102 103 104 105 106 |
import Mathlib.Data.Real.Basic variable {u : ℕ → ℝ} variable {a b : ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración del lema auxiliar -- ================================= example (ha : limite u a) (hb : limite u b) : b ≤ a := by by_contra h -- h : ¬b ≤ a -- ⊢ False let ε := b - a have hε : ε > 0 := sub_pos.mpr (not_le.mp h) have hε2 : ε / 2 > 0 := half_pos hε cases' ha (ε/2) hε2 with A hA -- A : ℕ -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2 cases' hb (ε/2) hε2 with B hB -- B : ℕ -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2 let N := max A B have hAN : A ≤ N := le_max_left A B have hBN : B ≤ N := le_max_right A B specialize hA N hAN -- hA : |u N - a| < ε / 2 specialize hB N hBN -- hB : |u N - b| < ε / 2 have h2 : ε < ε := by calc ε = b - a := rfl _ = |b - a| := (abs_of_pos hε).symm _ = |(b - a) + 0| := by {congr ; exact (add_zero (b - a)).symm} _ = |(b - a) + (u N - u N)| := by {congr ; exact (sub_self (u N)).symm} _ = |(u N - a) + (b - u N)| := congrArg (fun x => |x|) (by ring) _ ≤ |u N - a| + |b - u N| := abs_add (u N - a) (b - u N) _ = |u N - a| + |u N - b| := congrArg (|u N - a| + .) (abs_sub_comm b (u N)) _ < ε / 2 + ε / 2 := add_lt_add hA hB _ = ε := add_halves ε have h3 : ¬(ε < ε) := lt_irrefl ε show False exact h3 h2 -- 2ª demostración del lema auxiliar -- ================================= lemma aux (ha : limite u a) (hb : limite u b) : b ≤ a := by by_contra h -- h : ¬b ≤ a -- ⊢ False let ε := b - a cases' ha (ε/2) (by linarith) with A hA -- A : ℕ -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2 cases' hb (ε/2) (by linarith) with B hB -- B : ℕ -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2 let N := max A B have hAN : A ≤ N := le_max_left A B have hBN : B ≤ N := le_max_right A B specialize hA N hAN -- hA : |u N - a| < ε / 2 specialize hB N hBN -- hB : |u N - b| < ε / 2 rw [abs_lt] at hA hB -- hA : -(ε / 2) < u N - a ∧ u N - a < ε / 2 -- hB : -(ε / 2) < u N - b ∧ u N - b < ε / 2 linarith -- 1ª demostración -- =============== example (ha : limite u a) (hb : limite u b) : a = b := le_antisymm (aux hb ha) (aux ha hb) -- Lemas usados -- ============ -- variable (c d : ℝ) -- #check (not_le : ¬a ≤ b ↔ b < a) -- #check (sub_pos : 0 < a - b ↔ b < a) -- #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 (abs_lt : |a| < b ↔ -b < a ∧ a < b) -- #check (abs_of_pos : 0 < a → |a| = a) -- #check (add_zero a : a + 0 = a) -- #check (sub_self a : a - a = 0) -- #check (abs_add a b : |a + b| ≤ |a| + |b|) -- #check (abs_sub_comm a b : |a - b| = |b - a|) -- #check (add_lt_add : a < b → c < d → a + c < b + d) -- #check (add_halves a : a / 2 + a / 2 = a) -- #check (lt_irrefl a : ¬a < a) -- #check (le_antisymm : a ≤ b → b ≤ a → a = b) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
|
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 |
theory Unicidad_del_limite_de_las_sucesiones_convergentes imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" lemma aux : assumes "limite u a" "limite u b" shows "b ≤ a" proof (rule ccontr) assume "¬ b ≤ a" let ?ε = "b - a" have "0 < ?ε/2" using ‹¬ b ≤ a› by auto obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2" using assms(1) limite_def ‹0 < ?ε/2› by blast obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2" using assms(2) limite_def ‹0 < ?ε/2› by blast let ?C = "max A B" have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2" using hA by simp have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2" using hB by simp have "∀n≥?C. ¦a - b¦ < ?ε" proof (intro allI impI) fix n assume "n ≥ ?C" have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp finally show "¦a - b¦ < b - a" using hCa hCb ‹n ≥ ?C› by fastforce qed then show False by fastforce qed theorem assumes "limite u a" "limite u b" shows "a = b" proof (rule antisym) show "a ≤ b" using assms(2) assms(1) by (rule aux) next show "b ≤ a" using assms(1) assms(2) by (rule aux) qed end |
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:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Real.Basic 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 |
Read More «Si la sucesión u converge a a y la v a b, entonces u+v converge a a+b»
En Lean, una sucesión \(s₀, s₁, s₂, …\) se puede representar mediante una función \(s : ℕ → ℝ\) de forma que \(s(n)\) es \(sₙ\).
Se define que a es el límite de la sucesión \(s\), por
|
1 2 |
def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε |
Demostrar que el límite de la sucesión constante \(sₙ = c\) es \(c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example : limite (fun _ : ℕ ↦ c) c := by sorry |
Demostrar con Lean4 que en \(ℝ\), si \(1 < a\), entonces \(a < aa\)
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a : ℝ} example (h : 1 < a) : a < a * a := by sorry |