Compfiles/Imo2014P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2014, Problem 1

Let a₀ < a₁ < a₂ < ... an infinite sequence of positive integers. Prove that there exists a unique integer n ≥ 1 such that

aₙ < (a₀ + a₁ + ... + aₙ)/n ≤ aₙ₊₁.

Imports (2)
Imported by 1 file
  1. lemma Imo2014P1.lemma0 line 30 source

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

    Statement uses: Nat, ExistsUnique, HAdd.hAdd, OfNat.ofNat, And, LT.lt

    Proof uses: Eq, Exists.intro, And.intro, Nat.succ_pos, HSub.hSub

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  2. lemma Imo2014P1.lemma1 line 36 source

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

    Statement uses: Nat, Int, LT.lt, HAdd.hAdd, OfNat.ofNat, ExistsUnique, And, LE.le

    Proof uses: StrictMono, strictMono_nat_of_lt_succ, Set, Set.ofPred, Exists, Membership.mem, Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, CharP.cast_eq_zero, add_zero, Exists.intro, Int.toNat, HSub.hSub, Eq.mpr, id, Eq and 21 more

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 44 steps

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

  3. problem Imo2014P1.imo2014_p1 line 78 source

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

    Statement uses: Nat, Int, LT.lt, OfNat.ofNat, HAdd.hAdd, ExistsUnique, And, HMul.hMul, Finset.sum, Finset.range, LE.le

    Proof uses: HSub.hSub, Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, funext, Finset.sum_sub_distrib, HSMul.hSMul, Finset.card, Finset.sum_const, Finset.card_range, eq_self, congr, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, one_mul and 82 more

    111 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

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