Demostrar con Lean4 que si \\(a\\) y \\(b\\) son n\u00fameros reales tales que \\(a \\leq b\\), entonces
\n\\[\\log(1+e^a) \\leq \\log(1+e^b)\\]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\r\nopen Real\r\nvariable (a b : \u211d)\r\n\r\nexample\r\n (h : a \u2264 b)\r\n : log (1 + exp a) \u2264 log (1 + exp b) :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n\n
Por la monoton\u00eda del logaritmo, basta demostrar que
\n\\begin{align}
\n &0 < 1 + e^a \\tag{1} \\\\\n &1 + e^a \\leq 1 + e^b \\tag{2}\n\\end{align}\n\nLa (1), por la suma de positivos, se reduce a\n\\begin{align}\n &0 < 1 \\tag{1.1} \\\\\n &0 < e^a \\tag{1.2}\n\\end{align}\nLa (1.1) es una propiedad de los n\u00fameros naturales y la (1.2) de la\nfunci\u00f3n exponencial.\n\n\n\n
La (2), por la monoton\u00eda de la suma, se reduce a
\n\\[e^a \\leq e^b\\]
\nque, por la monoton\u00eda de la exponencial, se reduce a
\n\\[a \\leq b\\]
\nque es la hip\u00f3tesis.<\/p>\nDemostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\r\nopen Real\r\nvariable (a b : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (h : a \u2264 b)\r\n : log (1 + exp a) \u2264 log (1 + exp b) :=\r\nby\r\n have h1 : (0 : \u211d) < 1 :=\r\n zero_lt_one\r\n have h2 : 0 < exp a :=\r\n exp_pos a\r\n have h3 : 0 < 1 + exp a :=\r\n add_pos h1 h2\r\n have h4 : exp a \u2264 exp b :=\r\n exp_le_exp.mpr h\r\n have h5 : 1 + exp a \u2264 1 + exp b :=\r\n add_le_add_left h4 1\r\n show log (1 + exp a) \u2264 log (1 + exp b)\r\n exact log_le_log' h3 h5\r\n\r\n-- 2\u00aa demostraci\u1e55n\r\nexample\r\n (h : a \u2264 b)\r\n : log (1 + exp a) \u2264 log (1 + exp b) :=\r\nby\r\n apply log_le_log'\r\n { apply add_pos\r\n { exact zero_lt_one }\r\n { exact exp_pos a }}\r\n { apply add_le_add_left\r\n exact exp_le_exp.mpr h }\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