{"id":1942,"date":"2024-01-18T06:00:24","date_gmt":"2024-01-18T04:00:24","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1942"},"modified":"2024-01-17T13:53:22","modified_gmt":"2024-01-17T11:53:22","slug":"18-ene-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/18-ene-24\/","title":{"rendered":"Si (\u2203 x, y \u2208 \u211d)[z = x\u00b2 + y\u00b2 \u2228 z = x\u00b2 + y\u00b2 + 1], entonces z \u2265 0"},"content":{"rendered":"\n

Demostrar con Lean4 que si \\((\u2203 x, y \u2208 \u211d)[z = x\u00b2 + y\u00b2 \u2228 z = x\u00b2 + y\u00b2 + 1]\\), entonces \\(z \u2265 0\\).<\/p>\n

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

\r\nimport Mathlib.Data.Real.Basic\r\nimport Mathlib.Tactic\r\nvariable {z : \u211d}\r\n\r\nexample\r\n  (h : \u2203 x y, z = x^2 + y^2 \u2228 z = x^2 + y^2 + 1)\r\n  : z \u2265 0 :=\r\nby sorry\r\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/h2>\n
Usaremos los siguientes lemas
\n\\begin{align}
\n   &(\u2200 x \u2208 \u211d)[x\u00b2 \u2265 0]                                              \\tag{L1} \\\\
\n   &(\u2200 x, y \u2208 \u211d)[x \u2265 0 \u2192 y \u2265 0 \u2192 x + y \u2265 0]                        \\tag{L2} \\\\
\n   &1 \u2265 0                                                          \\tag{L3}
\n\\end{align}<\/p>\n
Sean \\(a\\) y \\(b\\) tales que
\n\\[ z = a\u00b2 + b\u00b2 \u2228 z = a\u00b2 + b\u00b2 + 1 \\]
\nEntonces, por L1, se tiene que
\n\\begin{align}
\n   &a\u00b2 \u2265 0                                                         \\tag{1} \\\\
\n   &b\u00b2 \u2265 0                                                         \\tag{2}
\n\\end{align}<\/p>\n
En el primer caso, \\(z = a\u00b2 + b\u00b2\\) y se tiene que \\(z \u2265 0\\) por el lema L2 aplicado a (1) y (2).<\/p>\n
En el segundo caso, \\(z = a\u00b2 + b\u00b2 + 1\\) y se tiene que \\(z \u2265 0\\) por el lema L2 aplicado a (1), (2) y L3.<\/p>\n
Demostraciones con Lean4<\/h2>\n
\r\nimport Mathlib.Data.Real.Basic\r\nimport Mathlib.Tactic\r\nvariable {z : \u211d}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : \u2203 x y, z = x^2 + y^2 \u2228 z = x^2 + y^2 + 1)\r\n  : z \u2265 0 :=\r\nby\r\n  rcases h with \u27e8a, b, h1\u27e9\r\n  -- a b : \u211d\r\n  -- h1 : z = a ^ 2 + b ^ 2 \u2228 z = a ^ 2 + b ^ 2 + 1\r\n  have h2 : a ^ 2 \u2265 0 := pow_two_nonneg a\r\n  have h3 : b ^ 2 \u2265 0 := pow_two_nonneg b\r\n  have h4 : a ^ 2 + b ^ 2 \u2265 0 := add_nonneg h2 h3\r\n  rcases h1 with h5 | h6\r\n  . -- h5 : z = a ^ 2 + b ^ 2\r\n    show z \u2265 0\r\n    calc z = a ^ 2 + b ^ 2 := h5\r\n         _ \u2265 0             := add_nonneg h2 h3\r\n  . -- h6 : z = a ^ 2 + b ^ 2 + 1\r\n    show z \u2265 0\r\n    calc z = (a ^ 2 + b ^ 2) + 1 := h6\r\n         _ \u2265 0                   := add_nonneg h4 zero_le_one\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : \u2203 x y, z = x^2 + y^2 \u2228 z = x^2 + y^2 + 1)\r\n  : z \u2265 0 :=\r\nby\r\n  rcases h with \u27e8a, b, h1 | h2\u27e9\r\n  . -- h1 : z = a ^ 2 + b ^ 2\r\n    have h1a : a ^ 2 \u2265 0 := pow_two_nonneg a\r\n    have h1b : b ^ 2 \u2265 0 := pow_two_nonneg b\r\n    show z \u2265 0\r\n    calc z = a ^ 2 + b ^ 2 := h1\r\n         _ \u2265 0             := add_nonneg h1a h1b\r\n  . -- h2 : z = a ^ 2 + b ^ 2 + 1\r\n    have h2a : a ^ 2 \u2265 0         := pow_two_nonneg a\r\n    have h2b : b ^ 2 \u2265 0         := pow_two_nonneg b\r\n    have h2c : a ^ 2 + b ^ 2 \u2265 0 := add_nonneg h2a h2b\r\n    show z \u2265 0\r\n    calc z = (a ^ 2 + b ^ 2) + 1 := h2\r\n         _ \u2265 0                   := add_nonneg h2c zero_le_one\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : \u2203 x y, z = x^2 + y^2 \u2228 z = x^2 + y^2 + 1)\r\n  : z \u2265 0 :=\r\nby\r\n  rcases h with \u27e8a, b, h1 | h2\u27e9\r\n  . -- h1 : z = a ^ 2 + b ^ 2\r\n    rw [h1]\r\n    -- \u22a2 a ^ 2 + b ^ 2 \u2265 0\r\n    apply add_nonneg\r\n    . -- \u22a2 0 \u2264 a ^ 2\r\n      apply pow_two_nonneg\r\n    . -- \u22a2 0 \u2264 b ^ 2\r\n      apply pow_two_nonneg\r\n  . -- h2 : z = a ^ 2 + b ^ 2 + 1\r\n    rw [h2]\r\n    -- \u22a2 a ^ 2 + b ^ 2 + 1 \u2265 0\r\n    apply add_nonneg\r\n    . -- \u22a2 0 \u2264 a ^ 2 + b ^ 2\r\n      apply add_nonneg\r\n      . -- \u22a2 0 \u2264 a ^ 2\r\n        apply pow_two_nonneg\r\n      . -- \u22a2 0 \u2264 b ^ 2\r\n        apply pow_two_nonneg\r\n    . -- \u22a2 0 \u2264 1\r\n      exact zero_le_one\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : \u2203 x y, z = x^2 + y^2 \u2228 z = x^2 + y^2 + 1)\r\n  : z \u2265 0 :=\r\nby\r\n  rcases h with \u27e8a, b, rfl | rfl\u27e9\r\n  . -- \u22a2 a ^ 2 + b ^ 2 \u2265 0\r\n    apply add_nonneg\r\n    . -- \u22a2 0 \u2264 a ^ 2\r\n      apply pow_two_nonneg\r\n    . -- \u22a2 0 \u2264 b ^ 2\r\n      apply pow_two_nonneg\r\n  . -- \u22a2 a ^ 2 + b ^ 2 + 1 \u2265 0\r\n    apply add_nonneg\r\n    . -- \u22a2 0 \u2264 a ^ 2 + b ^ 2\r\n      apply add_nonneg\r\n      . -- \u22a2 0 \u2264 a ^ 2\r\n        apply pow_two_nonneg\r\n      . -- \u22a2 0 \u2264 b ^ 2\r\n        apply pow_two_nonneg\r\n    . -- \u22a2 0 \u2264 1\r\n      exact zero_le_one\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : \u2203 x y, z = x^2 + y^2 \u2228 z = x^2 + y^2 + 1)\r\n  : z \u2265 0 :=\r\nby\r\n  rcases h with \u27e8a, b, rfl | rfl\u27e9\r\n  . -- \u22a2 a ^ 2 + b ^ 2 \u2265 0\r\n    nlinarith\r\n  . -- \u22a2 a ^ 2 + b ^ 2 + 1 \u2265 0\r\n    nlinarith\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : \u2203 x y, z = x^2 + y^2 \u2228 z = x^2 + y^2 + 1)\r\n  : z \u2265 0 :=\r\nby rcases h with \u27e8a, b, rfl | rfl\u27e9 <;> nlinarith\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- variable (x y : \u211d)\r\n-- #check (add_nonneg : 0 \u2264 x \u2192 0 \u2264 y \u2192 0 \u2264 x + y)\r\n-- #check (pow_two_nonneg x : 0 \u2264 x ^ 2)\r\n-- #check (zero_le_one : 0 \u2264 1)\r\n<\/pre>\n
Demostraciones interactivas<\/h2>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/h2>\n