Sean \\(a\\) y \\(b\\) n\u00fameros reales. Demostrar con Lean4 que
\n\\[2ab \u2264 a^2 + b^2\\]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable (a b : \u211d)\r\n\r\nexample : 2*a*b \u2264 a^2 + b^2 :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPuesto que los cuadrados son positivos, se tiene
\n\\[(a – b)^2 \u2265 0\\]
\nDesarrollando el cuadrado, se obtiene
\n\\[a^2 – 2ab + b^2 \u2265 0\\]
\nSumando \\(2ab\\) a ambos lados, queda
\n\\[a^2 + b^2 \u2265 2ab\\]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable (a b : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : 2*a*b \u2264 a^2 + b^2 :=\r\nby\r\n have h1 : 0 \u2264 (a - b)^2 := sq_nonneg (a - b)\r\n have h2 : 0 \u2264 a^2 - 2*a*b + b^2 := by linarith only [h1]\r\n show 2*a*b \u2264 a^2 + b^2\r\n linarith\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : 2*a*b \u2264 a^2 + b^2 :=\r\nby\r\n have h : 0 \u2264 a^2 - 2*a*b + b^2\r\n { calc a^2 - 2*a*b + b^2\r\n = (a - b)^2 := (sub_sq a b).symm\r\n _ \u2265 0 := sq_nonneg (a - b) }\r\n calc 2*a*b\r\n = 2*a*b + 0 := (add_zero (2*a*b)).symm\r\n _ \u2264 2*a*b + (a^2 - 2*a*b + b^2) := add_le_add (le_refl _) h\r\n _ = a^2 + b^2 := by ring\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : 2*a*b \u2264 a^2 + b^2 :=\r\nby\r\n have h : 0 \u2264 a^2 - 2*a*b + b^2\r\n { calc a^2 - 2*a*b + b^2\r\n = (a - b)^2 := (sub_sq a b).symm\r\n _ \u2265 0 := sq_nonneg (a - b) }\r\n linarith only [h]\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : 2*a*b \u2264 a^2 + b^2 :=\r\n-- by apply?\r\ntwo_mul_le_add_sq a b\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n