Compfiles/Imo1991P6.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1991, Problem 6

An infinite sequence x₀,x₁,x₂,... of real numbers is said to be bounded if there is a constant C such that |xᵢ| ≤ C for every i ≥ 0.

Given any real number a > 1, construct a bounded infinite sequence x₀,x₁,x₂,... such that

|xᵢ - xⱼ|⬝|i - j|ᵃ ≥ 1

for every pair of distinct nonnegative integers i, j.

Imports (2)
Imported by 1 file
  1. abbrev Imo1991P6.Bounded line 33 source

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

    Statement uses: Nat, Real

    Proof uses: Exists, LE.le, abs

    3 instances, coercions and auxiliary constants left out.

  2. theorem Imo1991P6.fract_sqrt_two_mul_gt line 42 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Real, HDiv.hDiv, HMul.hMul, HAdd.hAdd, Real.sqrt, Int.fract

    Proof uses: Eq.mpr, id, Eq, congrArg, propext, div_lt_iff₀, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, add_pos', Real.sqrt_pos_of_pos, inferInstance, PartialOrder, Iff.mpr, Nat.cast_pos', Nat.cast_one and 119 more

    192 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

  3. theorem Imo1991P6.Int.fract_sub_eq line 75 source

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

    Statement uses: Ring, LinearOrder, FloorRing, IsStrictOrderedRing, AddLeftMono, Exists, Fin, OfNat.ofNat, Nat, Eq, Int.fract, HSub.hSub, HAdd.hAdd

    Proof uses: dite, LE.le, Exists.intro, Eq.mpr, id, congrArg, Eq.trans, CharP.cast_eq_zero, add_zero, And, LT.lt, Int, propext, Int.fract_eq_iff, And.intro, sub_nonneg_of_le, sub_lt_iff_lt_add, lt_of_lt_of_le, of_eq_true, IsOrderedRing and 26 more

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

  4. theorem one_sub_fract_sqrt_two_mul_gt line 103 source
  5. theorem abs_fract_sqrt_two_mul_sub_fract_sqrt_two_mul line 126 source
  6. determine solution line 147 source
  7. problem imo1991_p6 line 151 source