Compfiles/Imo2010P6.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2010, Problem 6

Let a₁, a₂, a₃, ... be a sequence of positive real numbers. Suppose that for some positive integer s, we have aₙ = max{aₖ + aₙ₋ₖ | 1 ≤ k ≤ n − 1} for all n > s. Prove that there exist positive integers l and N, with l ≤ s and such that aₙ = aₗ + aₙ₋ₗ for all n ≥ N.

Imports (2)
Imported by 1 file
  1. def Imo2010P6.rec_max line 29 source

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

    Statement uses: PNat, Real, LT.lt, OfNat.ofNat, Nat

    Proof uses: Finset.max', Finset.image, HAdd.hAdd, HSub.hSub, Finset.Icc

    27 instances, coercions and auxiliary constants left out.

  2. def Imo2010P6.Rec line 32 source

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

    Statement uses: PNat, Real

    Proof uses: GT.gt, Eq, Imo2010P6.rec_max

    8 instances, coercions and auxiliary constants left out.

  3. lemma Imo2010P6.exists_max_ratio line 39 source

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

    Statement uses: PNat, Real, Exists, And, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Nat, LE.le, HDiv.hDiv

    Proof uses: Finset.exists_max_image, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, and_self

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. lemma Imo2010P6.finset_nonempty line 43 source

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

    Statement uses: PNat, Finset.Nonempty, Finset.Icc, OfNat.ofNat, Nat

    Proof uses: Iff.mpr, LE.le, Finset.nonempty_Icc, one_le

    23 instances, coercions and auxiliary constants left out.

  5. def Imo2010P6.res line 45 source

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

    Statement uses: PNat, Real

    Proof uses: HSub.hSub, HMul.hMul, HDiv.hDiv

    10 instances, coercions and auxiliary constants left out.

  6. lemma Imo2010P6.ne_zero_coe line 47 source

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

    Statement uses: PNat, Ne, Real, OfNat.ofNat

    Proof uses: ne_of_gt, Iff.mpr, LT.lt, Nat, Nat.cast_pos', PNat.pos

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. lemma Imo2010P6.res_nonpos line 49 source

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

    Statement uses: PNat, Real, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Nat, LE.le, HDiv.hDiv, Imo2010P6.res

    Proof uses: Trans.trans, Eq, HSub.hSub, HMul.hMul, rfl, Eq.mpr, id, congrArg, Eq.symm, mul_div_cancel₀, Imo2010P6.ne_zero_coe, Eq.refl, Eq.trans, HAdd.hAdd, sub_add_cancel, of_eq_true, LT.lt, True, Eq.mp, sub_self

    87 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  8. lemma Imo2010P6.max_of_image line 60 source

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

    Statement uses: Finset, Real, Finset.Nonempty, Eq, Finset.max', Finset.image, Iff.mpr, Finset.image_nonempty, Exists, And, Membership.mem

    Proof uses: Iff.mp, Finset.mem_image, Finset.max'_mem, Exists.intro, And.intro, Eq.trans, Eq.symm

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  9. lemma Imo2010P6.sum_multiset line 66 source

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

    Statement uses: Finset, PNat, Multiset, Subtype, Membership.mem, Real, Exists, Eq, HAdd.hAdd, Multiset.sum, Multiset.map, Bind.bind, Pure.pure

    Proof uses: Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, Function.comp, Multiset.map_congr, Multiset.bind_singleton, Eq.refl, Multiset.map_map, Multiset.bind, Singleton.singleton, Multiset.map_add, Multiset.sum_add, eq_self, eq_true, True.intro

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  10. lemma Imo2010P6.res_expansion line 71 source

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

    Statement uses: PNat, Real, Imo2010P6.Rec, Imo2010P6.res, Exists, Multiset, Subtype, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Nat, Eq, Multiset.sum, Multiset.map, Bind.bind, Pure.pure

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  11. lemma Imo2010P6.Multiset.sum_nonpos line 88 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: AddCommGroup, Preorder, Multiset, AddLeftMono, AddRightMono, Membership.mem, LE.le, OfNat.ofNat, Multiset.sum

    Proof uses: Multiset.map, Neg.neg, And, Eq, Exists, Iff.mp, Multiset.mem_map, Eq.mpr, id, congrArg, Eq.symm, Iff.mpr, neg_nonneg, Eq.mp, Eq.trans, Multiset.sum_map_neg', Multiset.sum_nonneg

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  12. lemma Imo2010P6.res_bounded_above line 99 source

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

    Statement uses: PNat, Real, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Nat, LE.le, Imo2010P6.res, Imo2010P6.Rec

    Proof uses: Multiset, Subtype, Eq, Multiset.sum, Multiset.map, Bind.bind, Pure.pure, Exists, Imo2010P6.res_expansion, Eq.mpr, id, congrArg, Imo2010P6.Multiset.sum_nonpos, And, Iff.mp, Multiset.mem_map, Eq.mp, Subtype.mk, Iff.mpr, Iff.of_eq and 9 more

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  13. lemma Imo2010P6.sub_lt line 112 source

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

    Statement uses: PNat, LT.lt, HSub.hSub

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  14. lemma Imo2010P6.bounded_below_aux line 114 source

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

    Statement uses: PNat, Real, LE.le, GT.gt, HAdd.hAdd, Exists, And, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Nat

    Proof uses: PNat.strongInductionOn, LT.lt, dite, Exists.intro, And.intro, Iff.mpr, Finset.mem_Icc, Subtype.property, Std.IsPreorder.le_refl, Not, Std.lt_of_le_of_lt, Eq.mp, HSub.hSub, Imo2010P6.sub_lt

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  15. lemma Imo2010P6.res_bounded_below line 125 source

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

    Statement uses: PNat, Real, LE.le, GT.gt, HAdd.hAdd, Imo2010P6.res, Exists, Neg.neg

    Proof uses: Exists.intro, Finset.max', Finset.image, abs, Finset.Icc, OfNat.ofNat, Nat, Iff.mpr, Finset.Nonempty, Finset.image_nonempty, Imo2010P6.finset_nonempty, And, Membership.mem, Finset, Imo2010P6.bounded_below_aux, Finset.mem_image_of_mem, Finset.le_max', le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl and 51 more

    85 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  16. lemma Imo2010P6.finite_bounded_card_multisets line 133 source

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

    Statement uses: Finset, Real, Set.Finite, Multiset, Subtype, Membership.mem, Set.ofPred, LE.le, Multiset.card

    Proof uses: Set.Finite.subset, Set.image, List, Nat, List.length, Nat.ceil, Set.Finite.image, List.finite_length_le, Set, Eq, Quotient, Quotient.mk, Exists, Quotient.exists_rep, Exists.intro, And, And.intro, Iff.mp, Nat.cast_le, le_trans and 2 more

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  17. lemma Imo2010P6.sum_filter_eq_zero line 140 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: DecidableEq, AddCommMonoid, Multiset, Eq, Multiset.sum, Multiset.filter, OfNat.ofNat

    Proof uses: Eq.mpr, Multiset.replicate, Multiset.count, id, congrArg, Multiset.filter_eq', of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, Nat, Multiset.sum_replicate, nsmul_zero, eq_self

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  18. lemma Imo2010P6.pos_of_min_of_abs_ne_zero line 145 source

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

    Statement uses: Finset, Real, Finset.Nonempty, Finset.filter, Ne, OfNat.ofNat, Eq, LT.lt, Finset.min', Finset.image, abs, Iff.mpr, Finset.image_nonempty

    Proof uses: Membership.mem, Finset.min'_mem, And, Exists, Iff.mp, Finset.mem_image, Eq.mpr, id, congrArg, Eq.symm, abs_pos, And.right, Finset.mem_filter

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  19. lemma Imo2010P6.map_sum_le_sup_mul_card line 153 source

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

    Statement uses: Multiset, Real, Membership.mem, LE.le, Multiset.sum, Multiset.map, HMul.hMul, Multiset.card

    Proof uses: Eq, Nat, of_eq_true, Eq.trans, True, congrArg, Multiset.card_map, eq_self, Eq.mpr, id, HSMul.hSMul, Multiset.sum_le_card_nsmul

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  20. lemma Imo2010P6.res_expansion_bounded line 161 source

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

    Statement uses: PNat, Real, LT.lt, OfNat.ofNat, Imo2010P6.Rec, Imo2010P6.res, Membership.mem, Finset, Finset.Icc, Nat, Ne, LE.le, Neg.neg, Exists, Multiset, Subtype, And, Eq, Multiset.sum, Multiset.map and 4 more

    Proof uses: Imo2010P6.res_expansion, Multiset.filter, Subtype.property, And.right, Iff.mp, Multiset.mem_filter, Eq.mpr, HAdd.hAdd, Not, id, congrArg, Eq.symm, Multiset.sum_filter_add_sum_filter_not, congr, Eq.trans, Multiset.filter.congr_simp, Eq.refl, Function.comp, Multiset.map_congr, Multiset.bind_singleton and 63 more

    135 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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

  21. lemma Imo2010P6.res_range_finite line 188 source

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

    Statement uses: PNat, Real, LE.le, Imo2010P6.res, OfNat.ofNat, Exists, Neg.neg, Imo2010P6.Rec, Finset, Membership.mem

    Proof uses: dite, Finset.Icc, Nat, Eq, Classical.propDecidable, Exists.intro, Singleton.singleton, Multiset, Subtype, Multiset.sum, Multiset.map, Bind.bind, Pure.pure, Imo2010P6.res_expansion, Eq.mpr, id, congrArg, Eq.trans, Function.comp, Multiset.map_congr and 42 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 36 steps

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

  22. lemma Imo2010P6.coe_mul_sub line 231 source

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

    Statement uses: Real, PNat, LT.lt, Eq, HMul.hMul, HSub.hSub

    Proof uses: HAdd.hAdd, cast, Eq.symm, Eq.trans, Nat, congrFun', congrArg, PNat.sub_add_of_lt

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  23. lemma Imo2010P6.max_of_image_sub line 235 source

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

    Statement uses: Finset, PNat, Real, Finset.Nonempty, Eq, Finset.max', Finset.image, HSub.hSub, Iff.mpr, Finset.image_nonempty

    Proof uses: Eq.mpr, Function.comp, id, congrArg, Finset.image_image, Eq.refl, Monotone, LE.le, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast and 38 more

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  24. lemma Imo2010P6.res_rec line 244 source

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

    Statement uses: PNat, Real, Imo2010P6.Rec, Imo2010P6.res

    Proof uses: GT.gt, LT.lt, OfNat.ofNat, Nat, one_lt_of_gt, HDiv.hDiv, Eq, Imo2010P6.rec_max, Finset.max', Finset.image, HSub.hSub, HAdd.hAdd, HMul.hMul, Finset.Icc, Iff.mpr, Finset.Nonempty, Finset.image_nonempty, Imo2010P6.finset_nonempty, id, LinearOrder and 19 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  25. lemma Imo2010P6.res_l_zero line 258 source

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

    Statement uses: PNat, Real, Eq, Imo2010P6.res, OfNat.ofNat

    Proof uses: GT.gt, Iff.mpr, LT.lt, Nat, Nat.cast_pos', PNat.pos, HMul.hMul, HDiv.hDiv, of_eq_true, Eq.trans, True, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, List.nil, Prod, Int, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, congr_arg₂ and 37 more

    62 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  26. lemma Imo2010P6.res_step_monotone line 263 source

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

    Statement uses: PNat, Real, Imo2010P6.Rec, Imo2010P6.res, GT.gt, HAdd.hAdd, LE.le

    Proof uses: LT.lt, OfNat.ofNat, Nat, one_lt_of_gt, Trans.trans, Eq, Imo2010P6.rec_max, HSub.hSub, Eq.symm, Iff.mpr, add_eq_right, Imo2010P6.res_l_zero, Eq.mpr, id, congrArg, PNat.add_sub, Eq.refl, Finset.le_max', Finset.image, Finset.Icc and 13 more

    62 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  27. lemma Imo2010P6.eventually_eq_succ_of_mem_finset_of_monotone line 279 source

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

    Statement uses: PNat, Real, Finset, Membership.mem, LT.lt, LE.le, Exists, GT.gt, Eq, HAdd.hAdd, OfNat.ofNat, Nat

    Proof uses: And, Set.Ioi, Set, Set.Finite, Set.range, Set.Finite.subset, Finset.finite_toSet, Eq.mpr, id, Set.Finite.toFinset, Finset.Nonempty, Set.Nonempty, congrArg, propext, Set.Finite.toFinset_nonempty, Set.range_nonempty, Set.Finite.mem_toFinset, Set.mem_range_self, Finset.max', Finset.max'_mem and 13 more

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

  28. lemma Imo2010P6.mono_of_mono_succ_rec line 314 source

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

    Statement uses: PNat, Real, LT.lt, LE.le, HAdd.hAdd, OfNat.ofNat, Nat

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  29. lemma Imo2010P6.mono_of_mono_succ line 339 source

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

    Statement uses: PNat, Real, LT.lt, LE.le, HAdd.hAdd, OfNat.ofNat, Nat

    Proof uses: Eq.mpr, HSub.hSub, id, Eq, congrArg, Eq.symm, PNat.add_sub_of_lt, Imo2010P6.mono_of_mono_succ_rec

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  30. lemma Imo2010P6.res_eventually_t_step_eq line 344 source

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

    Statement uses: PNat, Real, Exists, Finset, Membership.mem, Imo2010P6.res, GT.gt, HAdd.hAdd, LE.le, Finset.Icc, OfNat.ofNat, Nat, HMul.hMul, Eq

    Proof uses: Iff.mpr, Multiset, Finset.val, Finset.mem_def, LT.lt, Trans.trans, le_mul_iff_one_le_right', one_le, PNat.lt_add_left, PNat.lt_add_right, Eq.mpr, id, Eq.trans, congrArg, add_one_mul, Eq.mp, add_assoc, Imo2010P6.eventually_eq_succ_of_mem_finset_of_monotone, Imo2010P6.mono_of_mono_succ, Exists.intro and 1 more

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  31. lemma Imo2010P6.decompose line 367 source

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

    Statement uses: PNat, LT.lt, Exists, And, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Nat, Eq, HAdd.hAdd, HMul.hMul

    Proof uses: Exists.intro, PNat.mod, PNat.div, Eq.mpr, id, congrArg, Eq.symm, PNat.mod_add_div, mul_comm, Eq.refl, Decidable.byContradiction, Not, LE.le, cast, Eq.trans_le, Eq.mp, add_zero, Nat.mul_zero, Nat.eq_zero_of_not_pos, And.right and 10 more

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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

  32. lemma Imo2010P6.res_eventually_step_eq line 385 source

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

    Statement uses: PNat, Real, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Nat, Exists, GT.gt, HAdd.hAdd, HMul.hMul, Eq, Imo2010P6.res, GE.ge

    Proof uses: Finset.max', Finset.image, Subtype, Subtype.property, Finset.attach, Iff.mpr, Finset.Nonempty, Finset.image_nonempty, Finset.attach_nonempty_iff, Imo2010P6.finset_nonempty, Exists.intro, And, Imo2010P6.decompose, lt_of_lt_of_le, PNat.lt_add_left, LT.lt, Trans.trans, LE.le, Finset.le_max', Eq.mpr and 16 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  33. lemma Imo2010P6.step_eq_of_res_step_eq line 404 source

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

    Statement uses: PNat, Real, LT.lt, Eq, Imo2010P6.res, HSub.hSub, HAdd.hAdd

    Proof uses: cast, Eq.symm, Eq.trans, Nat, congrArg, PNat.add_sub_of_lt, Eq.mpr, id, add_comm, HMul.hMul, HDiv.hDiv, congrFun', Eq.mp, add_mul, mul_div_cancel₀, ne_of_gt, OfNat.ofNat, Iff.mpr, Nat.cast_pos', PNat.pos and 73 more

    118 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  34. lemma Imo2010P6.eventual_step_eq_of_eventual_res_step_eq line 414 source

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

    Statement uses: PNat, Real, GE.ge, Eq, Imo2010P6.res, HAdd.hAdd, Exists, HSub.hSub

    Proof uses: Exists.intro, Max.max, OfNat.ofNat, Nat, LT.lt, Trans.trans, LE.le, PNat.lt_succ_self, le_max_right, le_of_lt, PNat.lt_add_right, cast, Eq.symm, of_eq_true, Eq.trans, True, congr, congrArg, add_comm, Or and 10 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  35. problem Imo2010P6.imo2010_p6 line 439 source

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

    Statement uses: PNat, Real, Imo2010P6.Rec, Exists, And, LE.le, GE.ge, Eq, HAdd.hAdd, HSub.hSub

    Proof uses: Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Nat, HDiv.hDiv, Imo2010P6.exists_max_ratio, And.right, Iff.mp, Finset.mem_Icc, Imo2010P6.res, Imo2010P6.res_rec, Imo2010P6.res_nonpos, GT.gt, Imo2010P6.res_step_monotone, Imo2010P6.res_bounded_above, Neg.neg, Imo2010P6.res_bounded_below, Imo2010P6.res_range_finite, HMul.hMul and 5 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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