Compfiles/Imo1973P6.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1973, Problem 6

Let $a_1, a_2,\cdots, a_n$ be $n$ positive numbers, and let $q$ be a given real number such that $0 < q < 1$. Find $n$ numbers $b_1, b_2, \cdots, b_n$ for which

(a) $a_k < b_k$ for $k=1,2,\cdots, n$,

(b) $q < \dfrac{b_{k+1}}{b_k}<\dfrac{1}{q}$ for $k=1,2,\cdots,n-1$,

(c) $b_1+b_2+\cdots+b_n < \dfrac{1+q}{1-q}(a_1+a_2+\cdots+a_n)$.

Imports (2)
Imported by 1 file
  1. def Imo1973P6.m line 40 source

    no axioms what this means

    Statement uses: Nat

  2. theorem Imo1973P6.m_zero line 42 source

    no axioms what this means

    Statement uses: Nat, Eq, Imo1973P6.m, OfNat.ofNat

    Proof uses: Eq.refl

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem Imo1973P6.m_nonzero line 45 source

    no axioms what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1973P6.m

    4 instances, coercions and auxiliary constants left out.

  4. def Imo1973P6.Q line 48 source

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

    Statement uses: Nat, Real, Fin

    Proof uses: HPow.hPow, Imo1973P6.m, Int.natAbs, HSub.hSub, Int

    9 instances, coercions and auxiliary constants left out.

  5. theorem Imo1973P6.Q_diag_one line 50 source

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

    Statement uses: Nat, Real, Fin, Eq, Imo1973P6.Q, OfNat.ofNat

    Proof uses: id, of_eq_true, HPow.hPow, Imo1973P6.m, Int.natAbs, HSub.hSub, Int, Eq.trans, True, forall_congr, congrFun', congrArg, sub_self, Imo1973P6.m_zero, pow_zero, eq_self, implies_true

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  6. theorem Imo1973P6.Q_pos line 54 source

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

    Statement uses: Nat, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Fin, LT.lt, Imo1973P6.Q

    Proof uses: id, pow_pos, Imo1973P6.m, Int.natAbs, HSub.hSub, Int

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  7. theorem Imo1973P6.Q_row_neighbour_quot line 60 source

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

    Statement uses: Nat, Real, LT.lt, HAdd.hAdd, OfNat.ofNat, Fin, Membership.mem, Set, Set.Ioo, Exists, And, Finset, Insert.insert, Singleton.singleton, Inv.inv, Eq, Imo1973P6.Q, Fin.mk, HMul.hMul

    Proof uses: Eq.mpr, Or, id, Eq.trans, congrArg, funext, congrFun', propext, Iff.intro, Exists.elim, And.elim, And.intro, rfl, Eq.symm, Exists.intro, True, eq_self, true_and, HPow.hPow, Imo1973P6.m and 19 more

    97 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

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

  8. theorem Imo1973P6.imo1973_p6_of_n_eq_one line 75 source

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

    Statement uses: Nat, Fin, Real, Eq, OfNat.ofNat, Membership.mem, Set, Set.Ioo, LT.lt, Exists, And, HSub.hSub, HDiv.hDiv, Fin.mk, HAdd.hAdd, Finset.sum, Finset.univ, HMul.hMul

    Proof uses: Eq.rec, Eq.symm, Eq.mpr, Eq.refl, id, congrArg, funext, congr, Eq.trans, True, forall_congr, False, Eq.substr, tsub_self, Inv.inv, forall_prop_domain_congr, congrFun', one_div, implies_true, Singleton.singleton and 93 more

    151 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  9. problem Imo1973P6.imo1973_p6 line 98 source

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

    Statement uses: Nat, Fin, Real, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Exists, And, HSub.hSub, HDiv.hDiv, Fin.mk, HAdd.hAdd, Finset.sum, Finset.univ, HMul.hMul

    Proof uses: dite, Eq, Imo1973P6.imo1973_p6_of_n_eq_one, Not, Exists.intro, Matrix.mulVec, Equiv, Matrix, Matrix.of, Imo1973P6.Q, Nat.lt_of_le_of_ne, Ne.symm, NeZero, NeZero.of_gt, Eq.mpr, id, congrArg, propext, lt_div_iff₀, lt_of_not_ge and 243 more

    324 instances, coercions and auxiliary constants left out.

    Tactic trace: 251 steps (first 200 of 251)

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