Compfiles/Imo2012P2.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2012, Problem 2

Let a₂, a₃, ..., aₙ be positive reals with product 1, where n ≥ 3. Show that (1 + a₂)²(1 + a₃)³...(1 + aₙ)ⁿ > nⁿ.

Imports (3)
Imported by 1 file
  1. lemma Imo2012P2.Finset.prod_eq_prod_iff_of_pos_of_le line 32 source

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

    Statement uses: CommMonoidWithZero, PartialOrder, ZeroLEOneClass, PosMulStrictMono, MulPosStrictMono, Nontrivial, DecidableEq, Finset, Membership.mem, LT.lt, OfNat.ofNat, LE.le, Iff, Eq, Finset.prod

    Proof uses: Iff.intro, Finset.erase, Finset.prod_le_prod₀, le_of_lt, Finset.mem_of_mem_erase, lt_of_le_of_lt', Finset.prod_pos, And.left, Eq.mp, HMul.hMul, And, congrArg, propext, mul_eq_mul_iff_eq_and_eq_of_pos, Insert.insert, Finset.prod_insert, Finset.notMem_erase, Eq.symm, Finset.insert_erase, Finset.prod_congr and 1 more

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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

  2. lemma Imo2012P2.Real.geom_mean_eq_arith_mean2_weighted_iff line 58 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, Iff, HMul.hMul, HPow.hPow

    Proof uses: Fin, Nat.succ, Nat, Membership.mem, Finset, Finset.univ, Matrix.vecCons, Matrix.vecEmpty, Finset.sum, LE.le, Finset.prod, Real.geom_mean_eq_arith_mean_weighted_iff_of_pos', And, Eq.mp, Eq.trans, implies_congr, forall_congr, True, Eq.refl, congrArg and 18 more

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  3. lemma Imo2012P2.aux₁ line 74 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Real, HPow.hPow, Finset.prod, Finset.Icc, HDiv.hDiv, HSub.hSub

    Proof uses: Nat.le_induction, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congr, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, Singleton.singleton, Finset, Finset.prod_congr, Finset.Icc_self, Membership.mem, Finset.prod_div_distrib and 43 more

    141 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  4. lemma Imo2012P2.aux₂ line 82 source

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

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

    Proof uses: Eq.mpr, id, congrArg, propext, Nat.cast_pos, Eq.symm, Nat.cast_one, Nat.cast_sub, Real.rpow_natCast, Real.mul_rpow, le_of_lt, Real.rpow_pos_of_pos, div_pos, inferInstance, PartialOrder, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble and 47 more

    118 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

  5. lemma Imo2012P2.aux₃ line 99 source

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

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

    Proof uses: Eq.mpr, id, congrArg, propext, Nat.cast_pos, Eq.symm, Nat.cast_one, Nat.cast_sub, Real.rpow_natCast, Real.mul_rpow, le_of_lt, Iff.mpr, Nat.cast_pos', lt_of_lt_of_le, inferInstance, PartialOrder, Zero, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 66 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  6. lemma Imo2012P2.aux₄ line 112 source

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

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

    Proof uses: Eq.mpr, id, Eq, congrArg, propext, Nat.cast_pos, Eq.symm, Nat.cast_one, Nat.cast_sub, Imo2012P2.aux₂, Imo2012P2.aux₃, mul_le_mul_iff_right₀, pow_pos, Iff.mpr, Nat.cast_pos', lt_of_lt_of_le, inferInstance, PartialOrder, Zero, Mathlib.Meta.Positivity.pos_of_isNat and 73 more

    145 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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

  7. lemma Imo2012P2.aux₅ line 125 source

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

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

    Proof uses: Eq.mpr, id, congrArg, propext, Nat.cast_pos, Eq.symm, Nat.cast_one, Nat.cast_sub, Imo2012P2.aux₂, Imo2012P2.aux₃, mul_left_cancel_iff_of_pos, pow_pos, Iff.mpr, Nat.cast_pos', lt_of_lt_of_le, inferInstance, PartialOrder, Zero, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat and 73 more

    136 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  8. lemma Imo2012P2.aux₆ line 139 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Real, Finset.prod, Finset.Icc, HSub.hSub, Nat.factorial

    Proof uses: Nat.le_induction, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAddMonoidWithOne, congr, congrArg, Singleton.singleton, Finset, Finset.prod_congr, Finset.Icc_self, Membership.mem, Eq.refl, Finset.prod_singleton, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_sub, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_natCast and 72 more

    133 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  9. problem Imo2012P2.imo2012_p2 line 153 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Subtype, Membership.mem, Finset, Finset.Icc, Real, LT.lt, Eq, Finset.prod, Finset.univ, HPow.hPow, HAdd.hAdd

    Proof uses: dite, Subtype.mk, Not, id, Eq.mpr, Subtype.property, congrArg, dite_eq_left, Eq.refl, Finset.prod_congr, Eq.symm, Finset.prod_subtype, of_eq_true, Iff, Eq.trans, True, forall_congr, And, congr, iff_self and 48 more

    132 instances, coercions and auxiliary constants left out.

    Tactic trace: 72 steps

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