Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2020P2

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

File author(s): Joseph Myers, Yury Kudryashov

This problem has a complete formalized solution.

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