A. City Zhautykov 2017 Problem 2

Real numbers $a, b, x, y$ are such that $(ab)^3 + (xy)^3 \ge (ax)^3 + (by)^3$. Show that $ab + xy \ge ax + by$.

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.29.0.

import Mathlib.Data.Real.Basic

theorem solution (a b x y : ℝ) (h : (a * b) ^ 3 + (x * y) ^ 3 ≥ (a * x) ^ 3 + (b * y) ^ 3) : 
    a * b + x * y ≥ a * x + b * y := sorry

Submit Solution

Login to submit a solution.

Recent Submissions