Compfiles/Imo1984P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1984, Problem 1

Let $x$, $y$, $z$ be nonnegative real numbers with $x + y + z = 1$. Show that $0 \leq xy+yz+zx-2xyz \leq \frac{7}{27}$

Imports (2)
Imported by 1 file
  1. lemma Imo1984P1.geom_mean_le_arith_mean_3 line 28 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, HDiv.hDiv, HAdd.hAdd, Nat

    Proof uses: mul_nonneg, Eq.mpr, id, Eq, congrArg, Eq.symm, Real.rpow_mul, of_eq_true, Eq.trans, True, Inv.inv, congrFun', one_div, inv_mul_cancel₀, Not, False, not_false_eq_true, Real.rpow_one, eq_self, Real.rpow_le_rpow and 64 more

    98 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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

  2. problem Imo1984P1.imo1984_p1 line 48 source

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

    Statement uses: Real, And, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, HSub.hSub, HMul.hMul, Nat, HDiv.hDiv

    Proof uses: Eq.mpr, id, congrArg, Trans.trans, of_eq_true, Eq.trans, True, congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 144 more

    139 instances, coercions and auxiliary constants left out.

    Tactic trace: 76 steps

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