Compfiles/Usa2026P1.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2026, Problem 1

Fix an integer n ≥ 2. For which real numbers x is ⌊nx⌋ - ∑_{k=1}^n ⌊kx⌋/k maximal, and what is the maximal value that this expression can take?

Imports (3)
Imported by 1 file
  1. def Usa2026P1.f line 31 source

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

    Statement uses: Nat, Real

    Proof uses: HSub.hSub, Int.floor, HMul.hMul, Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv

    18 instances, coercions and auxiliary constants left out.

  2. determine Usa2026P1.solution_value line 34 source

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

    Statement uses: Nat, Real

    Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv

    11 instances, coercions and auxiliary constants left out.

  3. lemma Usa2026P1.f_periodic line 43 source

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

    Statement uses: Nat, Real, Eq, Usa2026P1.f, HAdd.hAdd, OfNat.ofNat

    Proof uses: id, Eq.mpr, HSub.hSub, Int.floor, HMul.hMul, Finset.sum, Finset.Icc, HDiv.hDiv, congrFun', congrArg, congr, Int, mul_add, Finset.sum_congr, Eq.refl, Finset, Membership.mem, mul_one, Int.floor_add_natCast, Eq.trans and 62 more

    121 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

  4. def Usa2026P1.T line 69 source

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

    Statement uses: Nat, Real

    Proof uses: HSub.hSub, Int.ceil, HMul.hMul, OfNat.ofNat, Finset.sum, Finset.Icc, HDiv.hDiv, Int

    22 instances, coercions and auxiliary constants left out.

  5. lemma Usa2026P1.f_rewrite line 72 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Real, Eq, Usa2026P1.f, HSub.hSub, Usa2026P1.solution_value, Usa2026P1.T

    Proof uses: id, Int.floor, HMul.hMul, Finset.sum, Finset.Icc, HDiv.hDiv, Eq.mpr, Int.ceil, Int, congrFun', congrArg, congr, mul_sub, Finset.sum_congr, Eq.refl, Finset, Membership.mem, mul_one, HAdd.hAdd, Neg.neg and 97 more

    147 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

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

  6. lemma Usa2026P1.T_eq_zero_of_small_y line 121 source

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

    Statement uses: Nat, Real, LE.le, OfNat.ofNat, LT.lt, HDiv.hDiv, Eq, Usa2026P1.T

    Proof uses: id, Iff.mpr, Nat.cast_pos, Membership.mem, Finset, Finset.Icc, Int, Int.ceil, HMul.hMul, And.left, Iff.mp, And, Finset.mem_Icc, And.right, Nat.cast_le, mul_pos, Trans.trans, mul_le_mul_of_nonneg_left, le_of_lt, mul_one_div and 74 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 31 steps

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

  7. lemma Usa2026P1.core_sum_bound line 154 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Real, Finset.sum, Finset.Icc, HDiv.hDiv, HSub.hSub, Int, Int.ceil, HMul.hMul, HAdd.hAdd

    Proof uses: HPow.hPow, Int.floor, Usa1981P5.usa1981_p5, Eq, Iff.mpr, Nat.cast_pos, Ne, ne_of_gt, id, Trans.trans, rfl, mul_sub, HSub, Eq.rec, Eq.refl, mul_div_cancel₀, mul_one_div, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 197 more

    223 instances, coercions and auxiliary constants left out.

    Tactic trace: 136 steps

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

  8. lemma Usa2026P1.T_nonneg line 308 source

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

    Statement uses: Nat, Real, LE.le, OfNat.ofNat, LT.lt, Usa2026P1.T

    Proof uses: Iff.mpr, Nat.cast_pos, Int, HSub.hSub, Int.ceil, HMul.hMul, mul_pos, Int.ceil_pos, sub_nonneg, dite, Eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 101 more

    155 instances, coercions and auxiliary constants left out.

    Tactic trace: 70 steps

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

  9. problem Usa2026P1.usa2026_p1 line 383 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, And, Real, Usa2026P1.f, Usa2026P1.solution_value, Exists, Eq

    Proof uses: And.intro, HSub.hSub, Int.fract, LT.lt, Iff.mpr, sub_pos, HAdd.hAdd, Int.fract_lt_one, sub_le_self, Int.fract_nonneg, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Mathlib.Tactic.Ring.Common.sub_congr, Int.rawCast, Int.negOfNat and 95 more

    151 instances, coercions and auxiliary constants left out.

    Tactic trace: 52 steps

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