{"id":7807,"date":"2022-10-02T11:03:24","date_gmt":"2022-10-02T09:03:24","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7807"},"modified":"2022-10-02T11:03:24","modified_gmt":"2022-10-02T09:03:24","slug":"dao-la-semana-en-calculemus-30-de-septiembre-de-2022","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/dao-la-semana-en-calculemus-30-de-septiembre-de-2022\/","title":{"rendered":"DAO: La semana en Calculemus (30 de septiembre de 2022)"},"content":{"rendered":"<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. Si a, b, c \u2208 \u211d tales que a \u2264 b, entonces c &#8211; e\u1d47 \u2264 c &#8211; e\u1d43<\/a><\/li>\n<li><a href=\"#ej2\">2. Si a, b \u2208 \u211d, entonces 2ab \u2264 a\u00b2 + b\u00b2<\/a><\/li>\n<li><a href=\"#ej3\">3. Si a, b \u2208 \u211d, entonces |ab| \u2264 (a\u00b2 + b\u00b2)\/2<\/a><\/li>\n<li><a href=\"#ej4\">4. Si a, b \u2208 \u211d, entonces min(a,b) = min(b,a)<\/a><\/li>\n<li><a href=\"#ej5\">5. Si a, b \u2208 \u211d, entonces max(a,b) = max(b,a)<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. Si a, b, c \u2208 \u211d tales que a \u2264 b, entonces c &#8211; e\u1d47 \u2264 c &#8211; e\u1d43<\/h3>\n<p>Demostrar que si a, b, c \u2208 \u211d tales que a \u2264 b, entonces c &#8211; e\u1d47 \u2264 c &#8211; e\u1d43.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport analysis.special_functions.log.basic\nimport tactic\nopen real\nvariables a b c : \u211d\n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport analysis.special_functions.log.basic\nimport tactic\nopen real\nvariables a b c : \u211d\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nbegin\n   apply sub_le_sub_left _ c,\n   exact exp_le_exp.mpr h,\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nsub_le_sub_left (exp_le_exp.mpr h) c\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a \u2264 b)\n  : c - b \u2264 c - a :=\n-- by library_search\nsub_le_sub_left h c\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\nby linarith [exp_le_exp.mpr h]\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a \u2264 b)\n  : c - exp b \u2264 c - exp a :=\n-- by hint\nby finish\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\/Desigualdad-con_exponencial_3.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 17.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Si a, b \u2208 \u211d, entonces 2ab \u2264 a\u00b2 + b\u00b2<\/h3>\n<p>Demostrar que si a, b \u2208 \u211d, entonces 2ab \u2264 a\u00b2 + b\u00b2<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\nimport tactic\n\nvariables a b : \u211d\n\nexample : 2*a*b \u2264 a^2 + b^2 :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport data.real.basic\nimport tactic\n\nvariables a b : \u211d\n\n-- 1\u00aa demostraci\u00f3n\nexample : 2*a*b \u2264 a^2 + b^2 :=\nbegin\n  have : 0 \u2264 (a - b)^2 := sq_nonneg (a - b),\n  have : 0 \u2264 a^2 - 2*a*b + b^2, by linarith,\n  show 2*a*b \u2264 a^2 + b^2, by linarith,\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample : 2*a*b \u2264 a^2 + b^2 :=\nbegin\n  have h : 0 \u2264 a^2 - 2*a*b + b^2,\n  { calc a^2 - 2*a*b + b^2\n        = (a - b)^2                   : by ring\n    ... \u2265 0                           : by apply pow_two_nonneg },\n  calc 2*a*b\n       = 2*a*b + 0                   : by ring\n   ... \u2264 2*a*b + (a^2 - 2*a*b + b^2) : add_le_add (le_refl _) h\n   ... = a^2 + b^2                   : by ring\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample : 2*a*b \u2264 a^2 + b^2 :=\nbegin\n  have : 0 \u2264 a^2 - 2*a*b + b^2,\n  { calc a^2 - 2*a*b + b^2\n         = (a - b)^2       : by ring\n     ... \u2265 0               : by apply pow_two_nonneg },\n  linarith,\nend\n\n-- 4\u00aa demostraci\u00f3n\nexample : 2*a*b \u2264 a^2 + b^2 :=\n-- by library_search\ntwo_mul_le_add_sq a b\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\/Doble_del_producto_menor_que_suma_de_cuadrados.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 17.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si a, b \u2208 \u211d, entonces |ab| \u2264 (a\u00b2 + b\u00b2)\/2<\/h3>\n<p>Demostrar que si a, b \u2208 \u211d, entonces |ab| \u2264 (a\u00b2 + b\u00b2)\/2<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\nimport tactic\n\nvariables a b : \u211d\n\nexample : abs (a*b) \u2264 (a^2 + b^2) \/ 2 :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport data.real.basic\nimport tactic\n\nvariables a b : \u211d\n\n-- 1\u00aa demostraci\u00f3n\nexample : abs (a*b) \u2264 (a^2 + b^2) \/ 2 :=\nbegin\n  apply abs_le.mpr,\n  split,\n  { have h1 : 0 \u2264 a^2 + 2*a*b + b^2,\n      calc 0 \u2264 (a+b)^2                : by exact pow_two_nonneg (a + b)\n         ... = a^2+2*a*b+b^2          : by ring,\n    have h2 : -2*(a*b) \u2264 a^2 + b^2,\n      calc -2*(a*b)\n           \u2264 -2*(a*b)+(a^2+2*a*b+b^2) : by exact le_add_of_nonneg_right h1\n       ... = a^2 + b^2                : by ring,\n    show -((a^2 + b^2) \/ 2) \u2264 a*b,      by linarith [h2] },\n  { have h3 : 0 \u2264 a^2 - 2*a*b + b^2,\n      calc 0 \u2264 (a-b)^2                : by exact pow_two_nonneg (a - b)\n         ... = a^2-2*a*b+b^2          : by ring,\n    have h4 : 2*(a*b) \u2264 a^2 + b^2,\n      calc 2*(a*b)\n           \u2264 2*(a*b)+(a^2-2*a*b+b^2)  : by exact le_add_of_nonneg_right h3\n       ... = a^2 + b^2                : by ring,\n    show a * b \u2264 (a^2 + b^2)\/2,         by linarith [h4] },\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample : abs (a*b) \u2264 (a^2 + b^2) \/ 2 :=\nbegin\n  apply abs_le.mpr,\n  split,\n  { have h1 : 0 \u2264 a^2 + 2*a*b + b^2,\n      calc 0 \u2264 (a+b)^2                : by exact pow_two_nonneg (a + b)\n         ... = a^2+2*a*b+b^2          : by ring,\n    have h2 : -2*(a*b) \u2264 a^2 + b^2,\n      calc -2*(a*b)\n           \u2264 -2*(a*b)+(a^2+2*a*b+b^2) : by exact le_add_of_nonneg_right h1\n       ... = a^2 + b^2                : by ring,\n    show -((a^2 + b^2) \/ 2) \u2264 a*b,      by linarith [h2] },\n  { have h4 : 2*a*b \u2264 a^2 + b^2       := two_mul_le_add_sq a b,\n    show a * b \u2264 (a^2 + b^2)\/2,         by linarith [h4] },\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample : abs (a*b) \u2264 (a^2 + b^2) \/ 2 :=\nbegin\n  apply abs_le.mpr,\n  split,\n  { have h1 : 0 \u2264 a^2 + 2*a*b + b^2,\n      calc 0 \u2264 (a+b)^2                : by exact pow_two_nonneg (a + b)\n         ... = a^2+2*a*b+b^2          : by ring,\n    have h2 : -2*(a*b) \u2264 a^2 + b^2,\n      calc -2*(a*b)\n           \u2264 -2*(a*b)+(a^2+2*a*b+b^2) : by exact le_add_of_nonneg_right h1\n       ... = a^2 + b^2                : by ring,\n    show -((a^2 + b^2) \/ 2) \u2264 a*b,      by linarith [h2] },\n  { show a * b \u2264 (a^2 + b^2)\/2,         by linarith [two_mul_le_add_sq a b] },\nend\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\/Valor_absoluto_del_producto_menor_media_de_cuadrados.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 18.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Si a, b \u2208 \u211d, entonces min(a,b) = min(b,a)<\/h3>\n<p>Demostrar que si a, b \u2208 \u211d, entonces min(a,b) = min(b,a).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariables a b : \u211d\n\nexample : min a b = min b a :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariables a b : \u211d\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min a b = min b a :=\nbegin\n  apply le_antisymm,\n  { show min a b \u2264 min b a,\n    apply le_min,\n    { apply min_le_right },\n    { apply min_le_left }},\n  { show min b a \u2264 min a b,\n    apply le_min,\n    { apply min_le_right },\n    { apply min_le_left }},\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min a b = min b a :=\nbegin\n  have h : \u2200 x y : \u211d, min x y \u2264 min y x,\n  { intros x y,\n    apply le_min,\n    { apply min_le_right },\n    { apply min_le_left }},\n  apply le_antisymm,\n  apply h,\n  apply h,\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min a b = min b a :=\nbegin\n  have h : \u2200 {x y : \u211d}, min x y \u2264 min y x,\n  { intros x y,\n    exact le_min (min_le_right x y) (min_le_left x y) },\n  exact le_antisymm h h,\nend\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : min a b = min b a :=\nbegin\n  apply le_antisymm,\n  repeat {\n    apply le_min,\n    apply min_le_right,\n    apply min_le_left },\nend\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\/Conmutatividad_del_minimo.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 19.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Si a, b \u2208 \u211d, entonces max(a,b) = max(b,a)<\/h3>\n<p>Demostrar que si a, b \u2208 \u211d, entonces max(a,b) = max(b,a)<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariables a b : \u211d\n\nexample : max a b = max b a :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariables a b : \u211d\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : max a b = max b a :=\nbegin\n  apply le_antisymm,\n  { show max a b \u2264 max b a,\n    apply max_le,\n    { apply le_max_right },\n    { apply le_max_left }},\n  { show max b a \u2264 max a b,\n    apply max_le,\n    { apply le_max_right },\n    { apply le_max_left }},\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : max a b = max b a :=\nbegin\n  have h : \u2200 x y : \u211d, max x y \u2264 max y x,\n  { intros x y,\n    apply max_le,\n    { apply le_max_right },\n    { apply le_max_left }},\n  apply le_antisymm,\n  apply h,\n  apply h,\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : max a b = max b a :=\nbegin\n  have h : \u2200 {x y : \u211d}, max x y \u2264 max y x,\n  { intros x y,\n    exact max_le (le_max_right y x) (le_max_left y x),},\n  exact le_antisymm h h,\nend\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : max a b = max b a :=\nbegin\n  apply le_antisymm,\n  repeat {\n    apply max_le,\n    apply le_max_right,\n    apply le_max_left },\nend\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\/Conmutatividad_del_maximo.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 19.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades: 1. Si a, b, c \u2208 \u211d tales que a \u2264 b, entonces c &#8211; e\u1d47 \u2264 c &#8211; e\u1d43 2. Si a, b \u2208 \u211d, entonces 2ab \u2264 a\u00b2 + b\u00b2 3. Si a, b \u2208 \u211d, entonces |ab| \u2264&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7807"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=7807"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7807\/revisions"}],"predecessor-version":[{"id":7808,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7807\/revisions\/7808"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7807"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7807"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7807"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}