Demostrar con Lean4 que si \(x\) e \(y\) son sumas de dos cuadrados, entonces \(xy\) tambi\u00e9n lo es<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Tactic\nvariable {\u03b1 : Type _} [CommRing \u03b1]\nvariable {x y : \u03b1}\n\n-- (suma_de_cuadrados x) afirma que x se puede escribir como la suma\n-- de dos cuadrados.\ndef suma_de_cuadrados (x : \u03b1) :=\n \u2203 a b, x = a^2 + b^2\n\nexample\n (hx : suma_de_cuadrados x)\n (hy : suma_de_cuadrados y)\n : suma_de_cuadrados (x * y) :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPuesto que \(x\) e \(y\) se pueden escribir como la suma de dos cuadrados, existen \(a\), \(b\) , \(c\) y \(d\) tales que
\n\begin{align}
\n x &= a\u00b2 + b\u00b2 \\
\n y &= c\u00b2 + d\u00b2
\n\end{align}
\nEntonces,
\n\begin{align}
\n xy &= (a\u00b2 + b\u00b2)(c\u00b2 + d\u00b2) \\
\n &= a\u00b2c\u00b2 + b\u00b2d\u00b2 + a\u00b2d\u00b2 + b\u00b2c\u00b2 \\
\n &= a\u00b2c\u00b2 – 2acbd + b\u00b2d\u00b2 + a\u00b2d\u00b2 + 2adbc + b\u00b2c\u00b2 \\
\n &= (ac – bd)\u00b2 + (ad + bc)\u00b2
\n\end{align}
\nPor tanto, \(xy\) es la suma de dos cuadrados.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Tactic\nvariable {\u03b1 : Type _} [CommRing \u03b1]\nvariable {x y : \u03b1}\n\n-- (suma_de_cuadrados x) afirma que x se puede escribir como la suma\n-- de dos cuadrados.\ndef suma_de_cuadrados (x : \u03b1) :=\n \u2203 a b, x = a^2 + b^2\n\n-- 1\u00aa demostraci\u00f3n\nexample\n (hx : suma_de_cuadrados x)\n (hy : suma_de_cuadrados y)\n : suma_de_cuadrados (x * y) :=\nby\n rcases hx with \u27e8a, b, xeq : x = a^2 + b^2\u27e9\n -- a b : \u03b1\n -- xeq : x = a ^ 2 + b ^ 2\n rcases hy with \u27e8c, d, yeq : y = c^2 + d^2\u27e9\n -- c d : \u03b1\n -- yeq : y = c ^ 2 + d ^ 2\n have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2 :=\n calc x * y\n = (a^2 + b^2) * (c^2 + d^2) :=\n by rw [xeq, yeq]\n _ = a^2*c^2 + b^2*d^2 + a^2*d^2 + b^2*c^2 :=\n by ring\n _ = a^2*c^2 - 2*a*c*b*d + b^2*d^2 + a^2*d^2 + 2*a*d*b*c + b^2*c^2 :=\n by ring\n _ = (a*c - b*d)^2 + (a*d + b*c)^2 :=\n by ring\n have h2 : \u2203 f, x * y = (a*c - b*d)^2 + f^2 :=\n Exists.intro (a*d + b*c) h1\n have h3 : \u2203 e f, x * y = e^2 + f^2 :=\n Exists.intro (a*c - b*d) h2\n show suma_de_cuadrados (x * y)\n exact h3\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (hx : suma_de_cuadrados x)\n (hy : suma_de_cuadrados y)\n : suma_de_cuadrados (x * y) :=\nby\n rcases hx with \u27e8a, b, xeq : x = a^2 + b^2\u27e9\n -- a b : \u03b1\n -- xeq : x = a ^ 2 + b ^ 2\n rcases hy with \u27e8c, d, yeq : y = c^2 + d^2\u27e9\n -- c d : \u03b1\n -- yeq : y = c ^ 2 + d ^ 2\n have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2 :=\n calc x * y\n = (a^2 + b^2) * (c^2 + d^2) := by rw [xeq, yeq]\n _ = (a*c - b*d)^2 + (a*d + b*c)^2 := by ring\n have h2 : \u2203 e f, x * y = e^2 + f^2 :=\n by tauto\n show suma_de_cuadrados (x * y)\n exact h2\n\n-- 3\u00aa demostraci\u00f3n\nexample\n (hx : suma_de_cuadrados x)\n (hy : suma_de_cuadrados y)\n : suma_de_cuadrados (x * y) :=\nby\n rcases hx with \u27e8a, b, xeq\u27e9\n -- a b : \u03b1\n -- xeq : x = a ^ 2 + b ^ 2\n rcases hy with \u27e8c, d, yeq\u27e9\n -- c d : \u03b1\n -- yeq : y = c ^ 2 + d ^ 2\n rw [xeq, yeq]\n -- \u22a2 suma_de_cuadrados ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))\n use a*c - b*d, a*d + b*c\n -- \u22a2 (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2)\n -- = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2\n ring\n\n-- 4\u00aa demostraci\u00f3n\nexample\n (hx : suma_de_cuadrados x)\n (hy : suma_de_cuadrados y)\n : suma_de_cuadrados (x * y) :=\nby\n rcases hx with \u27e8a, b, rfl\u27e9\n -- \u22a2 suma_de_cuadrados ((a ^ 2 + b ^ 2) * y)\n rcases hy with \u27e8c, d, rfl\u27e9\n -- \u22a2 suma_de_cuadrados ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))\n use a*c - b*d, a*d + b*c\n -- \u22a2 (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2)\n -- = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2\n ring\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n