Compfiles/Imo1977P2.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1977, Problem 2

In a finite sequence of real numbers the sum of any seven successive terms is negative and the sum of any eleven successive terms is positive. Determine the maximum number of terms in the sequence.

Imports (2)
Imported by 1 file
  1. def Imo1977P2.sum_successive_terms line 27 source

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

    Statement uses: AddCommMonoid, Nat, Fin, NeZero, LT.lt, HSub.hSub, HAdd.hAdd, OfNat.ofNat

    Proof uses: Finset.sum, Finset.Icc, Fin.mk

    21 instances, coercions and auxiliary constants left out.

  2. def Imo1977P2.coeFunctionInt2Real line 37 source

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

    Statement uses: Int, Real

    2 instances, coercions and auxiliary constants left out.

  3. instance Imo1977P2.(instance at line 39) line 39 source
  4. theorem Imo1977P2.sum_successive_terms_intCast line 43 source

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

    Statement uses: Nat, Fin, Int, NeZero, LT.lt, HSub.hSub, HAdd.hAdd, OfNat.ofNat, Eq, Real, Imo1977P2.sum_successive_terms

    Proof uses: id, Finset.sum, Finset.Icc, Fin.mk, of_eq_true, Eq.trans, True, congrFun', congrArg, Int.cast_sum, eq_self

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  5. def Imo1977P2.example_16_int line 48 source

    standard axioms: propext what this means

    Statement uses: Fin, OfNat.ofNat, Nat, Int

    Proof uses: Matrix.vecCons, Neg.neg, Matrix.vecEmpty

    4 instances, coercions and auxiliary constants left out.

  6. def Imo1977P2.example_16 line 50 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real

    Proof uses: Imo1977P2.example_16_int

    3 instances, coercions and auxiliary constants left out.

  7. determine Imo1977P2.max_num_terms line 56 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  8. problem Imo1977P2.imo1977_p2 line 58 source

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

    Statement uses: Maximal, Nat, Exists, Fin, Real, And, LT.lt, HSub.hSub, HAdd.hAdd, OfNat.ofNat, Imo1977P2.sum_successive_terms, Imo1977P2.max_num_terms

    Proof uses: Eq.mpr, Not, id, Eq, congrArg, propext, maximal_iff_forall_gt, And.intro, Exists.intro, Imo1977P2.example_16, Imo1977P2.example_16_int, Int, Eq.symm, Imo1977P2.sum_successive_terms_intCast, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, NeZero and 92 more

    188 instances, coercions and auxiliary constants left out.

    Tactic trace: 60 steps

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