Compfiles/Imo2001P2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2001, Problem 2

Let a, b, c be positive reals. Prove that

a / √(a² + 8bc) + b / √(b² + 8ca) + c / √(c² + 8ab) ≥ 1.

Imports (2)
Imported by 1 file
  1. theorem Imo2001P2.bound line 46 source

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

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

    Proof uses: Eq.mpr, id, Eq, congrArg, propext, div_le_div_iff₀, add_pos', pow_pos, Real.sqrt_pos_of_pos, inferInstance, Zero, PartialOrder, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Trans.trans and 71 more

    122 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  2. theorem Imo2001P2.imo2001_p2' line 61 source

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

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

    Proof uses: Ne, ne_of_gt, add_pos', pow_pos, Trans.trans, GE.ge, Eq, add_le_add, Imo2001P2.bound, Eq.mpr, Inv.inv, id, congrFun', congrArg, Eq.trans, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf and 78 more

    102 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. problem Imo2001P2.imo2001_p2 line 72 source

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

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

    Proof uses: Eq, Inv.inv, Eq.rec, Real.rpow_inv_natCast_pow, LT.lt.le, three_ne_zero, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Trans.trans, Imo2001P2.imo2001_p2', Real.rpow_pos_of_pos, Eq.mpr, id, congrArg

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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