Compfiles/Imo2013P5.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2013, Problem 5

Let ℚ>₀ be the set of positive rational numbers. Let f: ℚ>₀ → ℝ be a function satisfying the conditions

(1) f(x) * f(y) ≥ f(x * y) (2) f(x + y) ≥ f(x) + f(y)

for all x,y ∈ ℚ>₀. Given that f(a) = a for some rational a > 1, prove that f(x) = x for all x ∈ ℚ>₀.

Imports (2)
Imported by 1 file
  1. lemma Imo2013P5.le_of_all_pow_lt_succ line 42 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Nat, HSub.hSub, HPow.hPow, LE.le

    Proof uses: Decidable.byContradiction, Not, Max.max, lt_max_of_lt_right, zero_lt_one, HDiv.hDiv, Exists, False, pow_unbounded_of_one_lt, Iff.mpr, one_lt_div, max_lt, Eq.mp, Nat.pos_of_ne_zero, Eq, False.elim, Eq.trans, congrArg, pow_zero, eq_false and 76 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  2. lemma Imo2013P5.f_pos_of_pos line 58 source

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

    Statement uses: Rat, Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, Nat

    Proof uses: Rat.num, Rat.den, Trans.trans, Eq, Eq.mpr, id, congrArg, Eq.symm, Rat.mul_den_eq_num, Eq.refl, Iff.mpr, Nat.cast_pos, Rat.pos, Int, Rat.num_pos, Int.natAbs, Int.natAbs_of_nonneg, LT.lt.le, Ne, Int.natAbs_pos and 9 more

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  3. lemma Imo2013P5.fx_gt_xm1 line 77 source

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

    Statement uses: Rat, Real, LE.le, OfNat.ofNat, LT.lt, HMul.hMul, HAdd.hAdd, Nat, HSub.hSub

    Proof uses: Nat.floor, Trans.trans, cast, Eq.trans, congrFun', congrArg, Eq.symm, Nat.cast_one, Rat.cast_one, Nat.sub_one_lt_floor, Iff.mpr, Nat.floor_pos, Eq, Or, LE.le.eq_or_lt, Nat.floor_le, LE.le.trans, zero_le_one, Eq.mp, lt_add_of_pos_left and 7 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  4. lemma Imo2013P5.pow_f_le_f_pow line 95 source

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

    Statement uses: Rat, Real, Nat, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, HPow.hPow

    Proof uses: LT.lt.trans, zero_lt_one, Nat.le_induction, Nat.succ, of_eq_true, Eq.trans, True, congr, congrArg, zero_add, pow_one, Eq.mpr, HAdd.hAdd, id, Eq, pow_succ, Trans.trans, pow_pos, mul_le_mul_of_nonneg_right, LT.lt.le and 1 more

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  5. lemma Imo2013P5.fixed_point_of_pos_nat_pow line 108 source

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

    Statement uses: Rat, Real, Nat, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, Eq, HPow.hPow

    Proof uses: cast, Eq.symm, congrFun', congrArg, one_lt_pow₀, LT.lt.ne', Trans.trans, Imo2013P5.pow_f_le_f_pow, Eq.mpr, id, Eq.refl, Eq.trans, LE.le.antisymm

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  6. lemma Imo2013P5.fixed_point_of_gt_1 line 121 source

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

    Statement uses: Rat, Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, HAdd.hAdd, Nat, Eq

    Proof uses: HPow.hPow, Exists, pow_unbounded_of_one_lt, HSub.hSub, Iff.mpr, lt_sub_iff_add_lt, Trans.trans, add_le_add_left, add_le_add_right, LT.lt.trans, zero_lt_one, Nat.pos_of_ne_zero, False, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 77 more

    155 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  7. problem Imo2013P5.imo2013_p5 line 149 source

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

    Statement uses: Rat, Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, HAdd.hAdd, Exists, And, Eq

    Proof uses: Nat, Nat.le_induction, Nat.succ, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', zero_add, Nat.cast_one, one_mul, Eq.mpr, id, Nat.cast_add, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 77 more

    154 instances, coercions and auxiliary constants left out.

    Tactic trace: 53 steps

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