La semana en Calculemus (9 de septiembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En ℝ, |ab| ≤ (a²+b²)/2
- 2. En ℝ, min(a,b) = min(b,a)
- 3. En ℝ, max(a,b) = max(b,a)
- 4. En ℝ, min(min(a,b),c) = min(a,min(b,c))
- 5. En ℝ, min(a,b)+c = min(a+c,b+c)
A continuación se muestran las soluciones.
1. En ℝ, |ab| ≤ (a²+b²)/2
Sean \(a\) y \(b\) números reales. Demostrar con Lean4 que
\[|ab| \leq \frac{a^2 + b^2}{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 : |a * b| \\leq (a ^ 2 + b ^ 2) / 2 := by sorry |
Demostración en lenguaje natural
Para demostrar
\[|ab| \leq \frac{a^2 + b^2}{2}\]
basta demostrar estas dos desigualdades
\begin{align}
ab &\leq \frac{a^2 + b^2}{2} \tag{1} \\
-(ab) &\leq \frac{a^2 + b^2}{2} \tag{2}
\end{align}
Para demostrar (1) basta demostrar que
\[2ab \leq a^2 + b^2\]
que se prueba como sigue. En primer lugar, como los cuadrados son no negativos, se tiene
\[(a – b)^2 \geq 0\]
Desarrollando el cuandrado,
\[a^2 – 2ab + b^2 \geq 0\]
Sumando \(2ab\),
\[a^2 + b^2 \geq 2ab\]
Para demostrar (2) basta demostrar que
\[-2ab \leq a^2 + b^2\]
que se prueba como sigue. En primer lugar, como los cuadrados son no
negativos, se tiene
\[(a + b)^2 \geq 0\]
Desarrollando el cuandrado,
\[a^2 + 2ab + b^2 \geq 0\]
Restando \(2ab\),
\[a^2 + b^2 \geq -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 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- Lemas auxiliares -- ================ lemma aux1 : a * b * 2 ≤ 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 := by ring _ ≥ 0 := pow_two_nonneg (a - b) linarith only [h] lemma aux2 : -(a * b) * 2 ≤ 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 := by ring _ ≥ 0 := pow_two_nonneg (a + b) linarith only [h] -- 1ª demostración -- =============== example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by have h : (0 : ℝ) < 2 := by norm_num apply abs_le'.mpr constructor { have h1 : a * b * 2 ≤ a ^ 2 + b ^ 2 := aux1 a b show a * b ≤ (a ^ 2 + b ^ 2) / 2 exact (le_div_iff h).mpr h1 } { have h2 : -(a * b) * 2 ≤ a ^ 2 + b ^ 2 := aux2 a b show -(a * b) ≤ (a ^ 2 + b ^ 2) / 2 exact (le_div_iff h).mpr h2 } -- 2ª demostración -- =============== example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by have h : (0 : ℝ) < 2 := by norm_num apply abs_le'.mpr constructor { exact (le_div_iff h).mpr (aux1 a b) } { exact (le_div_iff h).mpr (aux2 a b) } -- 3ª demostración -- =============== example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by have h : (0 : ℝ) < 2 := by norm_num apply abs_le'.mpr constructor { rw [le_div_iff h] apply aux1 } { rw [le_div_iff h] apply aux2 } |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 16.
2. En ℝ, min(a,b) = min(b,a)
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces \(\min(a, b) = \min(b, a)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : min a b = min b a := by sorry |
Demostración en lenguaje natural
Es consecuencia de la siguiente propiedad
\[\min(a, b) \leq \min(b, a) \tag{1}\]
En efecto, intercambiando las variables en (1) se obtiene
\[\min(b, a) \leq \min(a, b) \tag{2}\]
Finalmente de (1) y (2) se obtiene
\[\min(b, a) = \min(a, b)\]
Para demostrar (1), se observa que
\begin{align}
\min(a, b) &\leq b \\
\min(a, b) &\leq a
\end{align}
y, por tanto,
\[\min(a, b) \leq \min(b, 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 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- Lema auxiliar -- ============= -- 1ª demostración del lema auxiliar -- ================================= example : min a b ≤ min b a := by have h1 : min a b ≤ b := min_le_right a b have h2 : min a b ≤ a := min_le_left a b show min a b ≤ min b a exact le_min h1 h2 -- 2ª demostración del lema auxiliar -- ================================= example : min a b ≤ min b a := by apply le_min { apply min_le_right } { apply min_le_left } -- 3ª demostración del lema auxiliar -- ================================= lemma aux : min a b ≤ min b a := by exact le_min (min_le_right a b) (min_le_left a b) -- 1ª demostración -- =============== example : min a b = min b a := by apply le_antisymm { exact aux a b} { exact aux b a} -- 2ª demostración -- =============== example : min a b = min b a := le_antisymm (aux a b) (aux b a) -- 3ª demostración -- =============== example : min a b = min b a := min_comm 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. 17.
3. En ℝ, max(a,b) = max(b,a)
Demostrar con Lean4 que si \(a\) y \(b\) son números reales, entonces \(\max(a, b) = \max(b, a)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : max a b = max b a := by sorry |
Demostración en lenguaje natural
Es consecuencia de la siguiente propiedad
\[\max(a, b) \leq \max(b, a) \tag{1}\]
En efecto, intercambiando las variables en (1) se obtiene
\[\max(b, a) \leq \max(a, b) \tag{2}\]
Finalmente de (1) y (2) se obtiene
\[\max(b, a) = \max(a, b)\]
Para demostrar (1), se observa que
\begin{align}
a &\leq \max(b, a) \\
b &\leq \max(b, a)
\end{align}
y, por tanto,
\[\max(a, b) \leq \max(b, 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 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- Lema auxiliar -- ============= -- 1ª demostración del lema auxiliar -- ================================= example : max a b ≤ max b a := by have h1 : a ≤ max b a := le_max_right b a have h2 : b ≤ max b a := le_max_left b a show max a b ≤ max b a exact max_le h1 h2 -- 2ª demostración del lema auxiliar -- ================================= example : max a b ≤ max b a := by apply max_le { apply le_max_right } { apply le_max_left } -- 3ª demostración del lema auxiliar -- ================================= lemma aux : max a b ≤ max b a := by exact max_le (le_max_right b a) (le_max_left b a) -- 1ª demostración -- =============== example : max a b = max b a := by apply le_antisymm { exact aux a b} { exact aux b a} -- 2ª demostración -- =============== example : max a b = max b a := le_antisymm (aux a b) (aux b a) -- 3ª demostración -- =============== example : max a b = max b a := max_comm 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. 17.
4. En ℝ, min(min(a,b),c) = min(a,min(b,c))
Demostrar con Lean4 que \(a\), \(b\) y \(c\) números reales, entonces \(\min(\min(a, b), c) = \min(a, \min(b, c))\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a b c : ℝ} example : min (min a b) c = min a (min b c) := by sorry |
Demostración en lenguaje natural
Por la propiedad antisimétrica, la igualdad es consecuencia de las siguientes desigualdades
\begin{align}
\min(\min(a, b), c) &\leq \min(a, \min(b, c)) \tag{1} \\
\min(a, \min(b, c)) &\leq \min(\min(a, b), c) \tag{2}
\end{align}
La (1) es consecuencia de las siguientes desigualdades
\begin{align}
\min(\min(a, b), c) &\leq a \tag{1a} \\
\min(\min(a, b), c) &\leq b \tag{1b} \\
\min(\min(a, b), c) &\leq c \tag{1c}
\end{align}
En efecto, de (1b) y (1c) se obtiene
\[ \min(\min(a, b), c) \leq \min(b,c) \]
que, junto con (1a) da (1).
La (2) es consecuencia de las siguientes desigualdades
\begin{align}
\min(a, \min(b, c)) &\leq a \tag{2a} \\
\min(a, \min(b, c)) &\leq b \tag{2b} \\
\min(a, \min(b, c)) &\leq c \tag{2c}
\end{align}
En efecto, de (2a) y (2b) se obtiene
\[ \min(a, \min(b, c)) \leq \min(a, b) \]
que, junto con (2c) da (2).
La demostración de (1a) es
\[ \min(\min(a, b), c) \leq \min(a, b) \leq a \]
La demostración de (1b) es
\[ \min(\min(a, b), c) \leq \min(a, b) \leq b \]
La demostración de (2b) es
\[ \min(a, \min(b, c)) \leq \min(b, c) \leq b \]
La demostración de (2c) es
\[ \min(a, \min(b, c)) \leq \min(b, c) \leq c \]
La (1c) y (2a) son inmediatas.
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 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 |
import Mathlib.Data.Real.Basic variable {a b c : ℝ} -- Lemas auxiliares -- ================ lemma aux1a : min (min a b) c ≤ a := calc min (min a b) c ≤ min a b := by exact min_le_left (min a b) c _ ≤ a := min_le_left a b lemma aux1b : min (min a b) c ≤ b := calc min (min a b) c ≤ min a b := by exact min_le_left (min a b) c _ ≤ b := min_le_right a b lemma aux1c : min (min a b) c ≤ c := by exact min_le_right (min a b) c -- 1ª demostración del lema aux1 lemma aux1 : min (min a b) c ≤ min a (min b c) := by apply le_min { show min (min a b) c ≤ a exact aux1a } { show min (min a b) c ≤ min b c apply le_min { show min (min a b) c ≤ b exact aux1b } { show min (min a b) c ≤ c exact aux1c }} -- 2ª demostración del lema aux1 lemma aux1' : min (min a b) c ≤ min a (min b c) := le_min aux1a (le_min aux1b aux1c) lemma aux2a : min a (min b c) ≤ a := by exact min_le_left a (min b c) lemma aux2b : min a (min b c) ≤ b := calc min a (min b c) ≤ min b c := by exact min_le_right a (min b c) _ ≤ b := min_le_left b c lemma aux2c : min a (min b c) ≤ c := calc min a (min b c) ≤ min b c := by exact min_le_right a (min b c) _ ≤ c := min_le_right b c -- 1ª demostración del lema aux2 lemma aux2 : min a (min b c) ≤ min (min a b) c := by apply le_min { show min a (min b c) ≤ min a b apply le_min { show min a (min b c) ≤ a exact aux2a } { show min a (min b c) ≤ b exact aux2b }} { show min a (min b c) ≤ c exact aux2c } -- 2ª demostración del lema aux2 lemma aux2' : min a (min b c) ≤ min (min a b) c := le_min (le_min aux2a aux2b) aux2c -- 1ª demostración -- =============== example : min (min a b) c = min a (min b c) := by apply le_antisymm { show min (min a b) c ≤ min a (min b c) exact aux1 } { show min a (min b c) ≤ min (min a b) c exact aux2 } -- 2ª demostración -- =============== example : min (min a b) c = min a (min b c) := by apply le_antisymm { exact aux1 } { exact aux2 } -- 3ª demostración -- =============== example : min (min a b) c = min a (min b c) := le_antisymm aux1 aux2 -- 4ª demostración -- =============== example : min (min a b) c = min a (min b c) := min_assoc a b c |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 18.
5. En ℝ, min(a,b)+c = min(a+c,b+c)
Demostrar con Lean4 que si \(a\), \(b\) y \(c\) números reales, entonces
\[\min(a,b)+c = \min(a+c,b+c)\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a b c : ℝ} example : min a b + c = min (a + c) (b + c) := by sorry |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
Aplicando la propiedad antisimétrica a las siguientes desigualdades
\begin{align}
\min(a, b) + c \leq \min(a + c, b + c) \tag{1} \\
\min(a + c, b + c) \leq \min(a, b) + c \tag{2}
\end{align}
Para demostrar (1) basta demostrar que se verifican las siguientes desigualdades
\begin{align}
\min(a, b) + c &\leq a + c \tag{1a} \\
\min(a, b) + c &\leq b + c \tag{1b}
\end{align}
que se tienen porque se verifican las siguientes desigualdades
\begin{align}
\min(a, b) &\leq a \\
\min(a, b) &\leq b
\end{align}
Para demostrar (2) basta demostrar que se verifica
\[ \min(a + c, b + c) – c \leq \min(a, b) \]
que se demuestra usando (1); en efecto,
\begin{align}
\min(a + c, b + c) – c &\leq \min(a + c – c, b + c – c) &&\text{[por (1)]}\\
&= \min(a, b)
\end{align}
2ª demostración en LN
Por casos según \(a \leq b\).
1º caso: Supongamos que \(a \leq b\). Entonces,
\begin{align}
\min(a, b) + c &= a + c \\
&= \min(a + c, b + c)
\end{align}
2º caso: Supongamos que \(a \nleq b\). Entonces,
\begin{align}
\min(a, b) + c &= b + c \\
&= \min(a + c, b + c)
\end{align}
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 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 |
import Mathlib.Data.Real.Basic variable {a b c : ℝ} -- En las demostraciones se usarán los siguientes lemas auxiliares -- aux1 : min a b + c ≤ min (a + c) (b + c) -- aux2 : min (a + c) (b + c) ≤ min a b + c -- cuyas demostraciones se exponen a continuación. -- 1ª demostración de aux1 lemma aux1 : min a b + c ≤ min (a + c) (b + c) := by have h1 : min a b ≤ a := min_le_left a b have h2 : min a b + c ≤ a + c := add_le_add_right h1 c have h3 : min a b ≤ b := min_le_right a b have h4 : min a b + c ≤ b + c := add_le_add_right h3 c show min a b + c ≤ min (a + c) (b + c) exact le_min h2 h4 -- 2ª demostración de aux1 example : min a b + c ≤ min (a + c) (b + c) := by apply le_min { apply add_le_add_right exact min_le_left a b } { apply add_le_add_right exact min_le_right a b } -- 3ª demostración de aux1 example : min a b + c ≤ min (a + c) (b + c) := le_min (add_le_add_right (min_le_left a b) c) (add_le_add_right (min_le_right a b) c) -- 1ª demostración de aux2 lemma aux2 : min (a + c) (b + c) ≤ min a b + c := by have h1 : min (a + c) (b + c) + -c ≤ min a b { calc min (a + c) (b + c) + -c ≤ min (a + c + -c) (b + c + -c) := aux1 _ = min a b := by ring_nf } show min (a + c) (b + c) ≤ min a b + c exact add_neg_le_iff_le_add.mp h1 -- 1ª demostración del ejercicio example : min a b + c = min (a + c) (b + c) := by have h1 : min a b + c ≤ min (a + c) (b + c) := aux1 have h2 : min (a + c) (b + c) ≤ min a b + c := aux2 show min a b + c = min (a + c) (b + c) exact le_antisymm h1 h2 -- 2ª demostración del ejercicio example : min a b + c = min (a + c) (b + c) := by apply le_antisymm { show min a b + c ≤ min (a + c) (b + c) exact aux1 } { show min (a + c) (b + c) ≤ min a b + c exact aux2 } -- 3ª demostración del ejercicio example : min a b + c = min (a + c) (b + c) := by apply le_antisymm { exact aux1 } { exact aux2 } -- 4ª demostración del ejercicio example : min a b + c = min (a + c) (b + c) := le_antisymm aux1 aux2 -- 5ª demostración del ejercicio example : min a b + c = min (a + c) (b + c) := by by_cases h : a ≤ b { have h1 : a + c ≤ b + c := add_le_add_right h c calc min a b + c = a + c := by simp [min_eq_left h] _ = min (a + c) (b + c) := by simp [min_eq_left h1]} { have h2: b ≤ a := le_of_not_le h have h3 : b + c ≤ a + c := add_le_add_right h2 c calc min a b + c = b + c := by simp [min_eq_right h2] _ = min (a + c) (b + c) := by simp [min_eq_right h3]} -- 6ª demostración del ejercicio example : min a b + c = min (a + c) (b + c) := (min_add_add_right a b c).symm |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 18.