{"id":738,"date":"2021-09-05T06:00:26","date_gmt":"2021-09-05T04:00:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=738"},"modified":"2021-09-01T19:17:56","modified_gmt":"2021-09-01T17:17:56","slug":"las-sucesiones-divergentes-positivas-no-tienen-limites-finitos","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/las-sucesiones-divergentes-positivas-no-tienen-limites-finitos\/","title":{"rendered":"Las sucesiones divergentes positivas no tienen l\u00edmites finitos"},"content":{"rendered":"

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

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

\r\n   def limite (u: \u2115 \u2192 \u211d) (a: \u211d) :=\r\n     \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - a| < \u03b5\r\n<\/pre>\n
donde se usa la notaci\u00f3n |x| para el valor absoluto de x<\/p>\n
\r\n   notation `|`x`|` := abs x\r\n<\/pre>\n
La sucesi\u00f3n u diverge positivamente cuando, para cada n\u00famero real A, se puede encontrar un n\u00famero natural m tal que, para n > m , se tenga u(n) > A. En Lean se puede definir por<\/p>\n
\r\n   def diverge_positivamente (u : \u2115 \u2192 \u211d) :=\r\n     \u2200 A, \u2203 m, \u2200 n \u2265 m, u n > A\r\n<\/pre>\n
Demostrar que si u diverge positivamente, entonces ning\u00fan n\u00famero real es l\u00edmite de u.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\r\nimport data.real.basic\r\nimport tactic\r\n\r\nvariable  {u : \u2115 \u2192 \u211d}\r\n\r\nnotation `|`x`|` := abs x\r\n\r\ndef limite (u : \u2115 \u2192 \u211d) (a : \u211d) :=\r\n  \u2200 \u03b5 > 0, \u2203 m, \u2200 n \u2265 m, |u n - a| < \u03b5\r\n\r\ndef diverge_positivamente (u : \u2115 \u2192 \u211d) :=\r\n  \u2200 A, \u2203 m, \u2200 n \u2265 m, u n > A\r\n\r\nexample\r\n  (h : diverge_positivamente u)\r\n  : \u00ac(\u2203 a, limite u a) :=\r\nsorry\r\n<\/pre>\n
[expand title=\"Soluciones con Lean\"]<\/p>\n
\r\nimport data.real.basic\r\nimport tactic\r\n\r\nvariable  {u : \u2115 \u2192 \u211d}\r\n\r\nnotation `|`x`|` := abs x\r\n\r\ndef limite (u : \u2115 \u2192 \u211d) (a : \u211d) :=\r\n  \u2200 \u03b5 > 0, \u2203 m, \u2200 n \u2265 m, |u n - a| < \u03b5\r\n\r\ndef diverge_positivamente (u : \u2115 \u2192 \u211d) :=\r\n  \u2200 A, \u2203 m, \u2200 n \u2265 m, u n > A\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (h : diverge_positivamente u)\r\n  : \u00ac(\u2203 a, limite u a) :=\r\nbegin\r\n  push_neg,\r\n  intros a ha,\r\n  cases ha 1 zero_lt_one with m1 hm1,\r\n  cases h (a+1) with m2 hm2,\r\n  let m := max m1 m2,\r\n  specialize hm1 m (le_max_left _ _),\r\n  specialize hm2 m (le_max_right _ _),\r\n  replace hm1 : u m - a < 1 := lt_of_abs_lt hm1,\r\n  replace hm2 : 1 < u m - a := lt_sub_iff_add_lt'.mpr hm2,\r\n  apply lt_irrefl (u m),\r\n  calc u m < a + 1 : sub_lt_iff_lt_add'.mp hm1\r\n       ... < u m   : lt_sub_iff_add_lt'.mp hm2,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (h : diverge_positivamente u)\r\n  : \u00ac(\u2203 a, limite u a) :=\r\nbegin\r\n  push_neg,\r\n  intros a ha,\r\n  cases ha 1 (by linarith) with m1 hm1,\r\n  cases h (a+1) with m2 hm2,\r\n  let m := max m1 m2,\r\n  replace hm1 : |u m - a| < 1 := by finish,\r\n  replace hm1 : u m - a < 1   := lt_of_abs_lt hm1,\r\n  replace hm2 : u m > a + 1   := by finish,\r\n  replace hm2 : 1 < u m - a   := lt_sub_iff_add_lt'.mpr hm2,\r\n  apply lt_irrefl (u m),\r\n  calc u m < a + 1 : by linarith\r\n       ... < u m   : by linarith\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (h : diverge_positivamente u)\r\n  : \u00ac(\u2203 a, limite u a) :=\r\nbegin\r\n  push_neg,\r\n  intros a ha,\r\n  cases ha 1 (by linarith) with m1 hm1,\r\n  cases h (a+1) with m2 hm2,\r\n  let m := max m1 m2,\r\n  specialize hm1 m (le_max_left _ _),\r\n  specialize hm2 m (le_max_right _ _),\r\n  rw abs_lt at hm1,\r\n  linarith,\r\nend\r\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="lean"> y otra con <\/pre>
\n[\/expand]<\/p>\n
[expand title=\"Soluciones con Isabelle\/HOL\"]<\/p>\n
\r\ntheory Las_sucesiones_divergentes_positivas_no_tienen_limites_finitos\r\nimports Main HOL.Real\r\nbegin\r\n\r\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\r\n  where \"limite u a \u27f7 (\u2200\u03b5>0. \u2203N. \u2200k\u2265N. \u00a6u k - a\u00a6 < \u03b5)\"\r\n\r\ndefinition diverge_positivamente :: \"(nat \u21d2 real) \u21d2 bool\"\r\n  where \"diverge_positivamente u \u27f7 (\u2200A. \u2203m. \u2200n\u2265m. u n > A)\"\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"diverge_positivamente u\"\r\n  shows   \"\u2204a. limite u a\"\r\nproof (rule notI)\r\n  assume \"\u2203a. limite u a\"\r\n  then obtain a where \"limite u a\" try\r\n    by auto\r\n  then obtain m1 where hm1 : \"\u2200n\u2265m1. \u00a6u n - a\u00a6 < 1\"\r\n    using limite_def by fastforce\r\n  obtain m2 where hm2 : \"\u2200n\u2265m2. u n > a + 1\"\r\n    using assms diverge_positivamente_def by blast\r\n  let ?m = \"max m1 m2\"\r\n  have \"u ?m < u ?m\" using hm1 hm2\r\n  proof -\r\n    have \"?m \u2265 m1\"\r\n      by (rule max.cobounded1)\r\n    have \"?m \u2265 m2\"\r\n      by (rule max.cobounded2)\r\n    have \"u ?m - a < 1\"\r\n      using hm1 \u2039?m \u2265 m1\u203a by fastforce\r\n    moreover have \"u ?m > a + 1\"\r\n      using hm2 \u2039?m \u2265 m2\u203a by simp\r\n    ultimately show \"u ?m < u ?m\"\r\n      by simp\r\n  qed\r\n  then show False\r\n    by auto\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"diverge_positivamente u\"\r\n  shows   \"\u2204a. limite u a\"\r\nproof (rule notI)\r\n  assume \"\u2203a. limite u a\"\r\n  then obtain a where \"limite u a\" try\r\n    by auto\r\n  then obtain m1 where hm1 : \"\u2200n\u2265m1. \u00a6u n - a\u00a6 < 1\"\r\n    using limite_def by fastforce\r\n  obtain m2 where hm2 : \"\u2200n\u2265m2. u n > a + 1\"\r\n    using assms diverge_positivamente_def by blast\r\n  let ?m = \"max m1 m2\"\r\n  have \"1 < 1\"\r\n  proof -\r\n    have \"1 < u ?m - a\"\r\n      using hm2\r\n      by (metis add.commute less_diff_eq max.cobounded2)\r\n    also have \"\u2026 < 1\"\r\n      using hm1\r\n      by (metis abs_less_iff max_def order_refl)\r\n    finally show \"1 < 1\" .\r\n  qed\r\n  then show False\r\n    by auto\r\nqed\r\n\r\nend\r\n<\/pre>\n
En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="isar"> y otra con <\/pre>
\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"
En Lean, una sucesi\u00f3n u\u2080, u\u2081, u\u2082, … se puede representar mediante una funci\u00f3n (u : \u2115 \u2192 \u211d) de forma que u(n) es u\u2099. Se define que a es el l\u00edmite de la sucesi\u00f3n u, por def limite (u: \u2115 \u2192 \u211d) (a: \u211d) := \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n – a| < \u03b5 donde se usa la notaci\u00f3n |x| para el valor absoluto de x notation `|`x`|` := abs x La sucesi\u00f3n u diverge positivamente cuando, para cada n\u00famero real A, se puede encontrar un n\u00famero natural m tal que, para n > m , se tenga u(n) > A. En Lean se puede definir por def diverge_positivamente (u : \u2115 \u2192 \u211d) := \u2200 A,…<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[14],"tags":[216,214,77,92,133,215,217,213,191,60,128,218,51,100,197,109,198,80,125,63,183,182,89,211,209,210,181,122,44,111,196,212,208],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/738"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=738"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/738\/revisions"}],"predecessor-version":[{"id":739,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/738\/revisions\/739"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=738"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=738"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=738"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}