Compfiles/Usa1974P2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1974, Problem 2

Prove that if a, b, and c are positive real numbers, then a^a * b^b * c^c ≥ (abc)^((a+b+c)/3)

Imports (3)
Imported by 1 file
  1. lemma Usa1974P2.usa1974_p2_wlog line 29 source

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

    Statement uses: Real, GT.gt, OfNat.ofNat, GE.ge, HMul.hMul, HPow.hPow, HDiv.hDiv, HAdd.hAdd, Nat

    Proof uses: mul_pos, Eq, Eq.mpr, id, congrArg, Eq.trans, Real.rpow_add, congr, Real.mul_rpow, le_of_lt, congrFun', Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 77 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  2. problem Usa1974P2.usa1974_p2 line 58 source

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

    Statement uses: Real, GT.gt, OfNat.ofNat, GE.ge, HMul.hMul, HPow.hPow, HDiv.hDiv, HAdd.hAdd, Nat

    Proof uses: Not, Or, Classical.em, Usa1974P2.usa1974_p2_wlog, Eq.mpr, of_eq_true, Eq, Eq.trans, True, congr, congrArg, mul_assoc, mul_comm, mul_left_comm, congrFun', add_comm, add_left_comm, eq_self, le_of_lt, Iff.mp and 4 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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