Compfiles/Usa2018P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2018, Problem 1

Given that a,b,c are positive real numbers such that

a + b + c = 4 ∛(abc)

prove that 2(ab + bc + ca) + 4min(a²,b²,c²) ≥ a² + b² + c²

Imports (3)
Imported by 1 file
  1. lemma Usa2018P1.am_gm line 32 source

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

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

    Proof uses: Mathlib.Meta.NormNum.isRat_le_true, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, Eq.mpr, id, Eq, congrArg and 70 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  2. problem Usa2018P1.usa2018_p1 line 41 source

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

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

    Proof uses: LE.le, Not, Or, Classical.em, mul_self_le_mul_self, le_of_lt, Eq.mpr, id, congrFun', congrArg, Eq.trans, min_eq_left, le_of_add_le_add_right, Function.swap, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm and 162 more

    173 instances, coercions and auxiliary constants left out.

    Tactic trace: 72 steps

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