Compfiles/Imo1995P4.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1995, Problem 4

The positive real numbers $x_0, x_1, x_2,.....x_{1994}, x_{1995}$ satisfy the relations $x_0=x_{1995}$ and $x_{i-1}+\frac{2}{x_{i-1}}=2{x_i}+\frac{1}{x_i}$ for $i=1,2,3,....1995$ Find the maximum value that $x_0$ can have.

Imports (2)
Imported by 1 file
  1. lemma Imo1995P4.aux₁ line 30 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Iff, Eq, HAdd.hAdd, HDiv.hDiv, Nat, HMul.hMul, Or

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma Imo1995P4.aux₂ line 34 source

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

    Statement uses: Nat, Real, LE.le, OfNat.ofNat, LT.lt, And, Eq, HAdd.hAdd, HSub.hSub, HDiv.hDiv, HMul.hMul, Or, Exists, Int, Dvd.dvd, Neg.neg, HPow.hPow

    Proof uses: Nat.le_induction, of_eq_true, Eq.trans, True, congr, congrArg, eq_true, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Mathlib.Meta.NormNum.isNat_le_true, Bool.true, and_self, True.intro, Eq.mp, propext, Imo1995P4.aux₁, congrFun' and 109 more

    187 instances, coercions and auxiliary constants left out.

    Tactic trace: 87 steps

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

  3. theorem Imo1995P4.generalized line 95 source

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

    Statement uses: Nat, Not, Dvd.dvd, OfNat.ofNat, IsGreatest, Real, Set.ofPred, Exists, And, Eq, LT.lt, LE.le, HAdd.hAdd, HSub.hSub, HDiv.hDiv, HMul.hMul, HPow.hPow

    Proof uses: And.intro, Membership.mem, Set, upperBounds, Exists.intro, ite, Eq.mpr, id, Eq.trans, True, congr, congrArg, congrFun', ite_self, CharP.cast_eq_zero, sub_zero, eq_self, forall_congr, Nat.cast_ite, ite_congr and 142 more

    190 instances, coercions and auxiliary constants left out.

    Tactic trace: 68 steps

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

  4. determine Imo1995P4.solution line 143 source

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

    Statement uses: Real

    Proof uses: HPow.hPow, Nat, OfNat.ofNat

    8 instances, coercions and auxiliary constants left out.

  5. problem Imo1995P4.imo1995_p4 line 145 source

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

    Statement uses: IsGreatest, Real, Set.ofPred, Exists, Nat, And, Eq, OfNat.ofNat, LT.lt, LE.le, HAdd.hAdd, HSub.hSub, HDiv.hDiv, HMul.hMul, Imo1995P4.solution

    Proof uses: HPow.hPow, of_eq_true, Eq.trans, True, congrArg, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Inv.inv, Mathlib.Meta.NormNum.isNNRat_mul, Eq.refl, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_sub, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one and 12 more

    75 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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