Compfiles/Usa1981P5.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1981, Problem 5

Show that for any positive real number x and any nonnegative integer n,

∑ₖ (⌊kx⌋/k) ≤ ⌊nx⌋

where the sum goes from k = 1 to k = n, inclusive.

Imports (2)
Imported by 2 files
  1. problem Usa1981P5.usa1981_p5 line 30 source

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

    Statement uses: Real, Nat, LE.le, Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, Int.floor, HMul.hMul

    Proof uses: Eq.mpr, HSub.hSub, Int.fract, id, Eq, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, congrFun', sub_div, mul_div_right_comm, Finset.sum_sub_distrib, And.left, Eq.mp, And, propext, Finset.mem_Icc and 104 more

    172 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

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