Compfiles/Usa1992P3.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Usa1992P3.monotone_of_consec_lt If the values a 0, …, a 10 are strictly increasing, then a is monotone on the interval [0, 10] line 37 source

   Source documentation

   If the values a 0, …, a 10 are strictly increasing, then a is monotone on the interval [0, 10].

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

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

   Proof uses: Nat.recAux, le_rfl, Eq.mpr, id, Eq, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HMul.hMul, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_pf_add_lt and 5 more

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 18 steps

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

   lemma monotone_of_consec_lt (a : ℕ → ℕ) (h : ∀ i, i < 10 → a i < a (i + 1))
       {i j : ℕ} (hij : i ≤ j) (hj : j ≤ 10) : a i ≤ a j := by
   …

   Mentions: h

2. lemma Usa1992P3.gap The key gap lemma: writing s j for the sum of the j smallest elements, if s j < 1500 then the next element satisfies a j ≤ s j + 1 line 59 source

   Source documentation

   The key gap lemma: writing s j for the sum of the j smallest elements, if s j < 1500 then the next element satisfies a j ≤ s j + 1. Indeed, s j + 1 ≤ 1500 must occur as a subset sum, and any subset with that sum must contain some a i with i ≥ j, so a j ≤ a i ≤ s j + 1.

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

   Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Finset, And, Finset.range, Eq, Finset.sum, LT.lt, HAdd.hAdd

   Proof uses: Decidable.byContradiction, Not, Membership.mem, Iff.mp, Finset.mem_range, Eq.mp, Finset.single_le_sum, Nat.zero_le, Iff.mpr, Finset.sum_le_sum_of_subset

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 18 steps

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

   lemma gap (a : ℕ → ℕ)
       (hsub : ∀ n : ℕ, 1 ≤ n → n ≤ 1500 →
         ∃ t : Finset ℕ, t ⊆ Finset.range 11 ∧ ∑ i ∈ t, a i = n)
       (hmono : ∀ {i j : ℕ}, i ≤ j → j ≤ 10 → a i ≤ a j)
       {j : ℕ} (_hj : j ≤ 10)
       (hs : ∑ i ∈ Finset.range j, a i < 1500) :
       a j ≤ ∑ i ∈ Finset.range j, a i + 1 := by
   …

3. lemma Usa1992P3.pow_bound Induction using the gap lemma: the sum of the k smallest elements is at most 2 ^ k - 1, for every k ≤ 10 line 90 source

   Source documentation

   Induction using the gap lemma: the sum of the k smallest elements is at most 2 ^ k - 1, for every k ≤ 10.

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

   Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Finset, And, Finset.range, Eq, Finset.sum, HSub.hSub, HPow.hPow

   Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', pow_zero, tsub_self, HAdd.hAdd, pow_le_pow_right', Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, LT.lt, Usa1992P3.gap, Eq.mpr, id, Finset.sum_range_succ and 5 more

   64 instances, coercions and auxiliary constants left out.

   Tactic trace: 19 steps

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

   lemma pow_bound (a : ℕ → ℕ)
       (hsub : ∀ n : ℕ, 1 ≤ n → n ≤ 1500 →
         ∃ t : Finset ℕ, t ⊆ Finset.range 11 ∧ ∑ i ∈ t, a i = n)
       (hmono : ∀ {i j : ℕ}, i ≤ j → j ≤ 10 → a i ≤ a j) :
       ∀ k : ℕ, k ≤ 10 → ∑ i ∈ Finset.range k, a i ≤ 2 ^ k - 1 := by
   …

4. def Usa1992P3.Good Documented declaration: Good line 116 source

   Source documentation

   Formalization of "a set of 11 distinct positive integers such that every integer between 1 and 1500 is the sum of a subset", with the elements listed in increasing order as a 0 < a 1 < … < a 10.

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

   Statement uses: Nat

   Proof uses: And, LT.lt, OfNat.ofNat, HAdd.hAdd, LE.le, Exists, Finset, Finset.range, Eq, Finset.sum

   9 instances, coercions and auxiliary constants left out.

   def Good (a : ℕ → ℕ) : Prop :=
   …

5. determine Usa1992P3.answer The answer to the problem line 122 source

   Source documentation

   The answer to the problem.

   no axioms what this means

   Statement uses: Nat

   Proof uses: OfNat.ofNat

   1 instances, coercions and auxiliary constants left out.

   determine answer : ℕ := 248

6. problem Usa1992P3.usa1992_p3 line 124 source

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

   Statement uses: IsLeast, Nat, Set.ofPred, Exists, And, Usa1992P3.Good, Eq, OfNat.ofNat, Usa1992P3.answer

   Proof uses: And.intro, Membership.mem, Set, lowerBounds, Exists.intro, List.getD, List.cons, List.nil, LT.lt, HAdd.hAdd, LE.le, Finset, Finset.range, Finset.sum, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl and 61 more

   81 instances, coercions and auxiliary constants left out.

   Tactic trace: 116 steps

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