Sean \\(a\\) y \\(b\\) n\u00fameros reales. Demostrar con Lean4 que
\n\\[|ab| \\leq \\frac{a^2 + b^2}{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 : |a * b| \\leq (a ^ 2 + b ^ 2) \/ 2 :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPara demostrar
\n\\[|ab| \\leq \\frac{a^2 + b^2}{2}\\]
\nbasta demostrar estas dos desigualdades
\n\\begin{align}
\n ab &\\leq \\frac{a^2 + b^2}{2} \\tag{1} \\\\
\n -(ab) &\\leq \\frac{a^2 + b^2}{2} \\tag{2}
\n\\end{align}<\/p>\n
Para demostrar (1) basta demostrar que
\n\\[2ab \\leq a^2 + b^2\\]
\nque se prueba como sigue. En primer lugar, como los cuadrados son no negativos, se tiene
\n\\[(a – b)^2 \\geq 0\\]
\nDesarrollando el cuandrado,
\n\\[a^2 – 2ab + b^2 \\geq 0\\]
\nSumando \\(2ab\\),
\n\\[a^2 + b^2 \\geq 2ab\\]<\/p>\n
Para demostrar (2) basta demostrar que
\n\\[-2ab \\leq a^2 + b^2\\]
\nque se prueba como sigue. En primer lugar, como los cuadrados son no
\nnegativos, se tiene
\n\\[(a + b)^2 \\geq 0\\]
\nDesarrollando el cuandrado,
\n\\[a^2 + 2ab + b^2 \\geq 0\\]
\nRestando \\(2ab\\),
\n\\[a^2 + b^2 \\geq -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-- Lemas auxiliares\r\n-- ================\r\n\r\nlemma aux1 : a * b * 2 \u2264 a ^ 2 + b ^ 2 := by\r\n have h : 0 \u2264 a ^ 2 - 2 * a * b + b ^ 2\r\n calc\r\n a ^ 2 - 2 * a * b + b ^ 2\r\n = (a - b) ^ 2 := by ring\r\n _ \u2265 0 := pow_two_nonneg (a - b)\r\n linarith only [h]\r\n\r\nlemma aux2 : -(a * b) * 2 \u2264 a ^ 2 + b ^ 2 := by\r\n have h : 0 \u2264 a ^ 2 + 2 * a * b + b ^ 2\r\n calc\r\n a ^ 2 + 2 * a * b + b ^ 2\r\n = (a + b) ^ 2 := by ring\r\n _ \u2265 0 := pow_two_nonneg (a + b)\r\n linarith only [h]\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : |a * b| \u2264 (a ^ 2 + b ^ 2) \/ 2 := by\r\n have h : (0 : \u211d) < 2 := by norm_num\r\n apply abs_le'.mpr\r\n constructor\r\n { have h1 : a * b * 2 \u2264 a ^ 2 + b ^ 2 := aux1 a b\r\n show a * b \u2264 (a ^ 2 + b ^ 2) \/ 2\r\n exact (le_div_iff h).mpr h1 }\r\n { have h2 : -(a * b) * 2 \u2264 a ^ 2 + b ^ 2 := aux2 a b\r\n show -(a * b) \u2264 (a ^ 2 + b ^ 2) \/ 2\r\n exact (le_div_iff h).mpr h2 }\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : |a * b| \u2264 (a ^ 2 + b ^ 2) \/ 2 := by\r\n have h : (0 : \u211d) < 2 := by norm_num\r\n apply abs_le'.mpr\r\n constructor\r\n { exact (le_div_iff h).mpr (aux1 a b) }\r\n { exact (le_div_iff h).mpr (aux2 a b) }\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : |a * b| \u2264 (a ^ 2 + b ^ 2) \/ 2 := by\r\n have h : (0 : \u211d) < 2 := by norm_num\r\n apply abs_le'.mpr\r\n constructor\r\n { rw [le_div_iff h]\r\n apply aux1 }\r\n { rw [le_div_iff h]\r\n apply aux2 }\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