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 |