Sean \(f\) y \(g\) funciones de \(\u211d\) en \(\u211d\). Demostrar con Lean4 que 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\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\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>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSe usar\u00e1 el siguiente lema
\n\[ \{a \u2264 b, c \u2264 d, 0 \u2264 c, 0 \u2264 b\} \u22a2 ac \u2264 bd \tag{L1} \]<\/p>\n
Hay que demostrar que
\n\[ (\u2200 x \u2208 \u211d) [f(x)g(x) \u2264 ab] \tag{1} \]
\nPara ello, sea \(x \u2208 R\). Puesto que \(a\) es una cota superior de \(f\), se tiene que
\n\[ f(x) \u2264 a \tag{2} \]
\npuesto que \(b\) es una cota superior de \(g\), se tiene que
\n\[ g(x) \u2264 b \tag{3} \]
\npuesto que \(g\) es no negativa, se tiene que
\n\[ 0 \u2264 g(x) \tag{4} \]
\ny, puesto que \(a\) es no negativo, se tiene que
\n\[ 0 \u2264 a \tag{5} \]
\nDe (2), (3), (4) y (5), por L1, se tiene que
\n\[ f(x)g(x) \u2264 ab \]
\nque es lo que hab\u00eda que demostrar.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\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>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n