Teorema del emparedado
Demostrar con Lean4 el teorema del emparedado.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import Mathlib.Data.Real.Basic variable (u v w : ℕ → ℝ) variable (a : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que para cada \(ε > 0\), existe un \(N ∈ ℕ\) tal que
\[ (∀ n ≥ N)[|v(n) – a| ≤ ε] \tag{1} \]
Puesto que el límite de \(u\) es \(a\), existe un \(U ∈ ℕ\) tal que
\[ (∀ n ≥ U)[|u(n) – a| ≤ ε] \tag{2} \]
y, puesto que el límite de \(w\) es \(a\), existe un \(W ∈ ℕ\) tal que
\[ (∀ n ≥ W)[|w(n) – a| ≤ ε] \tag{3} \]
Sea \(N = \text{máx}(U, W)\). Veamos que se verifica (1). Para ello, sea \(n ≥ N\). Entonces, \(n ≥ U\), \(n ≥ W\) y, por (2) y (3), se tiene que
\begin{align}
|u(n) – a| &≤ ε \tag{4} \\
|w(n) – a| &≤ ε \tag{5}
\end{align}
Para demostrar que
\[ |v(n) – a| ≤ ε \]
basta demostrar las siguientes desigualdades
\begin{align}
-ε ≤ &v(n) – a \tag{6} \\
&v(n) – a ≤ ε \tag{7}
\end{align}
La demostración de (6) es
\begin{align}
-ε &≤ u(n) – a &&\text{[por (4)]} \\
&≤ v(n) – a &&\text{[por hipótesis]}
\end{align}
La demostración de (7) es
\begin{align}
v(n) – a &≤ w(n) – a &&\text{[por hipótesis]} \\
&≤ ε &&\text{[por (5)]}
\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 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 |
import Mathlib.Data.Real.Basic variable (u v w : ℕ → ℝ) variable (a : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε -- Nota. En la demostración se usará el siguiente lema: lemma max_ge_iff {p q r : ℕ} : r ≥ max p q ↔ r ≥ p ∧ r ≥ q := max_le_iff -- 1ª demostración -- =============== example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v n - a| ≤ ε rcases hu ε hε with ⟨U, hU⟩ -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - a| ≤ ε clear hu rcases hw ε hε with ⟨W, hW⟩ -- W : ℕ -- hW : ∀ (n : ℕ), n ≥ W → |w n - a| ≤ ε clear hw hε use max U W intros n hn -- n : ℕ -- hn : n ≥ max U W -- ⊢ |v n - a| ≤ ε rw [max_ge_iff] at hn -- hn : n ≥ U ∧ n ≥ W specialize hU n hn.1 -- hU : |u n - a| ≤ ε specialize hW n hn.2 -- hW : |w n - a| ≤ ε specialize h1 n -- h1 : u n ≤ v n specialize h2 n -- h2 : v n ≤ w n clear hn rw [abs_le] at * -- ⊢ -ε ≤ v n - a ∧ v n - a ≤ ε constructor . -- ⊢ -ε ≤ v n - a calc -ε ≤ u n - a := hU.1 _ ≤ v n - a := by linarith . -- ⊢ v n - a ≤ ε calc v n - a ≤ w n - a := by linarith _ ≤ ε := hW.2 -- 2ª demostración example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v n - a| ≤ ε rcases hu ε hε with ⟨U, hU⟩ -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - a| ≤ ε clear hu rcases hw ε hε with ⟨W, hW⟩ -- W : ℕ -- hW : ∀ (n : ℕ), n ≥ W → |w n - a| ≤ ε clear hw hε use max U W intros n hn -- n : ℕ -- hn : n ≥ max U W rw [max_ge_iff] at hn -- hn : n ≥ U ∧ n ≥ W specialize hU n (by linarith) -- hU : |u n - a| ≤ ε specialize hW n (by linarith) -- hW : |w n - a| ≤ ε specialize h1 n -- h1 : u n ≤ v n specialize h2 n -- h2 : v n ≤ w n rw [abs_le] at * -- ⊢ -ε ≤ v n - a ∧ v n - a ≤ ε constructor . -- ⊢ -ε ≤ v n - a linarith . -- ⊢ v n - a ≤ ε linarith -- 3ª demostración example (hu : limite u a) (hw : limite w a) (h1 : ∀ n, u n ≤ v n) (h2 : ∀ n, v n ≤ w n) : limite v a := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v n - a| ≤ ε rcases hu ε hε with ⟨U, hU⟩ -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - a| ≤ ε clear hu rcases hw ε hε with ⟨W, hW⟩ -- W : ℕ -- hW : ∀ (n : ℕ), n ≥ W → |w n - a| ≤ ε clear hw hε use max U W intros n hn -- n : ℕ -- hn : n ≥ max U W -- ⊢ |v n - a| ≤ ε rw [max_ge_iff] at hn -- hn : n ≥ U ∧ n ≥ W specialize hU n (by linarith) -- hU : |u n - a| ≤ ε specialize hW n (by linarith) -- hW : |w n - a| ≤ ε specialize h1 n -- h1 : u n ≤ v n specialize h2 n -- h2 : v n ≤ w n rw [abs_le] at * -- hU : -ε ≤ u n - a ∧ u n - a ≤ ε -- hW : -ε ≤ w n - a ∧ w n - a ≤ ε -- ⊢ -ε ≤ v n - a ∧ v n - a ≤ ε constructor <;> linarith |
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 46 47 48 49 50 51 52 53 54 55 |
theory Teorema_del_emparedado imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" lemma assumes "limite u a" "limite w a" "∀n. u n ≤ v n" "∀n. v n ≤ w n" shows "limite v a" proof (unfold limite_def; intro allI impI) fix ε :: real assume hε : "0 < ε" obtain N where hN : "∀n≥N. ¦u n - a¦ < ε" using assms(1) hε limite_def by auto obtain N' where hN' : "∀n≥N'. ¦w n - a¦ < ε" using assms(2) hε limite_def by auto have "∀n≥max N N'. ¦v n - a¦ < ε" proof (intro allI impI) fix n assume hn : "n≥max N N'" have "v n - a < ε" proof - have "v n - a ≤ w n - a" using assms(4) by simp also have "… ≤ ¦w n - a¦" by simp also have "… < ε" using hN' hn by auto finally show "v n - a < ε" . qed moreover have "-(v n - a) < ε" proof - have "-(v n - a) ≤ -(u n - a)" using assms(3) by auto also have "… ≤ ¦u n - a¦" by simp also have "… < ε" using hN hn by auto finally show "-(v n - a) < ε" . qed ultimately show "¦v n - a¦ < ε" by (simp only: abs_less_iff) qed then show "∃k. ∀n≥k. ¦v n - a¦ < ε" by (rule exI) qed end |
