import Mathlib.Analysis.MeanInequalities /-! # International Mathematical Olympiad 2020, Problem 2 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`. -/ open Real 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 := sorry

This problem has a complete solution written by Joseph Myers and Yury Kudryashov.

The solution was imported from mathlib4/Archive/Imo/Imo2020Q2.lean.