Compfiles/Usa1985P5.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

7 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1985, Problem 5

0 < a₁ ≤ a₂ ≤ a₃ ≤ ⋯ is an unbounded sequence of integers. Let bₙ = m if aₘ is the first member of the sequence to equal or exceed n. Given that a₁₉ = 85, what is the maximum possible value of a₁ + a₂ + ⋯ + a₁₉ + b₁ + b₂ + ⋯ + b₈₅?

Imports (5)
Imported by 1 file
  1. abbrev Usa1985P5.c The first index i (0-based) such that n ≤ a i line 31 source

    Source documentation

    The first index i (0-based) such that n ≤ a i. This exists because a is unbounded. The problem's bₙ is c a hu n + 1 (the 1-based index).

    no axioms what this means

    Statement uses: Nat, Exists, LE.le

    Proof uses: Nat.find

    3 instances, coercions and auxiliary constants left out.

    noncomputable abbrev c (a : ℕ → ℕ) (hu : ∀ n, ∃ i, n ≤ a i) (n : ℕ) : ℕ :=
…
  2. lemma Usa1985P5.find_iff line 36 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Nat, Monotone, Exists, LE.le, Iff, Usa1985P5.c

    Proof uses: Iff.intro, le_trans, Nat.find, Nat.find_spec, Nat.find_le

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  3. lemma Usa1985P5.sum_indicator_left ∑ j ∈ range 85, (if j < a i then 1 else 0) counts the elements of range (a i) when a i ≤ 85 line 46 source

    Source documentation

    ∑ j ∈ range 85, (if j < a i then 1 else 0) counts the elements of range (a i) when a i ≤ 85.

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Finset.sum, Finset.range, ite, LT.lt

    Proof uses: Eq.mpr, Finset.card, Finset.filter, id, congrArg, Eq.symm, Finset.card_filter, Finset, Finset.ext, Iff, Membership.mem, And, congr, Eq.trans, congrFun', Iff.intro, And.right, And.intro, lt_of_lt_of_le, Finset.card_range and 1 more

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

    lemma sum_indicator_left {a : ℕ → ℕ} {i : ℕ} (hi : a i ≤ 85) :
    ∑ j ∈ Finset.range 85, (if j < a i then 1 else 0) = a i := by
…
  4. lemma Usa1985P5.sum_indicator_right ∑ i ∈ range 19, (if i < c a hu (j+1) then 1 else 0) counts the elements of range (c a hu (j+1)) when c a hu (j+1) ≤ 18 line 59 source

    Source documentation

    ∑ i ∈ range 19, (if i < c a hu (j+1) then 1 else 0) counts the elements of range (c a hu (j+1)) when c a hu (j+1) ≤ 18.

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

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

    Proof uses: Eq.mpr, Finset.card, Finset.filter, id, congrArg, Eq.symm, Finset.card_filter, Finset, Finset.ext, Iff, Membership.mem, And, congr, Eq.trans, congrFun', Iff.intro, And.right, And.intro, lt_of_lt_of_le, Finset.card_range and 1 more

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    lemma sum_indicator_right {a : ℕ → ℕ} {hu : ∀ n, ∃ i, n ≤ a i} {j : ℕ}
    (hj : c a hu (j + 1) ≤ 18) :
    ∑ i ∈ Finset.range 19, (if i < c a hu (j + 1) then 1 else 0) = c a hu (j + 1) := by
…

    Mentions: Usa1985P5.c

  5. lemma Usa1985P5.sum_eq The key identity: the sum is constant line 76 source

    Source documentation

    The key identity: the sum is constant. Double-count the pairs (i, j) ∈ range 19 × range 85: for each pair, exactly one of j < a i and i < c a hu (j+1) holds, so the two indicator sums add up to 19 * 85; the extra + 1 in each b term contributes another 85.

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

    Statement uses: Nat, Monotone, Exists, LE.le, Eq, OfNat.ofNat, HAdd.hAdd, Finset.sum, Finset.range, Usa1985P5.c

    Proof uses: Iff, LT.lt, Eq.mpr, Not, id, congrArg, Eq.symm, propext, Nat.not_le, Usa1985P5.find_iff, Iff.trans, Nat.lt_add_one_iff, Membership.mem, Finset, Iff.mp, Finset.mem_range, Nat.find_le, ite, Finset.sum_congr, rfl and 39 more

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 44 steps

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

    lemma sum_eq (a : ℕ → ℕ) (hm : Monotone a) (hu : ∀ n, ∃ i, n ≤ a i)
    (h19 : a 18 = 85) :
    ∑ i ∈ Finset.range 19, a i + ∑ j ∈ Finset.range 85, (c a hu (j + 1) + 1) = 1700 := by
…

    Mentions: Usa1985P5.c

  6. determine Usa1985P5.solution line 136 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  7. problem Usa1985P5.usa1985_p5 line 138 source

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

    Statement uses: IsGreatest, Nat, Set.ofPred, Exists, Monotone, LT.lt, OfNat.ofNat, LE.le, And, Eq, HAdd.hAdd, Finset.sum, Finset.range, Usa1985P5.c, Usa1985P5.solution

    Proof uses: HSub.hSub, Nat.add_le_add_left, Nat.sub_le_sub_right, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Exists.intro, And.intro, Membership.mem, Set, upperBounds, Eq.symm, Usa1985P5.sum_eq, Eq.mpr, congrArg, le_of_eq

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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