{"id":2014,"date":"2024-02-02T06:00:23","date_gmt":"2024-02-02T04:00:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=2014"},"modified":"2024-02-18T14:11:41","modified_gmt":"2024-02-18T12:11:41","slug":"02-feb-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/02-feb-24\/","title":{"rendered":"La sucesi\u00f3n constante s\u2099 = c converge a c"},"content":{"rendered":"\n

En Lean, una sucesi\u00f3n \(s\u2080, s\u2081, s\u2082, …\) se puede representar mediante una funci\u00f3n \(s : \u2115 \u2192 \u211d\) de forma que \(s(n)\) es \(s\u2099\).<\/p>\n

Se define que a es el l\u00edmite de la sucesi\u00f3n \(s\), por<\/p>\n

\ndef limite (s : \u2115 \u2192 \u211d) (a : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |s n - a| < \u03b5\n<\/pre>\n
Demostrar que el l\u00edmite de la sucesi\u00f3n constante \(s\u2099 = c\) es \(c\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\n\ndef limite (s : \u2115 \u2192 \u211d) (a : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |s n - a| < \u03b5\n\nexample : limite (fun _ : \u2115 \u21a6 c) c :=\nby sorry\n<\/pre>\n
<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemos que demostrar que para cada \(\u03b5 \u2208 \u211d\) tal que \(\u03b5 > 0\), existe un \(N \u2208 \u2115\), tal que \((\u2200n \u2208 \u2115)[n \u2265 N \u2192 |s(n) - a| < \u03b5]\). Basta tomar \(N\) como \(0\), ya que para todo \(n \u2265 N\) se tiene
\n\begin{align}
\n   |s(n) - a| &= |a - a| \\
\n              &= |0|     \\
\n              &= 0       \\
\n              &< \u03b5       \\
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n
\nimport Mathlib.Data.Real.Basic\n\ndef limite (s : \u2115 \u2192 \u211d) (a : \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |s n - a| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) c :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun _ => c) n - c| < \u03b5\n  use 0\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 0 \u2192 |(fun _ => c) n - c| < \u03b5\n  intros n _hn\n  -- n : \u2115\n  -- hn : n \u2265 0\n  -- \u22a2 |(fun _ => c) n - c| < \u03b5\n  show |(fun _ => c) n - c| < \u03b5\n  calc |(fun _ => c) n - c| = |c - c| := by dsimp\n                          _ = |0|     := by {congr ; exact sub_self c}\n                          _ = 0       := abs_zero\n                          _ < \u03b5       := h\u03b5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) c :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun _ => c) n - c| < \u03b5\n  use 0\n  -- \u22a2 \u2200 (n : \u2115), n \u2265 0 \u2192 |(fun _ => c) n - c| < \u03b5\n  intros n _hn\n  -- n : \u2115\n  -- hn : n \u2265 0\n  -- \u22a2 |(fun _ => c) n - c| < \u03b5\n  show |(fun _ => c) n - c| < \u03b5\n  calc |(fun _ => c) n - c| = 0       := by simp\n                          _ < \u03b5       := h\u03b5\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) c :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun _ => c) n - c| < \u03b5\n  aesop\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) c :=\nby\n  intros \u03b5 h\u03b5\n  -- \u03b5 : \u211d\n  -- h\u03b5 : \u03b5 > 0\n  -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(fun _ => c) n - c| < \u03b5\n  aesop\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : limite (fun _ : \u2115 \u21a6 c) c :=\n  fun \u03b5 h\u03b5 \u21a6 by aesop\n\n-- Lemas usados\n-- ============\n\n-- #check (sub_self a : a - a = 0)\n<\/pre>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
3. Demostraciones con Isabelle\/HOL<\/h2>\n
\ntheory Limite_de_sucesiones_constantes\nimports Main HOL.Real\nbegin\n\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"limite (\u03bb n. c) c\"\nproof (unfold limite_def)\n  show \"\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6c - c\u00a6 < \u03b5\"\n  proof (intro allI impI)\n    fix \u03b5 :: real\n    assume \"0 < \u03b5\"\n    have \"\u2200n\u22650::nat. \u00a6c - c\u00a6 < \u03b5\"\n    proof (intro allI impI)\n      fix n :: nat\n      assume \"0 \u2264 n\"\n      have \"c - c = 0\"\n        by (simp only: diff_self)\n      then have \"\u00a6c - c\u00a6 = 0\"\n        by (simp only: abs_eq_0_iff)\n      also have \"\u2026 < \u03b5\"\n        by (simp only: \u20390 < \u03b5\u203a)\n      finally show \"\u00a6c - c\u00a6 < \u03b5\"\n        by this\n    qed\n    then show \"\u2203k::nat. \u2200n\u2265k. \u00a6c - c\u00a6 < \u03b5\"\n      by (rule exI)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"limite (\u03bb n. c) c\"\nproof (unfold limite_def)\n  show \"\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6c - c\u00a6 < \u03b5\"\n  proof (intro allI impI)\n    fix \u03b5 :: real\n    assume \"0 < \u03b5\"\n    have \"\u2200n\u22650::nat. \u00a6c - c\u00a6 < \u03b5\"          by (simp add: \u20390 < \u03b5\u203a)\n    then show \"\u2203k::nat. \u2200n\u2265k. \u00a6c - c\u00a6 < \u03b5\" by (rule exI)\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma \"limite (\u03bb n. c) c\"\n  unfolding limite_def\n  by simp\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"limite (\u03bb n. c) c\"\n  by (simp add: limite_def)\n\nend\n<\/pre>\n
Referencias<\/h2>\n