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.
