{"id":1639,"date":"2023-10-06T06:00:51","date_gmt":"2023-10-06T04:00:51","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1639"},"modified":"2023-10-10T12:10:07","modified_gmt":"2023-10-10T10:10:07","slug":"06-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/06-oct-23\/","title":{"rendered":"El producto de funciones no negativas es no negativo"},"content":{"rendered":"

Demostrar con Lean4 que si \(f\) y \(g\) son funciones no negativas de \(\u211d\) en \(\u211d\), entonces su producto es no negativo.<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\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>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\nSe usar\u00e1 el siguiente lema
\n\[ \{0 \u2264 a, 0 \u2264 b\} \vdash 0 \u2264 ab \tag{L1} \]<\/p>\n
Hay que demostrar que
\n\[ (\u2200 x \u2208 \u211d) [0 \u2264 f(x)g(x)] \tag{1} \]
\nPara ello, sea \(x \u2208 R\). Puesto que \(f\) es no negatica, se tiene que
\n\[ 0 \u2264 f(x) \tag{2} \]
\ny, puesto que \(g\) es no negativa, se tiene que
\n\[ 0 \u2264 g(x) \tag{3} \]
\nDe (2) y (3), por L1, se tiene que
\n\[ 0 \u2264 f(x)g(x) \]
\nque es lo que hab\u00eda que demostrar.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\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
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n