Compfiles/Usa1997P6.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1997, Problem 6

Suppose the sequence of nonnegative integers a₁, a₂, ..., a₁₉₉₇ satisfies

aᵢ + aⱼ ≤ aᵢ₊ⱼ ≤ aᵢ + aⱼ + 1

for all i, j ≥ 1 with i + j ≤ 1997. Prove that there exists a real number x such that aₙ = ⌊nx⌋ for all 1 ≤ n ≤ 1997.

Imports (4)
Imported by 1 file
  1. lemma Usa1997P6.key_ineq line 43 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, HMul.hMul

    Proof uses: Eq, Nat.strong_induction_on, LT.lt, Or, lt_trichotomy, Exists, Exists.intro, HSub.hSub, rfl, Trans.trans, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.mpr, id, congrArg, Eq.symm and 19 more

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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

  2. problem Usa1997P6.usa1997_p6 line 84 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Exists, Real, Eq, Int, Int.floor, HMul.hMul

    Proof uses: And, Membership.mem, Finset, Finset.Icc, HDiv.hDiv, Finset.exists_max_image, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, and_self, Eq.mp, propext, Finset.mem_Icc, Iff.mpr, And.intro, Usa1997P6.key_ineq, LT.lt and 65 more

    144 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

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