{"id":8032,"date":"2023-10-07T11:15:08","date_gmt":"2023-10-07T09:15:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8032"},"modified":"2023-10-07T11:15:08","modified_gmt":"2023-10-07T09:15:08","slug":"07-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/07-oct-23\/","title":{"rendered":"La semana en Calculemus (7 de octubre de 2023)"},"content":{"rendered":"<p><br \/>\nEsta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. En los espacios m\u00e9tricos, d(x,y) \u2265 0<\/a><\/li>\n<li><a href=\"#ej2\">2. En \u211d, {0 &lt; \u03b5, \u03b5 \u2264 1, |x| &lt; \u03b5, |y| &lt; \u03b5} \u22a2 |xy| &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 funciones no negativas es no negativo<\/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. En los espacios m\u00e9tricos, d(x,y) \u2265 0<\/h3>\n<p>Demostrar con Lean4 que en los espacios m\u00e9tricos, &#92;(d(x,y) \u2265 0&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Topology.MetricSpace.Basic\nvariable {X : Type _} [MetricSpace X]\nvariable (x y : X)\n\nexample : 0 \u2264 d x y :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1n los siguientes lemas:<br \/>\n&#92;begin{align}<br \/>\n   &amp;0 \u2264 ab \u2192 0 &lt; b \u2192 0 \u2264 a   &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;d(x,x) = 0               &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;d(x,z) \u2264 d(x,y) + d(y,z) &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;d(x,y) = d(y,x)          &#92;tag{L4} &#92;&#92;<br \/>\n   &amp;2a = a + a               &#92;tag{L5} &#92;&#92;<br \/>\n   &amp;0 &lt; 2                    &#92;tag{L6} &#92;&#92;<br \/>\n&#92;end{align}<\/p>\n<p>Por L1 es suficiente demostrar las siguientes desigualdades:<br \/>\n&#92;begin{align}<br \/>\n   0 &amp;\u2264 2d(x,y) &#92;tag{1} &#92;&#92;<br \/>\n   0 &amp;&lt; 2       &#92;tag{2}<br \/>\n&#92;end{align}<\/p>\n<p>La (1) se demuestra por las siguiente cadena de desigualdades:<br \/>\n&#92;begin{align}<br \/>\n   0 &amp;= d(x,x)             &amp;&amp;&#92;text{[por L2]} &#92;&#92;<br \/>\n     &amp;\u2264 d(x,y) + d(y,x)    &amp;&amp;&#92;text{[por L3]} &#92;&#92;<br \/>\n     &amp;= d(x,y) + d(x,y)    &amp;&amp;&#92;text{[por L4]} &#92;&#92;<br \/>\n     &amp;= 2 d(x,y)           &amp;&amp;&#92;text{[por L5]}<br \/>\n&#92;end{align}<\/p>\n<p>La (2) se tiene por L6.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Topology.MetricSpace.Basic\nvariable {X : Type _} [MetricSpace X]\nvariable (x y : X)\n\n-- 1\u00aa demostraci\u00f3n\nexample : 0 \u2264 dist x y :=\nby\n  have h1 : 0 \u2264 dist x y * 2 := calc\n    0 = dist x x            := (dist_self x).symm\n    _ \u2264 dist x y + dist y x := dist_triangle x y x\n    _ = dist x y + dist x y := by rw [dist_comm x y]\n    _ = dist x y * 2        := (mul_two (dist x y)).symm\n  show 0 \u2264 dist x y\n  exact nonneg_of_mul_nonneg_left h1 zero_lt_two\n\n-- 2\u00aa demostraci\u00f3n\nexample : 0 \u2264 dist x y :=\nby\n  apply nonneg_of_mul_nonneg_left\n  . -- 0 \u2264 dist x y * 2\n    calc 0 = dist x x            := by simp only [dist_self]\n         _ \u2264 dist x y + dist y x := by simp only [dist_triangle]\n         _ = dist x y + dist x y := by simp only [dist_comm]\n         _ = dist x y * 2        := by simp only [mul_two]\n  . -- 0 < 2\n    exact zero_lt_two\n\n-- 3\u00aa demostraci\u00f3n\nexample : 0 \u2264 dist x y :=\nby\n  have : 0 \u2264 dist x y + dist y x := by\n    rw [\u2190 dist_self x]\n    apply dist_triangle\n  linarith [dist_comm x y]\n\n-- 3\u00aa demostraci\u00f3n\nexample : 0 \u2264 dist x y :=\n-- by apply?\ndist_nonneg\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- variable (z : X)\n-- #check (dist_comm x y : dist x y = dist y x)\n-- #check (dist_nonneg : 0 \u2264 dist x y)\n-- #check (dist_self x : dist x x = 0)\n-- #check (dist_triangle x y z : dist x z \u2264 dist x y + dist y z)\n-- #check (mul_two a : a * 2 = a + a)\n-- #check (nonneg_of_mul_nonneg_left : 0 \u2264 a * b \u2192 0 < b \u2192 0 \u2264 a)\n-- #check (zero_lt_two : 0 < 2)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Ejercicio_en_espacios_metricos.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 22.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. En \u211d, {0 &lt; \u03b5, \u03b5 \u2264 1, |x| &lt; \u03b5, |y| &lt; \u03b5} \u22a2 |xy| &lt; \u03b5<\/h3>\n<p>Demostrar con Lean4, que en \u211d<br \/>\n&#92;[ &#92;left&#92;{ 0 &lt; \u03b5, \u03b5 \u2264 1, |x| &lt; \u03b5, |y| &lt; \u03b5 &#92;right&#92;} \u22a2 |xy| &lt; \u03b5 &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nexample :\n  \u2200 {x y \u03b5 : \u211d}, 0 < \u03b5 \u2192 \u03b5 \u2264 1 \u2192 |x| < \u03b5 \u2192 |y| < \u03b5 \u2192 |x * y| < \u03b5 :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1n los siguientes lemas<br \/>\n&#92;begin{align}<br \/>\n   &amp;|a\u00b7b| = |a|\u00b7|b|            &#92;tag{L1} &#92;&#92;<br \/>\n   &amp;0\u00b7a = 0                    &#92;tag{L2} &#92;&#92;<br \/>\n   &amp;0 \u2264 |a|                    &#92;tag{L3} &#92;&#92;<br \/>\n   &amp;a \u2264 b \u2192 a \u2260 b \u2192 a &lt; b      &#92;tag{L4} &#92;&#92;<br \/>\n   &amp;a \u2260 b \u2194 b \u2260 a              &#92;tag{L5} &#92;&#92;<br \/>\n   &amp;0 &lt; a \u2192 (ab &lt; ac \u2194 b &lt; c)  &#92;tag{L6} &#92;&#92;<br \/>\n   &amp;0 &lt; a \u2192 (ba &lt; ca \u2194 b &lt; c)  &#92;tag{L7} &#92;&#92;<br \/>\n   &amp;0 &lt; a \u2192 (ba \u2264 ca \u2194 b \u2264 c)  &#92;tag{L8} &#92;&#92;<br \/>\n   &amp;1\u00b7a = a                    &#92;tag{L9} &#92;&#92;<br \/>\n&#92;end{align}<\/p>\n<p>Sean &#92;(x, y, \u03b5 \u2208 \u211d&#92;) tales que<br \/>\n&#92;begin{align}<br \/>\n   0   &amp;&lt; \u03b5 &#92;tag{he1} &#92;&#92;<br \/>\n   \u03b5   &amp;\u2264 1 &#92;tag{he2} &#92;&#92;<br \/>\n   |x| &amp;&lt; \u03b5 &#92;tag{hx} &#92;&#92;<br \/>\n   |y| &amp;&lt; \u03b5 &#92;tag{hy}<br \/>\n&#92;end{align}<br \/>\ny tenemos que demostrar que<br \/>\n&#92;[   |xy| &lt; \u03b5 &#92;]<br \/>\nLo haremos distinguiendo caso seg\u00fan &#92;(|x| = 0&#92;).<\/p>\n<p>1\u00ba caso. Supongamos que<br \/>\n&#92;[   |x| = 0 &#92;tag{1} &#92;]<br \/>\nEntonces,<br \/>\n&#92;begin{align}<br \/>\n   |xy| &amp;= |x||y|    &amp;&amp;&#92;text{[por L1]} &#92;&#92;<br \/>\n        &amp;= 0|y|      &amp;&amp;&#92;text{[por h1]} &#92;&#92;<br \/>\n        &amp;= 0         &amp;&amp;&#92;text{[por L2]} &#92;&#92;<br \/>\n        &amp;&lt; \u03b5         &amp;&amp;&#92;text{[por he1]}<br \/>\n&#92;end{align}<\/p>\n<p>2\u00ba caso. Supongamos que<br \/>\n&#92;[ |x| \u2260 0 &#92;tag{2} &#92;]<br \/>\nEntonces, por L4, L3 y L5, se tiene<br \/>\n&#92;[ 0 &lt; x &#92;tag{3} &#92;]<br \/>\ny, por tanto,<br \/>\n&#92;begin{align}<br \/>\n   |xy| &amp;= |x||y|    &amp;&amp;&#92;text{[por L1]} &#92;&#92;<br \/>\n        &amp;&lt; |x|\u03b5      &amp;&amp;&#92;text{[por L6, (3) y (hy)]} &#92;&#92;<br \/>\n        &amp;&lt; \u03b5\u03b5        &amp;&amp;&#92;text{[por L7, (he1) y (hx)]} &#92;&#92;<br \/>\n        &amp;\u2264 1\u03b5        &amp;&amp;&#92;text{[por L8, (he1) y (he2)]} &#92;&#92;<br \/>\n        &amp;= \u03b5         &amp;&amp;&#92;text{[por L9]}<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\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 :=\nby\n  intros x y \u03b5 he1 he2 hx hy\n  by_cases h : (|x| = 0)\n  . -- h : |x| = 0\n    show |x * y| < \u03b5\n    calc\n      |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  . -- h : \u00ac|x| = 0\n    have h1 : 0 < |x| := by\n      have h2 : 0 \u2264 |x| := abs_nonneg x\n      show 0 < |x|\n      exact lt_of_le_of_ne h2 (ne_comm.mpr h)\n    show |x * y| < \u03b5\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\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 :=\nby\n  intros x y \u03b5 he1 he2 hx hy\n  by_cases (|x| = 0)\n  . -- h : |x| = 0\n    show |x * y| < \u03b5\n    calc\n      |x * y| = |x| * |y| := by apply abs_mul\n            _ = 0 * |y|   := by rw [h]\n            _ = 0         := by apply zero_mul\n            _ < \u03b5         := by apply he1\n  . -- h : \u00ac|x| = 0\n    have h1 : 0 < |x| := by\n      have h2 : 0 \u2264 |x| := by apply abs_nonneg\n      exact lt_of_le_of_ne h2 (ne_comm.mpr h)\n    show |x * y| < \u03b5\n    calc\n      |x * y| = |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]\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 :=\nby\n  intros x y \u03b5 he1 he2 hx hy\n  by_cases (|x| = 0)\n  . -- h : |x| = 0\n    show |x * y| < \u03b5\n    calc |x * y| = |x| * |y| := by simp only [abs_mul]\n               _ = 0 * |y|   := by simp only [h]\n               _ = 0         := by simp only [zero_mul]\n               _ < \u03b5         := by simp only [he1]\n  . -- h : \u00ac|x| = 0\n    have h1 : 0 < |x| := by\n      have h2 : 0 \u2264 |x| := by simp only [abs_nonneg]\n      exact lt_of_le_of_ne h2 (ne_comm.mpr h)\n    show |x * y| < \u03b5\n    calc\n      |x * y| = |x| * |y| := by simp [abs_mul]\n            _ < |x| * \u03b5   := by simp only [mul_lt_mul_left, h1, hy]\n            _ < \u03b5 * \u03b5     := by simp only [mul_lt_mul_right, he1, hx]\n            _ \u2264 1 * \u03b5     := by simp only [mul_le_mul_right, he1, he2]\n            _ = \u03b5         := by simp only [one_mul]\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : \u211d)\n-- #check (abs_mul a b : |a * b| = |a| * |b|)\n-- #check (abs_nonneg a : 0 \u2264 |a|)\n-- #check (lt_of_le_of_ne : a \u2264 b \u2192 a \u2260 b \u2192 a < b)\n-- #check (mul_le_mul_right : 0 < a \u2192 (b * a \u2264 c * a \u2194 b \u2264 c))\n-- #check (mul_lt_mul_left : 0 < a \u2192 (a * b < a * c \u2194 b < c))\n-- #check (mul_lt_mul_right : 0 < a \u2192 (b * a < c * a \u2194 b < c))\n-- #check (ne_comm : a \u2260 b \u2194 b \u2260 a)\n-- #check (one_mul a : 1 * a = a)\n-- #check (zero_mul a : 0 * a = 0)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Acotacion_del_producto.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 24.<\/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 con Lean4 que si &#92;(f&#92;) y &#92;(g&#92;) son funciones de &#92;(\u211d&#92;) en &#92;(\u211d&#92;), entonces la suma de una cota superior de &#92;(f&#92;) y una cota superior de &#92;(g&#92;) es una cota superior de &#92;(f+g&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\n-- (CotaSuperior f a) se verifica si a es una cota superior de f.\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\nvariable (f g : \u211d \u2192 \u211d)\nvariable (a b : \u211d)\n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  : CotaSuperior (f + g) (a + b) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 el siguiente lema<br \/>\n&#92;[ &#92;{a \u2264 b, c \u2264 d&#92;} &#92;vdash a + c \u2264 b + d &#92;tag{L1} &#92;]<\/p>\n<p>Por la definici\u00f3n de cota superior, hay que demostrar que<br \/>\n&#92;[ (\u2200 x \u2208 \u211d) [f(x) + g(x) \u2264 a + b] &#92;tag{1} &#92;]<br \/>\nPara ello, sea &#92;(x \u2208 R&#92;). Puesto que &#92;(a&#92;) es una cota superior de &#92;(f&#92;), se tiene que<br \/>\n&#92;[ f(x) \u2264 a &#92;tag{2} &#92;]<br \/>\ny, puesto que &#92;(b&#92;) es una cota superior de &#92;(g&#92;), se tiene que<br \/>\n&#92;[ g(x) \u2264 b &#92;tag{3} &#92;]<br \/>\nDe (2) y (3), por L1, se tiene que<br \/>\n&#92;[ f(x) + g(x) \u2264 a + b &#92;]<br \/>\nque es lo que hab\u00eda que demostrar.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\n-- (CotaSuperior f a) se verifica si a es una cota superior de f.\ndef CotaSuperior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, f x \u2264 a\n\nvariable (f g : \u211d \u2192 \u211d)\nvariable (a b : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  : CotaSuperior (f + g) (a + b) :=\nby\n  have h1 : \u2200 x, (f + g) x  \u2264 a + b := by\n  { intro x\n    have h2 : f x \u2264 a := hfa x\n    have h3 : g x \u2264 b := hgb x\n    show (f + g) x \u2264 a + b\n    exact add_le_add h2 h3 }\n  show CotaSuperior (f + g) (a + b)\n  exact h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  : CotaSuperior (f + g) (a + b) :=\nby\n  have h1 : \u2200 x, (f + g) x \u2264 a + b := by\n  { intro x\n    show (f + g) x \u2264 a + b\n    exact add_le_add (hfa x) (hgb x) }\n  show CotaSuperior (f + g) (a + b)\n  exact h1\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  : CotaSuperior (f + g) (a + b) :=\nby\n  intro x\n  dsimp\n  apply add_le_add\n  . apply hfa\n  . apply hgb\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  : CotaSuperior (f + g) (a + b) :=\n\u03bb x \u21a6 add_le_add (hfa x) (hgb x)\n\n-- Lemas usados\n-- ============\n\n-- variable (c d : \u211d)\n-- #check (add_le_add : a \u2264 b \u2192 c \u2264 d \u2192 a + c \u2264 b + d)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Suma_de_cotas_superiores.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 25.<\/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 con Lean4 que si &#92;(f&#92;) y &#92;(g&#92;) son funciones de &#92;(\u211d&#92;) en &#92;(\u211d&#92;), entonces la suma de una cota inferior de &#92;(f&#92;) y una cota inferior de &#92;(g&#92;) es una cota inferior de &#92;(f+g&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\n-- (CotaInferior f a) expresa que a es una cota inferior de f.\ndef CotaInferior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, a \u2264 f x\n\nvariable (f g : \u211d \u2192 \u211d)\nvariable (a b : \u211d)\n\nexample\n  (hfa : CotaInferior f a)\n  (hgb : CotaInferior g b)\n  : CotaInferior (f + g) (a + b) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 el siguiente lema<br \/>\n&#92;[ a \u2264 b \u2192 c \u2264 d \u2192 a + c \u2264 b + d &#92;tag{L1} &#92;]<\/p>\n<p>Por la definici\u00f3n de cota inferior, hay que demostrar que<br \/>\n&#92;[ (\u2200 x \u2208 \u211d) [a + b \u2264 f(x) + g(x)] &#92;tag{1} &#92;]<br \/>\nPara ello, sea &#92;(x \u2208 R&#92;). Puesto que es &#92;(a&#92;) es una cota inferior de &#92;(f&#92;), se tiene que<br \/>\n&#92;[ a \u2264 f(x) &#92;tag{2} &#92;]<br \/>\ny, puesto que &#92;(b&#92;) es una cota inferior de &#92;(g&#92;), se tiene que<br \/>\n&#92;[ b \u2264 g(x) &#92;tag{3} &#92;]<br \/>\nDe (2) y (3), por L1, se tiene que<br \/>\n&#92;[ a + b \u2264 f(x) + g(x) &#92;]<br \/>\nque es lo que hab\u00eda que demostrar.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\n-- (CotaInferior f a) expresa que a es una cota inferior de f.\ndef CotaInferior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, a \u2264 f x\n\nvariable (f g : \u211d \u2192 \u211d)\nvariable (a b : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaInferior f a)\n  (hgb : CotaInferior g b)\n  : CotaInferior (f + g) (a + b) :=\nby\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    exact add_le_add h1a h1b }\n  show CotaInferior (f + g) (a + b)\n  exact h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaInferior f a)\n  (hgb : CotaInferior g b)\n  : CotaInferior (f + g) (a + b) :=\nby\n  have h1 : \u2200 x, a + b \u2264 f x + g x\n  { intro x\n    show a + b \u2264 f x + g x\n    exact add_le_add (hfa x) (hgb x) }\n  show CotaInferior (f + g) (a + b)\n  exact h1\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaInferior f a)\n  (hgb : CotaInferior g b)\n  : CotaInferior (f + g) (a + b) :=\nby\n  intro x\n  dsimp\n  apply add_le_add\n  . apply hfa\n  . apply hgb\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaInferior f a)\n  (hgb : CotaInferior g b)\n  : CotaInferior (f + g) (a + b) :=\n\u03bb x \u21a6 add_le_add (hfa x) (hgb x)\n\n-- Lemas usados\n-- ============\n\n-- variable (c d : \u211d)\n-- #check (add_le_add : a \u2264 b \u2192 c \u2264 d \u2192 a + c \u2264 b + d)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Suma_de_cotas_inferiores.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 25.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. El producto de funciones no negativas es no negativo<\/h3>\n<p>Demostrar con Lean4 que si &#92;(f&#92;) y &#92;(g&#92;) son funciones no negativas de &#92;(\u211d&#92;) en &#92;(\u211d&#92;), entonces su producto es no negativo.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\n-- (CotaInferior f a) expresa que a es una cota inferior de f.\ndef CotaInferior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, a \u2264 f x\n\nvariable (f g : \u211d \u2192 \u211d)\n\nexample\n  (nnf : CotaInferior f 0)\n  (nng : CotaInferior g 0)\n  : CotaInferior (f * g) 0 :=\nby\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 el siguiente lema<br \/>\n&#92;[ &#92;{0 \u2264 a, 0 \u2264 b&#92;} &#92;vdash 0 \u2264 ab &#92;tag{L1} &#92;]<\/p>\n<p>Hay que demostrar que<br \/>\n&#92;[ (\u2200 x \u2208 \u211d) [0 \u2264 f(x)g(x)] &#92;tag{1} &#92;]<br \/>\nPara ello, sea &#92;(x \u2208 R&#92;). Puesto que &#92;(f&#92;) es no negatica, se tiene que<br \/>\n&#92;[ 0 \u2264 f(x) &#92;tag{2} &#92;]<br \/>\ny, puesto que &#92;(g&#92;) es no negativa, se tiene que<br \/>\n&#92;[ 0 \u2264 g(x) &#92;tag{3} &#92;]<br \/>\nDe (2) y (3), por L1, se tiene que<br \/>\n&#92;[ 0 \u2264 f(x)g(x) &#92;]<br \/>\nque es lo que hab\u00eda que demostrar.<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\n-- (CotaInferior f a) expresa que a es una cota inferior de f.\ndef CotaInferior (f : \u211d \u2192 \u211d) (a : \u211d) : Prop :=\n  \u2200 x, a \u2264 f x\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (nnf : CotaInferior f 0)\n  (nng : CotaInferior g 0)\n  : CotaInferior (f * g) 0 :=\nby\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    exact mul_nonneg h2 h3 }\n  show CotaInferior (f * g) 0\n  exact h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (nnf : CotaInferior f 0)\n  (nng : CotaInferior g 0)\n  : CotaInferior (f * g) 0 :=\nby\n  have h1 : \u2200x, 0 \u2264 f x * g x\n  { intro x\n    show 0 \u2264 f x * g x\n    exact mul_nonneg (nnf x) (nng x) }\n  show CotaInferior (f * g) 0\n  exact h1\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (nnf : CotaInferior f 0)\n  (nng : CotaInferior g 0)\n  : CotaInferior (f * g) 0 :=\nby\n  intro x\n  dsimp\n  apply mul_nonneg\n  . apply nnf\n  . apply nng\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (nnf : CotaInferior f 0)\n  (nng : CotaInferior g 0)\n  : CotaInferior (f * g) 0 :=\n\u03bb x \u21a6 mul_nonneg (nnf x) (nng x)\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (mul_nonneg : 0 \u2264 a \u2192 0 \u2264 b \u2192 0 \u2264 a * b)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Producto_de_funciones_no_negativas.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 25.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. En los espacios m\u00e9tricos, d(x,y) \u2265 0 2. En \u211d, {0 &lt; \u03b5, \u03b5 \u2264 1, |x| &lt; \u03b5, |y| &lt; \u03b5} \u22a2 |xy| &lt; \u03b5 3. La suma de una cota superior de f y una cota superior de&#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\/8032"}],"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=8032"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8032\/revisions"}],"predecessor-version":[{"id":8033,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8032\/revisions\/8033"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8032"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8032"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8032"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}