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.
