Si a, b ∈ ℝ, entonces 2ab ≤ a² + b²
Demostrar que si a, b ∈ ℝ, entonces 2ab ≤ a² + b²
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 |
import data.real.basic import tactic variables a b : ℝ example : 2*a*b ≤ a^2 + b^2 := sorry |
Soluciones con Lean
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 data.real.basic import tactic variables a b : ℝ -- 1ª demostración example : 2*a*b ≤ a^2 + b^2 := begin have : 0 ≤ (a - b)^2 := sq_nonneg (a - b), have : 0 ≤ a^2 - 2*a*b + b^2, by linarith, show 2*a*b ≤ a^2 + b^2, by linarith, end -- 2ª demostración example : 2*a*b ≤ a^2 + b^2 := begin have h : 0 ≤ a^2 - 2*a*b + b^2, { calc a^2 - 2*a*b + b^2 = (a - b)^2 : by ring ... ≥ 0 : by apply pow_two_nonneg }, calc 2*a*b = 2*a*b + 0 : by ring ... ≤ 2*a*b + (a^2 - 2*a*b + b^2) : add_le_add (le_refl _) h ... = a^2 + b^2 : by ring end -- 3ª demostración example : 2*a*b ≤ a^2 + b^2 := begin have : 0 ≤ a^2 - 2*a*b + b^2, { calc a^2 - 2*a*b + b^2 = (a - b)^2 : by ring ... ≥ 0 : by apply pow_two_nonneg }, linarith, end -- 4ª demostración example : 2*a*b ≤ a^2 + b^2 := -- by library_search two_mul_le_add_sq a b |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 17.