Compfiles/Imo2020P2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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.

Imports (2)
Imported by 1 file
  1. problem imo2020_p2 line 29 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, Eq, HAdd.hAdd, HMul.hMul, Nat, HPow.hPow

    Proof uses: Real.geom_mean_le_arith_mean4_weighted, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 102 more

    130 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.