{"id":8035,"date":"2023-10-14T16:42:06","date_gmt":"2023-10-14T14:42:06","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8035"},"modified":"2023-10-14T16:42:06","modified_gmt":"2023-10-14T14:42:06","slug":"14-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/14-oct-23\/","title":{"rendered":"La semana en Calculemus (14 de octubre de 2023)"},"content":{"rendered":"\n<p>Esta 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. Si a es una cota superior no negativa de f y b es es una cota superior de la funci\u00f3n no negativa g, entonces ab es una cota superior de fg<\/a><\/li>\n<li><a href=\"#ej2\">2. La suma de dos funciones mon\u00f3tonas es mon\u00f3tona<\/a><\/li>\n<li><a href=\"#ej3\">3. Si c es no negativo y f es mon\u00f3tona, entonces cf es mon\u00f3tona<\/a><\/li>\n<li><a href=\"#ej4\">4. La composici\u00f3n de dos funciones mon\u00f3tonas es mon\u00f3tona<\/a><\/li>\n<li><a href=\"#ej5\">5. La suma de dos funciones pares es par<\/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 es una cota superior no negativa de f y b es es una cota superior de la funci\u00f3n no negativa g, entonces ab es una cota superior de fg<\/h3>\n<p>Sean &#92;(f&#92;) y &#92;(g&#92;) funciones de &#92;(\u211d&#92;) en &#92;(\u211d&#92;). Demostrar con Lean4 que si &#92;(a&#92;) es una cota superior no negativa de &#92;(f&#92;) y &#92;(b&#92;) es es una cota superior de la funci\u00f3n no negativa &#92;(g&#92;), entonces &#92;(ab&#92;) es una cota superior de &#92;(fg&#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\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 : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  (nng : CotaInferior g 0)\n  (nna : 0 \u2264 a)\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, 0 \u2264 c, 0 \u2264 b&#92;} \u22a2 ac \u2264 bd &#92;tag{L1} &#92;]<\/p>\n<p>Hay que demostrar que<br \/>\n&#92;[ (\u2200 x \u2208 \u211d) [f(x)g(x) \u2264 ab] &#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 \/>\npuesto 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 \/>\npuesto que &#92;(g&#92;) es no negativa, se tiene que<br \/>\n&#92;[ 0 \u2264 g(x) &#92;tag{4} &#92;]<br \/>\ny, puesto que &#92;(a&#92;) es no negativo, se tiene que<br \/>\n&#92;[ 0 \u2264 a &#92;tag{5} &#92;]<br \/>\nDe (2), (3), (4) y (5), por L1, se tiene que<br \/>\n&#92;[ f(x)g(x) \u2264 ab &#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\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 : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  (nng : CotaInferior g 0)\n  (nna : 0 \u2264 a)\n  : CotaSuperior (f * g) (a * b) :=\nby\n  have h1 : \u2200 x, f x * g x \u2264 a * b\n  { intro x\n    have h2 : f x \u2264 a := hfa x\n    have h3 : g x \u2264 b := hgb x\n    have h4 : 0 \u2264 g x := nng x\n    show f x * g x \u2264 a * b\n    exact mul_le_mul h2 h3 h4 nna }\n  show CotaSuperior (f * g) (a * b)\n  exact h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  (nng : CotaInferior g 0)\n  (nna : 0 \u2264 a)\n  : CotaSuperior (f * g) (a * b) :=\nby\n  intro x\n  dsimp\n  apply mul_le_mul\n  . apply hfa\n  . apply hgb\n  . apply nng\n  . apply nna\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  (nng : CotaInferior g 0)\n  (nna : 0 \u2264 a)\n  : CotaSuperior (f * g) (a * b) :=\nby\n  intro x\n  have h1:= hfa x\n  have h2:= hgb x\n  have h3:= nng x\n  exact mul_le_mul h1 h2 h3 nna\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  (nng : CotaInferior g 0)\n  (nna : 0 \u2264 a)\n  : CotaSuperior (f * g) (a * b) :=\nby\n  intro x\n  specialize hfa x\n  specialize hgb x\n  specialize nng x\n  exact mul_le_mul hfa hgb nng nna\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (hfa : CotaSuperior f a)\n  (hgb : CotaSuperior g b)\n  (nng : CotaInferior g 0)\n  (nna : 0 \u2264 a)\n  : CotaSuperior (f * g) (a * b) :=\n\u03bb x \u21a6 mul_le_mul (hfa x) (hgb x) (nng x) nna\n\n-- Lemas usados\n-- ============\n\n-- variable (c d : \u211d)\n-- #check (mul_le_mul : a \u2264 b \u2192 c \u2264 d \u2192 0 \u2264 c \u2192 0 \u2264 b \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\/Cota_superior_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. 25.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. La suma de dos funciones mon\u00f3tonas es mon\u00f3tona<\/h3>\n<p>Demostrar con Lean4 que la suma de dos funciones mon\u00f3tonas es mon\u00f3tona.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f + g) :=\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;} \u22a2 a + c \u2264 b + d &#92;tag{L1} &#92;]<\/p>\n<p>Supongamos que &#92;(f&#92;) y &#92;(g&#92;) son mon\u00f3tonas y teneno que demostrar que &#92;(f+g&#92;) tambi\u00e9n lo es; que<br \/>\n&#92;[ (\u2200 a,&#92; b &#92;in \u211d) [a \u2264 b \u2192 (f + g)(a) \u2264 (f + g)(b)] &#92;]<br \/>\nSean &#92;(a, b \u2208 \u211d&#92;) tales que<br \/>\n&#92;[ a \u2264 b &#92;tag{1} &#92;]<br \/>\nEntonces, por ser &#92;(f&#92;) y &#92;(g&#92;) mon\u00f3tonas se tiene<br \/>\n&#92;begin{align}<br \/>\n   f(a) &amp;\u2264 f(b) &#92;tag{2} &#92;&#92;<br \/>\n   g(a) &amp;\u2264 g(b) &#92;tag{3}<br \/>\n&#92;end{align}<br \/>\nEntonces,<br \/>\n&#92;begin{align}<br \/>\n   (f + g)(a) &amp;= f(a) + g(a)    &#92;&#92;<br \/>\n              &amp;\u2264 f(b) + g(b)    &amp;&amp;&#92;text{[por L1, (2) y (3)]} &#92;&#92;<br \/>\n              &amp;= (f + g)(b)<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f + g) :=\nby\n  have h1 : \u2200 a b, a \u2264 b \u2192 (f + g) a \u2264 (f + g) b\n  { intros a b hab\n    have h2 : f a \u2264 f b := mf hab\n    have h3 : g a \u2264 g b := mg hab\n    calc (f + g) a\n         = f a + g a := rfl\n       _ \u2264 f b + g b := add_le_add h2 h3\n       _ = (f + g) b := rfl }\n  show Monotone (f + g)\n  exact h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f + g) :=\nby\n  have h1 : \u2200 a b, a \u2264 b \u2192 (f + g) a \u2264 (f + g) b\n  { intros a b hab\n    calc (f + g) a\n         = f a + g a := rfl\n       _ \u2264 f b + g b := add_le_add (mf hab) (mg hab)\n       _ = (f + g) b := rfl }\n  show Monotone (f + g)\n  exact h1\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f + g) :=\nby\n  have h1 : \u2200 a b, a \u2264 b \u2192 (f + g) a \u2264 (f + g) b\n  { intros a b hab\n    show (f + g) a \u2264 (f + g) b\n    exact add_le_add (mf hab) (mg hab) }\n  show Monotone (f + g)\n  exact h1\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f + g) :=\nby\n  -- a b : \u211d\n  -- hab : a \u2264 b\n  intros a b hab\n  apply add_le_add\n  . -- f a \u2264 f b\n    apply mf hab\n  . --  g a \u2264 g b\n    apply mg hab\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f + g) :=\n\u03bb _ _ hab \u21a6 add_le_add (mf hab) (mg hab)\n\n-- Lemas usados\n-- ============\n\n-- variable (a b 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:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Suma_de_funciones_monotonas.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. 26.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si c es no negativo y f es mon\u00f3tona, entonces cf es mon\u00f3tona<\/h3>\n<p>Demostrar con Lean4 que si &#92;(c&#92;) es no negativo y &#92;(f&#92;) es mon\u00f3tona, entonces &#92;(cf&#92;) es mon\u00f3tona.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (f : \u211d \u2192 \u211d)\nvariable {c : \u211d}\n\nexample\n  (mf : Monotone f)\n  (nnc : 0 \u2264 c)\n  : Monotone (fun x \u21a6 c * f x) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Se usar\u00e1 el Lema<br \/>\n&#92;[ &#92;{b \u2264 c, 0 \u2264 a&#92;} \u22a2 ab \u2264 ac &#92;tag{L1} &#92;]<\/p>\n<p>Tenemos que demostrar que<br \/>\n&#92;[ (\u2200 a, b \u2208 \u211d) [a \u2264 b \u2192 (cf)(a) \u2264 (cf)(b)] &#92;]<br \/>\nSean &#92;(a, b \u2208 \u211d&#92;) tales que &#92;(a \u2264 b&#92;). Puesto que &#92;(f&#92;) es mon\u00f3tona, se tiene<br \/>\n&#92;[ f(a) \u2264 f(b) &#92;]<br \/>\ny, junto con la hip\u00f3tesis de que &#92;(c&#92;) es no negativo, usando el lema L1, se tiene que<br \/>\n&#92;[ cf(a) \u2264 cf(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\nvariable (f : \u211d \u2192 \u211d)\nvariable {c : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (nnc : 0 \u2264 c)\n  : Monotone (fun x \u21a6 c * f x) :=\nby\n  have h1 : \u2200 a b, a \u2264 b \u2192 (fun x \u21a6 c * f x) a \u2264 (fun x \u21a6 c * f x) b\n  { intros a b hab\n    have h2 : f a \u2264 f b := mf hab\n    show (fun x \u21a6 c * f x) a \u2264 (fun x \u21a6 c * f x) b\n    exact mul_le_mul_of_nonneg_left h2 nnc }\n  show Monotone (fun x \u21a6 c * f x)\n  exact h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (nnc : 0 \u2264 c)\n  : Monotone (fun x \u21a6 c * f x) :=\nby\n  -- a b : \u211d\n  -- hab : a \u2264 b\n  intros a b hab\n  -- (fun x => c * f x) a \u2264 (fun x => c * f x) b\n  apply mul_le_mul_of_nonneg_left\n  . -- f a \u2264 f b\n    apply mf hab\n  . -- 0 \u2264 c\n    apply nnc\n\n-- 3\u00aa demostraci\u00f3n\nexample (mf : Monotone f) (nnc : 0 \u2264 c) :\n  Monotone (fun x \u21a6 c * f x) :=\n\u03bb _ _ hab \u21a6 mul_le_mul_of_nonneg_left (mf hab) nnc\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : \u211d)\n-- #check (mul_le_mul_of_nonneg_left : b \u2264 c \u2192 0 \u2264 a \u2192 a * b \u2264 a * c)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Producto_de_un_positivo_por_una_funcion_monotona.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. 26.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. La composici\u00f3n de dos funciones mon\u00f3tonas es mon\u00f3tona<\/h3>\n<p>Demostrar con Lean4 que la composici\u00f3n de dos funciones mon\u00f3tonas es mon\u00f3tona.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f \u2218 g) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Sean &#92;(f&#92;) y &#92;(g&#92;) dos funciones mon\u00f3tonas de &#92;(\u211d&#92;) en &#92;(\u211d&#92;). Tenemos que demostrar que &#92;(f \u2218 g&#92;) es mon\u00f3tona; es decir, que<br \/>\n&#92;[ (\u2200 a, b \u2208 \u211d) [a \u2264 b \u2192 (f \u2218 g)(a) \u2264 (f \u2218 g)(b)] &#92;]<br \/>\nSean &#92;(a, b \u2208 \u211d&#92;) tales que &#92;(a \u2264 b&#92;). Por ser &#92;(g&#92;) mon\u00f3tona, se tiene<br \/>\n&#92;[ g(a) \u2264 g(b) &#92;]<br \/>\ny, por ser f mon\u00f3tona, se tiene<br \/>\n&#92;[ f(g(a)) \u2264 f(g(b)) &#92;]<br \/>\nFinalmente, por la definici\u00f3n de composici\u00f3n,<br \/>\n&#92;[ (f \u2218 g)(a) \u2264 (f \u2218 g)(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\nvariable (f g : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f \u2218 g) :=\nby\n  have h1 : \u2200 a b, a \u2264 b \u2192 (f \u2218 g) a \u2264 (f \u2218 g) b\n  { intros a b hab\n    have h1 : g a \u2264 g b := mg hab\n    show (f \u2218 g) a \u2264 (f \u2218 g) b\n    exact mf h1 }\n  show Monotone (f \u2218 g)\n  exact h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f \u2218 g) :=\nby\n  have h1 : \u2200 a b, a \u2264 b \u2192 (f \u2218 g) a \u2264 (f \u2218 g) b\n  { intros a b hab\n    show (f \u2218 g) a \u2264 (f \u2218 g) b\n    exact mf (mg hab) }\n  show Monotone (f \u2218 g)\n  exact h1\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (mf : Monotone f)\n  (mg : Monotone g)\n  : Monotone (f \u2218 g) :=\nby\n  -- a b : \u211d\n  -- hab : a \u2264 b\n  intros a b hab\n  -- (f \u2218 g) a \u2264 (f \u2218 g) b\n  apply mf\n  -- g a \u2264 g b\n  apply mg\n  -- a \u2264 b\n  apply hab\n\n-- 4\u00aa demostraci\u00f3n\nexample (mf : Monotone f) (mg : Monotone g) :\n  Monotone (f \u2218 g) :=\n\u03bb _ _ hab \u21a6 mf (mg hab)\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Composicion_de_funciones_monotonas.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. 26.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. La suma de dos funciones pares es par<\/h3>\n<p>Demostrar con Lean4 que la suma de dos funciones pares es par.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- (esPar f) expresa que f es par.\ndef esPar (f : \u211d \u2192 \u211d) : Prop :=\n  \u2200 x, f x = f (-x)\n\nexample\n  (h1 : esPar f)\n  (h2 : esPar g)\n  : esPar (f + g) :=\nby sorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p>Supongamos que &#92;(f&#92;) y &#92;(g&#92;) son funciones pares. Tenemos que demostrar que &#92;(f+g&#92;) es par; es decir, que<br \/>\n&#92;[ (\u2200 x \u2208 \u211d) [(f + g)(x) = (f + g)(-x)] &#92;]<br \/>\nSea &#92;(x \u2208 \u211d&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   (f + g) x &amp;= f(x) + g(x)   &#92;&#92;<br \/>\n             &amp;= f(-x) + g(x)  &amp;&amp;&#92;text{[porque &#92;(f&#92;) es par]} &#92;&#92;<br \/>\n             &amp;= f(-x) + g(-x) &amp;&amp;&#92;text{[porque &#92;(g&#92;) es par]} &#92;&#92;<br \/>\n             &amp;= (f + g)(-x)<br \/>\n&#92;end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- (esPar f) expresa que f es par.\ndef esPar (f : \u211d \u2192 \u211d) : Prop :=\n  \u2200 x, f x = f (-x)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : esPar f)\n  (h2 : esPar g)\n  : esPar (f + g) :=\nby\n  intro x\n  have h1 : f x = f (-x) := h1 x\n  have h2 : g x = g (-x) := h2 x\n  calc (f + g) x\n       = f x + g x       := rfl\n     _ = f (-x) + g x    := congrArg (. + g x) h1\n     _ = f (-x) + g (-x) := congrArg (f (-x) + .) h2\n     _ = (f + g) (-x)    := rfl\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : esPar f)\n  (h2 : esPar g)\n  : esPar (f + g) :=\nby\n  intro x\n  calc (f + g) x\n       = f x + g x       := rfl\n     _ = f (-x) + g x    := congrArg (. + g x) (h1 x)\n     _ = f (-x) + g (-x) := congrArg (f (-x) + .) (h2 x)\n     _ = (f + g) (-x)    := rfl\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h1 : esPar f)\n  (h2 : esPar g)\n  : esPar (f + g) :=\nby\n  intro x\n  calc (f + g) x\n       = f x + g x       := rfl\n     _ = f (-x) + g (-x) := by rw [h1, h2]\n     _ = (f + g) (-x)    := rfl\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Suma_funciones_pares.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. 26.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. Si a es una cota superior no negativa de f y b es es una cota superior de la funci\u00f3n no negativa g, entonces ab es una cota superior de fg 2. La suma de dos funciones mon\u00f3tonas es mon\u00f3tona&#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\/8035"}],"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=8035"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8035\/revisions"}],"predecessor-version":[{"id":8036,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8035\/revisions\/8036"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8035"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8035"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8035"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}