La semana en Calculemus (2 de septiembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En ℝ, si a ≤ b y c < d, entonces a + eᶜ + f ≤ b + eᵈ + f
- 2. En ℝ, si d ≤ f, entonces c + e^(a + d) ≤ c + e^(a + f)
- 3. En ℝ, si a ≤ b, entonces log(1+e^a) ≤ log(1+e^b)
- 4. En ℝ, si a ≤ b entonces c – e^b ≤ c – e^a
- 5. En ℝ, 2ab ≤ a² + b²
A continuación se muestran las soluciones.
1. En ℝ, si a ≤ b y c < d, entonces a + eᶜ + f ≤ b + eᵈ + f
Demostrar con Lean4 que \(a\), \(b\), \(c\), \(d\) y \(f\) son números reales tales que \(a \leq b\) y \(c < d\), entonces
\[a + e^c + f \leq b + e^d + f\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b c d f : ℝ) example (h1 : a ≤ b) (h2 : c < d) : a + exp c + f < b + exp d + f := by sorry |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
Aplicando a la hipótesis 3 (\(c < d\)) la monotonía de la exponencial, se tiene
\[e^c < e^d\]
que, junto a la hipótesis 1 (\(a \leq b\)) y la monotonía de la suma da
\[a + e^c < b + e^d\]
y, de nuevo por la monotonía de la suma, se tiene
\[a + e^c + f < b + e^d + f\]
2ª demostración en LN
Tenemos que demostrar que
\[(a + e^c) + f < (b + e^d) + f\]
que, por la monotonía de la suma, se reduce a las siguientes dos desigualdades:
\begin{align}
&a + e^c < b + e^d \tag{1} \\
&f \leq f \tag{2}
\end{align}
La (1), de nuevo por la monotonía de la suma, se reduce a las siguientes dos:
\begin{align}
&a \leq b \tag{1.1} \\
&e^c < e^d \tag{1.2}
\end{align}
<
div>La (1.1) se tiene por la hipótesis 1, la (1.2) se tiene aplicando la monotonía de la exponencial a la hipótesis 2 y la (2) se tiene por la propiedad reflexiva.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b c d f : ℝ) -- 1ª demostración example (h1 : a ≤ b) (h2 : c < d) : a + exp c + f < b + exp d + f := by have h3 : exp c < exp d := exp_lt_exp.mpr h2 have h4 : a + exp c < b + exp d := add_lt_add_of_le_of_lt h1 h3 show a + exp c + f < b + exp d + f exact add_lt_add_right h4 f -- 2ª demostración example (h1 : a ≤ b) (h2 : c < d) : a + exp c + f < b + exp d + f := by apply add_lt_add_of_lt_of_le { apply add_lt_add_of_le_of_lt { exact h1 } { apply exp_lt_exp.mpr exact h2 } } { apply le_refl } -- 3ª demostración example (h1 : a ≤ b) (h2 : c < d) : a + exp c + f < b + exp d + f := by apply add_lt_add_of_lt_of_le . apply add_lt_add_of_le_of_lt h1 apply exp_lt_exp.mpr h2 rfl |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 15.
2. En ℝ, si d ≤ f, entonces c + e^(a + d) ≤ c + e^(a + f)
Demostrar con Lean4 que si \(a\), \(c\), \(d\) y \(f\) son números reales tales que \(d ≤ f\), entonces
\[c + e^{a + d} \leq c + e^{a + f}\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a c d f : ℝ) example (h : d ≤ f) : c + exp (a + d) ≤ c + exp (a + f) := by sorry |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
De la hipótesis, por la monotonia de la suma, se tiene
\[a + d \leq a + f\]
que, por la monotonía de la exponencial, da
\[e^{a + d} \leq e^{a + f}\]
y, por la monotonía de la suma, se tiene
\[c + e^{a + d} \leq c + e^{a + f}\]
2ª demostración en LN
Tenemos que demostrar que
\[c + e^{a + d} \leq c + e^{a + f}\]
Por la monotonía de la suma, se reduce a
\[e^{a + d} \leq e^{a + f}\]
que, por la monotonía de la exponencial, se reduce a
\[a + d \leq a + f\]
que, por la monotonía de la suma, se reduce a
\[d \leq f\]
que es la hipótesis.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a c d f : ℝ) -- 1ª demostración example (h : d ≤ f) : c + exp (a + d) ≤ c + exp (a + f) := by have h1 : a + d ≤ a + f := add_le_add_left h a have h2 : exp (a + d) ≤ exp (a + f) := exp_le_exp.mpr h1 show c + exp (a + d) ≤ c + exp (a + f) exact add_le_add_left h2 c -- 2ª demostración example (h : d ≤ f) : c + exp (a + d) ≤ c + exp (a + f) := by apply add_le_add_left apply exp_le_exp.mpr apply add_le_add_left exact h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 15.
3. En ℝ, si a ≤ b, entonces log(1+e^a) ≤ log(1+e^b)
Demostrar con Lean4 que si \(a\) y \(b\) son números reales tales que \(a \leq b\), entonces
\[\log(1+e^a) \leq \log(1+e^b)\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b : ℝ) example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by sorry |
Demostración en lenguaje natural
Por la monotonía del logaritmo, basta demostrar que
\begin{align}
&0 < 1 + e^a \tag{1} \\
&1 + e^a \leq 1 + e^b \tag{2}
\end{align}
La (1), por la suma de positivos, se reduce a
\begin{align}
&0 < 1 \tag{1.1} \\
&0 < e^a \tag{1.2}
\end{align}
La (1.1) es una propiedad de los números naturales y la (1.2) de la
función exponencial.
<
div>La (2), por la monotonía de la suma, se reduce a
\[e^a \leq e^b\]
que, por la monotonía de la exponencial, se reduce a
\[a \leq b\]
que es la hipótesis.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b : ℝ) -- 1ª demostración example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by have h1 : (0 : ℝ) < 1 := zero_lt_one have h2 : 0 < exp a := exp_pos a have h3 : 0 < 1 + exp a := add_pos h1 h2 have h4 : exp a ≤ exp b := exp_le_exp.mpr h have h5 : 1 + exp a ≤ 1 + exp b := add_le_add_left h4 1 show log (1 + exp a) ≤ log (1 + exp b) exact log_le_log' h3 h5 -- 2ª demostraciṕn example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by apply log_le_log' { apply add_pos { exact zero_lt_one } { exact exp_pos a }} { apply add_le_add_left exact exp_le_exp.mpr h } |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 15.
4. En ℝ, si a ≤ b entonces c – e^b ≤ c – e^a
Sean \(a\), \(b\) y \(c\) números reales. Demostrar con Lean4 que si \(a \leq b\), entonces
\[c – e^b \leq c – e^a\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b c : ℝ) example (h : a ≤ b) : c - exp b ≤ c - exp a := by sorry |
Demostración en lenguaje natural
Aplicando la monotonía de la exponencial a la hipótesis, se tiene
\[e^a \leq e^b\]
y, restando de \(c\), se invierte la desigualdad
\[c – e^b ≤ c – e^a\]
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b c : ℝ) -- 1ª demostración example (h : a ≤ b) : c - exp b ≤ c - exp a := by have h1 : exp a ≤ exp b := exp_le_exp.mpr h show c - exp b ≤ c - exp a exact sub_le_sub_left h1 c -- 2ª demostración example (h : a ≤ b) : c - exp b ≤ c - exp a := by apply sub_le_sub_left _ c apply exp_le_exp.mpr h -- 3ª demostración example (h : a ≤ b) : c - exp b ≤ c - exp a := sub_le_sub_left (exp_le_exp.mpr h) c -- 4ª demostración example (h : a ≤ b) : c - exp b ≤ c - exp a := by linarith [exp_le_exp.mpr h] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 16.
5. En ℝ, 2ab ≤ a² + b²
Sean \(a\) y \(b\) números reales. Demostrar con Lean4 que
\[2ab ≤ a^2 + b^2\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : 2*a*b ≤ a^2 + b^2 := by sorry |
Demostración en lenguaje natural
Puesto que los cuadrados son positivos, se tiene
\[(a – b)^2 ≥ 0\]
Desarrollando el cuadrado, se obtiene
\[a^2 – 2ab + b^2 ≥ 0\]
Sumando \(2ab\) a ambos lados, queda
\[a^2 + b^2 ≥ 2ab\]
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- 1ª demostración example : 2*a*b ≤ a^2 + b^2 := by have h1 : 0 ≤ (a - b)^2 := sq_nonneg (a - b) have h2 : 0 ≤ a^2 - 2*a*b + b^2 := by linarith only [h1] show 2*a*b ≤ a^2 + b^2 linarith -- 2ª demostración example : 2*a*b ≤ a^2 + b^2 := by have h : 0 ≤ a^2 - 2*a*b + b^2 { calc a^2 - 2*a*b + b^2 = (a - b)^2 := (sub_sq a b).symm _ ≥ 0 := sq_nonneg (a - b) } calc 2*a*b = 2*a*b + 0 := (add_zero (2*a*b)).symm _ ≤ 2*a*b + (a^2 - 2*a*b + b^2) := add_le_add (le_refl _) h _ = a^2 + b^2 := by ring -- 3ª demostración example : 2*a*b ≤ a^2 + b^2 := by have h : 0 ≤ a^2 - 2*a*b + b^2 { calc a^2 - 2*a*b + b^2 = (a - b)^2 := (sub_sq a b).symm _ ≥ 0 := sq_nonneg (a - b) } linarith only [h] -- 4ª demostración example : 2*a*b ≤ a^2 + b^2 := -- by apply? two_mul_le_add_sq a b |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 16.