{"id":670,"date":"2021-08-21T06:00:21","date_gmt":"2021-08-21T04:00:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=670"},"modified":"2021-08-21T12:44:52","modified_gmt":"2021-08-21T10:44:52","slug":"las-sucesiones-convergentes-son-sucesiones-de-cauchy","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/las-sucesiones-convergentes-son-sucesiones-de-cauchy\/","title":{"rendered":"Las sucesiones convergentes son sucesiones de Cauchy"},"content":{"rendered":"<p><strong>Nota<\/strong>: El problema de hoy lo ha escrito Sara D\u00edaz Real y es uno de los que se encuentran en su Trabajo Fin de M\u00e1ster <a href=\"https:\/\/raw.githubusercontent.com\/saradiazr11\/IMO_en_Lean\/main\/doc\/IMO_en_Lean.pdf\">Formalizaci\u00f3n en Lean de problemas de las Olimpiadas Internacionales de Matem\u00e1ticas (IMO)<\/a>. Concretamente, el problema se encuentra en la <a href=\"https:\/\/raw.githubusercontent.com\/saradiazr11\/IMO_en_Lean\/main\/doc\/IMO_en_Lean.pdf#page=52\">p\u00e1gina 52<\/a> junto con la demostraci\u00f3n en lenguaje natural.<\/p>\n<hr \/>\n<p>En Lean, una sucesi\u00f3n u\u2080, u\u2081, u\u2082, &#8230; se puede representar mediante una funci\u00f3n (u : \u2115 \u2192 \u211d) de forma que u(n) es u\u2099.<\/p>\n<p>Se define<\/p>\n<ul>\n<li>el valor absoluto de x por<\/li>\n<\/ul>\n<pre lang=\"text\">\n     notation `|`x`|` := abs x\n<\/pre>\n<ul>\n<li>a es un l\u00edmite de la sucesi\u00f3n u, por<\/li>\n<\/ul>\n<pre lang=\"text\">\n     def limite (u : \u2115 \u2192 \u211d) (a : \u211d) :=\n       \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - a| \u2264 \u03b5\n<\/pre>\n<ul>\n<li>la sucesi\u00f3n u es convergente por<\/li>\n<\/ul>\n<pre lang=\"text\">\n     def suc_convergente (u : \u2115 \u2192 \u211d) :=\n       \u2203 l, limite u l\n<\/pre>\n<ul>\n<li>la sucesi\u00f3n u es de Cauchy por<\/li>\n<\/ul>\n<pre lang=\"text\">\n     def suc_cauchy (u : \u2115 \u2192 \u211d) :=\n       \u2200 \u03b5 > 0, \u2203 N, \u2200 p \u2265 N, \u2200 q \u2265 N, |u p - u q| \u2264 \u03b5\n<\/pre>\n<p>Demostrar que las sucesiones convergentes son de Cauchy.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariable {u : \u2115 \u2192 \u211d }\n\nnotation `|`x`|` := abs x\n\ndef limite (u : \u2115 \u2192 \u211d) (l : \u211d) : Prop :=\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - l| \u2264 \u03b5\n\ndef suc_convergente (u : \u2115 \u2192 \u211d) :=\n  \u2203 l, limite u l\n\ndef suc_cauchy (u : \u2115 \u2192 \u211d) :=\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 p \u2265 N, \u2200 q \u2265 N, |u p - u q| \u2264 \u03b5\n\nexample\n  (h : suc_convergente u)\n  : suc_cauchy u :=\nsorry\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\r\nimport data.real.basic\r\n\r\nvariable {u : \u2115 \u2192 \u211d }\r\n\r\nnotation `|`x`|` := abs x\r\n\r\ndef limite (u : \u2115 \u2192 \u211d) (l : \u211d) : Prop :=\r\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - l| \u2264 \u03b5\r\n\r\ndef suc_convergente (u : \u2115 \u2192 \u211d) :=\r\n  \u2203 l, limite u l\r\n\r\ndef suc_cauchy (u : \u2115 \u2192 \u211d) :=\r\n  \u2200 \u03b5 > 0, \u2203 N, \u2200 p \u2265 N, \u2200 q \u2265 N, |u p - u q| \u2264 \u03b5\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (h : suc_convergente u)\r\n  : suc_cauchy u :=\r\nbegin\r\n  unfold suc_cauchy,\r\n  intros \u03b5 h\u03b5,\r\n  have h\u03b52 : 0 < \u03b5\/2 := half_pos h\u03b5,\r\n  cases h with l hl,\r\n  cases hl (\u03b5\/2) h\u03b52 with N hN,\r\n  clear h\u03b5 hl h\u03b52,\r\n  use N,\r\n  intros p hp q hq,\r\n  calc |u p - u q|\r\n       = |(u p - l) + (l - u q)| : by ring_nf\r\n   ... \u2264 |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)\r\n   ... = |u p - l|  + |u q - l|  : congr_arg2 (+) rfl (abs_sub_comm l (u q))\r\n   ... \u2264 \u03b5\/2 + \u03b5\/2               : add_le_add (hN p hp) (hN q hq)\r\n   ... = \u03b5                       : add_halves \u03b5,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (h : suc_convergente u)\r\n  : suc_cauchy u :=\r\nbegin\r\n  intros \u03b5 h\u03b5,\r\n  cases h with l hl,\r\n  cases hl (\u03b5\/2) (half_pos h\u03b5) with N hN,\r\n  clear h\u03b5 hl,\r\n  use N,\r\n  intros p hp q hq,\r\n  calc |u p - u q|\r\n       = |(u p - l) + (l - u q)| : by ring_nf\r\n   ... \u2264 |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)\r\n   ... = |u p - l|  + |u q - l|  : congr_arg2 (+) rfl (abs_sub_comm l (u q))\r\n   ... \u2264 \u03b5\/2 + \u03b5\/2               : add_le_add (hN p hp) (hN q hq)\r\n   ... = \u03b5                       : add_halves \u03b5,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (h : suc_convergente u)\r\n  : suc_cauchy u :=\r\nbegin\r\n  intros \u03b5 h\u03b5,\r\n  cases h with l hl,\r\n  cases hl (\u03b5\/2) (half_pos h\u03b5) with N hN,\r\n  clear h\u03b5 hl,\r\n  use N,\r\n  intros p hp q hq,\r\n  have cota1 : |u p - l| \u2264 \u03b5 \/ 2 := hN p hp,\r\n  have cota2 : |u q - l| \u2264 \u03b5 \/ 2 := hN q hq,\r\n  clear hN hp hq,\r\n  calc |u p - u q|\r\n       = |(u p - l) + (l - u q)| : by ring_nf\r\n   ... \u2264 |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)\r\n   ... = |u p - l|  + |u q - l|  : by rw abs_sub_comm l (u q)\r\n   ... \u2264 \u03b5                       : by linarith,\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  (h : suc_convergente u)\r\n  : suc_cauchy u :=\r\nbegin\r\n  intros \u03b5 h\u03b5,\r\n  cases h with l hl,\r\n  cases hl (\u03b5\/2) (half_pos h\u03b5) with N hN,\r\n  clear h\u03b5 hl,\r\n  use N,\r\n  intros p hp q hq,\r\n  calc |u p - u q|\r\n       = |(u p - l) + (l - u q)| : by ring_nf\r\n   ... \u2264 |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)\r\n   ... = |u p - l|  + |u q - l|  : by rw abs_sub_comm l (u q)\r\n   ... \u2264 \u03b5                       : by linarith [hN p hp, hN q hq],\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n  (h : suc_convergente u)\r\n  : suc_cauchy u :=\r\nbegin\r\n  intros \u03b5 h\u03b5,\r\n  cases h with l hl,\r\n  cases hl (\u03b5\/2) (by linarith) with N hN,\r\n  use N,\r\n  intros p hp q hq,\r\n  calc |u p - u q|\r\n       = |(u p - l) + (l - u q)| : by ring_nf\r\n   ... \u2264 |u p - l|  + |l - u q|  : by simp [abs_add]\r\n   ... = |u p - l|  + |u q - l|  : by simp [abs_sub_comm]\r\n   ... \u2264 \u03b5                       : by linarith [hN p hp, hN q hq],\r\nend\r\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Las_sucesiones_convergentes_son_sucesiones_de_Cauchy.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;lean&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n<p>[expand title=\"Soluciones con Isabelle\/HOL\"]<\/p>\n<pre lang=\"isar\">\r\ntheory Las_sucesiones_convergentes_son_sucesiones_de_Cauchy\r\nimports Main HOL.Real\r\nbegin\r\n\r\ndefinition limite :: \"(nat \u21d2 real) \u21d2 real \u21d2 bool\"\r\n  where \"limite u c \u27f7 (\u2200\u03b5>0. \u2203k::nat. \u2200n\u2265k. \u00a6u n - c\u00a6 < \u03b5)\"\r\n\r\ndefinition suc_convergente :: \"(nat \u21d2 real) \u21d2 bool\"\r\n  where \"suc_convergente u \u27f7 (\u2203 l. limite u l)\"\r\n\r\ndefinition suc_cauchy :: \"(nat \u21d2 real) \u21d2 bool\"\r\n  where \"suc_cauchy u \u27f7 (\u2200\u03b5>0. \u2203k. \u2200m\u2265k. \u2200n\u2265k. \u00a6u m - u n\u00a6 < \u03b5)\"\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"suc_convergente u\"\r\n  shows   \"suc_cauchy u\"\r\nproof (unfold suc_cauchy_def; intro allI impI)\r\n  fix \u03b5 :: real\r\n  assume \"0 < \u03b5\"\r\n  then have \"0 < \u03b5\/2\"\r\n    by simp\r\n  obtain a where \"limite u a\"\r\n    using assms suc_convergente_def by blast\r\n  then obtain k where hk : \"\u2200n\u2265k. \u00a6u n - a\u00a6 < \u03b5\/2\"\r\n    using \u20390 < \u03b5 \/ 2\u203a limite_def by blast\r\n  have \"\u2200m\u2265k. \u2200n\u2265k. \u00a6u m - u n\u00a6 < \u03b5\"\r\n  proof (intro allI impI)\r\n    fix p q\r\n    assume hp : \"p \u2265 k\" and hq : \"q \u2265 k\"\r\n    then have hp' : \"\u00a6u p - a\u00a6 < \u03b5\/2\"\r\n      using hk by blast\r\n    have hq' : \"\u00a6u q - a\u00a6 < \u03b5\/2\"\r\n      using hk hq by blast\r\n    have \"\u00a6u p - u q\u00a6 = \u00a6(u p - a) + (a - u q)\u00a6\"\r\n      by simp\r\n    also have \"\u2026 \u2264 \u00a6u p - a\u00a6  + \u00a6a - u q\u00a6\"\r\n      by simp\r\n    also have \"\u2026 = \u00a6u p - a\u00a6  + \u00a6u q - a\u00a6\"\r\n      by simp\r\n    also have \"\u2026 < \u03b5\/2 + \u03b5\/2\"\r\n      using hp' hq' by simp\r\n    also have \"\u2026 = \u03b5\"\r\n      by simp\r\n    finally show \"\u00a6u p - u q\u00a6 < \u03b5\"\r\n      by this\r\n  qed\r\n  then show \"\u2203k. \u2200m\u2265k. \u2200n\u2265k. \u00a6u m - u n\u00a6 < \u03b5\"\r\n    by (rule exI)\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"suc_convergente u\"\r\n  shows   \"suc_cauchy u\"\r\nproof (unfold suc_cauchy_def; intro allI impI)\r\n  fix \u03b5 :: real\r\n  assume \"0 < \u03b5\"\r\n  then have \"0 < \u03b5\/2\"\r\n    by simp\r\n  obtain a where \"limite u a\"\r\n    using assms suc_convergente_def by blast\r\n  then obtain k where hk : \"\u2200n\u2265k. \u00a6u n - a\u00a6 < \u03b5\/2\"\r\n    using \u20390 < \u03b5 \/ 2\u203a limite_def by blast\r\n  have \"\u2200m\u2265k. \u2200n\u2265k. \u00a6u m - u n\u00a6 < \u03b5\"\r\n  proof (intro allI impI)\r\n    fix p q\r\n    assume hp : \"p \u2265 k\" and hq : \"q \u2265 k\"\r\n    then have hp' : \"\u00a6u p - a\u00a6 < \u03b5\/2\"\r\n      using hk by blast\r\n    have hq' : \"\u00a6u q - a\u00a6 < \u03b5\/2\"\r\n      using hk hq by blast\r\n    show \"\u00a6u p - u q\u00a6 < \u03b5\"\r\n      using hp' hq' by argo\r\n  qed\r\n  then show \"\u2203k. \u2200m\u2265k. \u2200n\u2265k. \u00a6u m - u n\u00a6 < \u03b5\"\r\n    by (rule exI)\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"suc_convergente u\"\r\n  shows   \"suc_cauchy u\"\r\nproof (unfold suc_cauchy_def; intro allI impI)\r\n  fix \u03b5 :: real\r\n  assume \"0 < \u03b5\"\r\n  then have \"0 < \u03b5\/2\"\r\n    by simp\r\n  obtain a where \"limite u a\"\r\n    using assms suc_convergente_def by blast\r\n  then obtain k where hk : \"\u2200n\u2265k. \u00a6u n - a\u00a6 < \u03b5\/2\"\r\n    using \u20390 < \u03b5 \/ 2\u203a limite_def by blast\r\n  have \"\u2200m\u2265k. \u2200n\u2265k. \u00a6u m - u n\u00a6 < \u03b5\"\r\n    using hk by (smt (z3) field_sum_of_halves)\r\n  then show \"\u2203k. \u2200m\u2265k. \u2200n\u2265k. \u00a6u m - u n\u00a6 < \u03b5\"\r\n    by (rule exI)\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"suc_convergente u\"\r\n  shows   \"suc_cauchy u\"\r\nproof (unfold suc_cauchy_def; intro allI impI)\r\n  fix \u03b5 :: real\r\n  assume \"0 < \u03b5\"\r\n  then have \"0 < \u03b5\/2\"\r\n    by simp\r\n  obtain a where \"limite u a\"\r\n    using assms suc_convergente_def by blast\r\n  then obtain k where hk : \"\u2200n\u2265k. \u00a6u n - a\u00a6 < \u03b5\/2\"\r\n    using \u20390 < \u03b5 \/ 2\u203a limite_def by blast\r\n  then show \"\u2203k. \u2200m\u2265k. \u2200n\u2265k. \u00a6u m - u n\u00a6 < \u03b5\"\r\n    by (smt (z3) field_sum_of_halves)\r\nqed\r\n\r\nend\r\n<\/pre>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;isar&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Nota: El problema de hoy lo ha escrito Sara D\u00edaz Real y es uno de los que se encuentran en su Trabajo Fin de M\u00e1ster Formalizaci\u00f3n en Lean de problemas de las Olimpiadas Internacionales de Matem\u00e1ticas (IMO). Concretamente, el problema se encuentra en la p\u00e1gina 52 junto con la demostraci\u00f3n en lenguaje natural. En Lean, una sucesi\u00f3n u\u2080, u\u2081, u\u2082, &#8230; se puede representar mediante una funci\u00f3n (u : \u2115 \u2192 \u211d) de forma que u(n) es u\u2099. Se define el valor absoluto de x por notation `|`x`|` := abs x a es un 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 &#8211; a|&#8230;<\/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":[101,90,95,92,94,97,91,51,100,96,98,83,85,87,86,80,81,84,88,43,63,89,82,99,46],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/670"}],"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=670"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/670\/revisions"}],"predecessor-version":[{"id":673,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/670\/revisions\/673"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=670"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=670"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=670"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}