{"id":7837,"date":"2022-11-06T11:06:40","date_gmt":"2022-11-06T10:06:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7837"},"modified":"2022-11-06T11:06:40","modified_gmt":"2022-11-06T10:06:40","slug":"dao-la-semana-en-calculemus-4-de-noviembre-de-2022","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/dao-la-semana-en-calculemus-4-de-noviembre-de-2022\/","title":{"rendered":"DAO: La semana en Calculemus (4 de noviembre 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 X es un espacio m\u00e9trico y x, y \u2208 X, entonces dist(x,y) \u2265 0<\/a><\/li>\n<li><a href=\"#ej2\">2. Si x, y, \u03b5 \u2208 \u211d tales que 0 &lt; \u03b5 \u2264 1, |x| &lt; \u03b5 y |y| &lt; \u03b5, entonces |x*y| &lt; \u03b5<\/a><\/li>\n<li><a href=\"#ej3\">3. La suma de una cota superior de f y una cota superior de g es una cota superior de f+g<\/a><\/li>\n<li><a href=\"#ej4\">4. La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g<\/a><\/li>\n<li><a href=\"#ej5\">5. El producto de dos funciones no negativas es no negativa<\/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 X es un espacio m\u00e9trico y x, y \u2208 X, entonces dist(x,y) \u2265 0<\/h3>\n<p>Demostrar que si X es un espacio m\u00e9trico y x, y \u2208 X, entonces<\/p>\n<pre lang=\"text\">\n   0 \u2264 dist x y\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport topology.metric_space.basic\n\nvariables {X : Type*} [metric_space X]\nvariables x y : X\n\nexample : 0 \u2264 dist x y :=\nsorry\n<\/pre>\n<p><!--more--><\/p>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport topology.metric_space.basic\n\nvariables {X : Type*} [metric_space X]\nvariables x y : X\n\n-- 1\u00aa demostraci\u00f3n\nexample : 0 \u2264 dist x y :=\n  have h1 : 2 * dist x y \u2265 0, by calc\n    2 * dist x y = dist x y + dist x y : two_mul (dist x y)\n             ... = dist x y + dist y x : by rw [dist_comm x y]\n             ... \u2265 dist x x            : dist_triangle x y x\n             ... = 0                   : dist_self x,\n  show 0 \u2264 dist x y,\n    by exact nonneg_of_mul_nonneg_left h1 zero_lt_two\n\n-- 2\u00aa demostraci\u00f3n\nexample : 0 \u2264 dist x y :=\n-- by library_search\ndist_nonneg\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\/Distancia_no_negativa.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. 24.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Si x,y,\u03b5 \u2208 \u211d tales que 0 &lt; \u03b5 \u2264 1, |x| &lt; \u03b5 y |y| &lt; \u03b5, entonces |x*y| &lt; \u03b5<\/h3>\n<p>Demostrar que si x,y,\u03b5 \u2208 \u211d tales que 0 &lt; \u03b5 \u2264 1, |x| &lt; \u03b5 y |y| &lt; \u03b5, entonces |x*y| &lt; \u03b5.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic tactic\n\nexample :\n  \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\nsorry\n<\/pre>\n<p><!--more--><\/p>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport data.real.basic tactic\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\nbegin\n  intros x y \u03b5 he1 he2 hx hy,\n  by_cases h : (|x| = 0),\n  { calc |x * y|\n         = |x| * |y| : abs_mul x y\n     ... = 0 * |y|   : by rw h\n     ... = 0         : zero_mul (abs y)\n     ... < \u03b5         : he1 },\n  { have h1 : 0 < |x|,\n    { have h2 : 0 \u2264 |x| := abs_nonneg x,\n      show 0 < |x|,\n        exact lt_of_le_of_ne h2 (ne.symm h) },\n    calc |x * y|\n         = |x| * |y| : abs_mul x y\n     ... < |x| * \u03b5   : (mul_lt_mul_left h1).mpr hy\n     ... < \u03b5 * \u03b5     : (mul_lt_mul_right he1).mpr hx\n     ... \u2264 1 * \u03b5     : (mul_le_mul_right he1).mpr he2\n     ... = \u03b5         : one_mul \u03b5 },\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\nbegin\n  intros x y \u03b5 he1 he2 hx hy,\n  by_cases h : (|x| = 0),\n  { calc |x * y|\n         = |x| * |y| : by apply abs_mul\n     ... = 0 * |y|   : by rw h\n     ... = 0         : by apply zero_mul\n     ... < \u03b5         : by apply he1 },\n  { have h1 : 0 < |x|,\n      { have h2 : 0 \u2264 |x|,\n          apply abs_nonneg,\n        exact lt_of_le_of_ne h2 (ne.symm h) },\n    calc |x * y|\n         = |x| * |y| : by rw abs_mul\n     ... < |x| * \u03b5   : by apply (mul_lt_mul_left h1).mpr hy\n     ... < \u03b5 * \u03b5     : by apply (mul_lt_mul_right he1).mpr hx\n     ... \u2264 1 * \u03b5     : by apply (mul_le_mul_right he1).mpr he2\n     ... = \u03b5         : by rw [one_mul] },\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\nbegin\n  intros x y \u03b5 he1 he2 hx hy,\n  by_cases (|x| = 0),\n  { by finish },\n  { have : 0 < |x|, by finish,\n    calc |x * y|\n         = |x| * |y| : by rw abs_mul\n     ... < |x| * \u03b5   : by finish\n     ... \u2264 1 * \u03b5     : by nlinarith\n     ... = \u03b5         : by finish },\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\/Cota_del_valor_absoluto_del_producto.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. 26.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. La suma de una cota superior de f y una cota superior de g es una cota superior de f+g<\/h3>\n<p>Demostrar que la suma de una cota superior de f y una cota superior de g es una cota superior de f+g.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\n-- (cota_superior f a) se verifica si a es una cota superior de f.\ndef cota_superior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n\u2200 x, f x \u2264 a\n\nvariables (f g : \u211d \u2192 \u211d)\nvariables (a b : \u211d)\n\nexample\n  (hfa : cota_superior f a)\n  (hgb : cota_superior g b)\n  : cota_superior (\u03bb x, f x + g x) (a + b) :=\nsorry\n<\/pre>\n<p><!--more--><\/p>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\n-- (cota_superior f a) se verifica si a es una cota superior de f.\ndef cota_superior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n\u2200 x, f x \u2264 a\n\nvariables (f g : \u211d \u2192 \u211d)\nvariables (a b : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : cota_superior f a)\n  (hgb : cota_superior g b)\n  : cota_superior (\u03bb x, f x + g x) (a + b) :=\nbegin\n  have h1 : \u2200 x, f x + g x \u2264 a + b,\n  { intro x,\n    have h1a : f x \u2264 a := hfa x,\n    have h1b : g x \u2264 b := hgb x,\n    show f x + g x \u2264 a + b,\n      by exact add_le_add (hfa x) (hgb x), },\n  show cota_superior (\u03bb x, f x + g x) (a + b),\n    by exact h1,\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : cota_superior f a)\n  (hgb : cota_superior g b)\n  : cota_superior (\u03bb x, f x + g x) (a + b) :=\nbegin\n  intro x,\n  dsimp,\n  change f x + g x \u2264 a + b,\n  apply add_le_add,\n  apply hfa,\n  apply hgb\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : cota_superior f a)\n  (hgb : cota_superior g b)\n  : cota_superior (\u03bb x, f x + g x) (a + b) :=\n\u03bb x, add_le_add (hfa x) (hgb x)\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\/Suma_de_cotas_superiores.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. 27.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g<\/h3>\n<p>Demostrar que la suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\n-- (cota_inferior f a) se verifica si a es una cota inferior de f.\ndef cota_inferior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n\u2200 x, a \u2264 f x\n\nvariables (f g : \u211d \u2192 \u211d)\nvariables (a b : \u211d)\n\nexample\n  (hfa : cota_inferior f a)\n  (hgb : cota_inferior g b)\n  : cota_inferior (\u03bb x, f x + g x) (a + b) :=\nsorry\n<\/pre>\n<p><!--more--><\/p>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\n-- (cota_inferior f a) se verifica si a es una cota inferior de f.\ndef cota_inferior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n\u2200 x, a \u2264 f x\n\nvariables (f g : \u211d \u2192 \u211d)\nvariables (a b : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : cota_inferior f a)\n  (hgb : cota_inferior g b)\n  : cota_inferior (\u03bb x, f x + g x) (a + b) :=\nbegin\n  have h1 : \u2200 x, a + b \u2264 f x + g x,\n  { intro x,\n    have h1a : a \u2264 f x := hfa x,\n    have h1b : b \u2264 g x := hgb x,\n    show a + b \u2264 f x + g x,\n      by exact add_le_add (hfa x) (hgb x), },\n  show cota_inferior (\u03bb x, f x + g x) (a + b),\n    by exact h1,\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : cota_inferior f a)\n  (hgb : cota_inferior g b)\n  : cota_inferior (\u03bb x, f x + g x) (a + b) :=\nbegin\n  intro x,\n  dsimp,\n  change a + b \u2264 f x + g x,\n  apply add_le_add,\n  apply hfa,\n  apply hgb\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : cota_inferior f a)\n  (hgb : cota_inferior g b)\n  : cota_inferior (\u03bb x, f x + g x) (a + b) :=\n\u03bb x, add_le_add (hfa x) (hgb x)\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\/Suma_de_cotas_inferiores.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. 27.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. El producto de dos funciones no negativas es no negativa<\/h3>\n<p>Demostrar que el producto de dos funciones no negativas es no negativa.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\nvariables (f g : \u211d \u2192 \u211d)\n\ndef no_negativa (f : \u211d \u2192 \u211d) : Prop := \u2200 x, 0 \u2264 f x\n\nexample\n  (nnf : no_negativa f)\n  (nng : no_negativa g)\n  : no_negativa (f * g) :=\nsorry\n<\/pre>\n<p><!--more--><\/p>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport data.real.basic\nvariables (f g : \u211d \u2192 \u211d)\n\ndef no_negativa (f : \u211d \u2192 \u211d) : Prop := \u2200 x, 0 \u2264 f x\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (nnf : no_negativa f)\n  (nng : no_negativa g)\n  : no_negativa (f * g) :=\nbegin\n  have h1 : \u2200x, 0 \u2264 f x * g x,\n  { intro x,\n    have h2: 0 \u2264 f x := nnf x,\n    have h3: 0 \u2264 g x := nng x,\n    show 0 \u2264 f x * g x,\n      by exact mul_nonneg (nnf x) (nng x), },\n  show no_negativa (f * g),\n    by exact h1,\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (nnf : no_negativa f)\n  (nng : no_negativa g)\n  : no_negativa (f * g) :=\nbegin\n  intro x,\n  change 0 \u2264 f x * g x,\n  apply mul_nonneg,\n  apply nnf,\n  apply nng\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (nnf : no_negativa f)\n  (nng : no_negativa g)\n  : no_negativa (f * g) :=\n\u03bb x, mul_nonneg (nnf x) (nng x)\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\/Producto_no_negativas.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. 27.<\/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 X es un espacio m\u00e9trico y x, y \u2208 X, entonces dist(x,y) \u2265 0 2. Si x, y, \u03b5 \u2208 \u211d tales que 0 &lt; \u03b5 \u2264 1, |x| &lt; \u03b5 y |y| &lt; \u03b5, entonces |x*y| &lt; \u03b5&#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\/7837"}],"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=7837"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7837\/revisions"}],"predecessor-version":[{"id":7838,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7837\/revisions\/7838"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7837"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7837"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7837"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}