lean_workbook_plus_50879
ProvedUsing AM-GM:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50879 : ∀ x y : ℝ, 2 * x * y ≤ (2 * x + y) ^ 2 / 2 := by sorry
Source
Using AM-GM:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_50879 : ∀ x y : ℝ, 2 * x * y ≤ (2 * x + y) ^ 2 / 2 := by sorry