28 septiembre 2022 – Calculemus

Si a, b ∈ ℝ, entonces |ab| ≤ (a² + b²)/2

PorJosé A. Alonso 28 septiembre 202211 septiembre 2022

Demostrar que si a, b ∈ ℝ, entonces |ab| ≤ (a² + b²)/2

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
import tactic

variables a b : ℝ

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
sorry

import data.real.basic

import tactic

variables a b : ℝ

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=

sorry