Compfiles/Imo1995P2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1995, Problem 2

Let a, b, c be positive real numbers such that abc = 1. Show that

1 / (a³(b + c)) + 1 / (b³(c + a)) + 1 / (c³(a + b)) ≥ 3/2.

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

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

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

    Proof uses: GE.ge, Fin, Unit, Real.sqrt, Finset.sum, Insert.insert, Finset, Singleton.singleton, Finset.sum_mul_sq_le_sq_mul_sq, Inv.inv, le_of_lt, mul_pos, inv_pos_of_pos, add_pos', pow_pos, of_eq_true, Eq.trans, True, congr, congrArg and 194 more

    194 instances, coercions and auxiliary constants left out.

    Tactic trace: 102 steps

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