IMO 2020 Q2 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The real numbers a, b, c, d are such that a ≥ b ≥ c ≥ d > 0 and a + b + c + d = 1. Prove that (a + 2b + 3c + 4d) a^a b^b c^c d^d < 1.

A solution is to eliminate the powers using weighted AM-GM and replace 1 by (a+b+c+d)^3, leaving a homogeneous inequality that can be proved in many ways by expanding, rearranging and comparing individual terms. The version here using factors such as a+3b+3c+3d is from the official solutions.

source

theorem imo2020_q2 (a b c d : ℝ) (hd0 : 0 < d) (hdc : d ≤ c) (hcb : c ≤ b) (hba : b ≤ a) (h1 : a + b + c + d = 1) :

(a + 2 * b + 3 * c + 4 * d) * a ^ a * b ^ b * c ^ c * d ^ d < 1