Compfiles/Imo2007P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2007, Problem 1

Real numbers a₁, a₂, ..., aₙ are fixed. For each 1 ≤ i ≤ n, we let dᵢ = max {aⱼ : 1 ≤ j ≤ i} - min {aⱼ : i ≤ j ≤ n}, and let d = max {dᵢ : 1 ≤ i ≤ n}.

(a) Prove that for any real numbers x₁ ≤ ... ≤ xₙ, we have max { |xᵢ - aᵢ| : 1 ≤ i ≤ n } ≥ d / 2.

(b) Show that there exists some choice of x₁ ≤ ... ≤ xₙ which achieves equality.

Imports (2)
Imported by 1 file
  1. abbrev Imo2007P1.d line 32 source

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

    Statement uses: Nat, Fin, Real

    Proof uses: HSub.hSub, iSup, Subtype, LE.le, iInf

    6 instances, coercions and auxiliary constants left out.

  2. problem Imo2007P1.imo2007_p1a line 35 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Real, Monotone, LE.le, HDiv.hDiv, iSup, Imo2007P1.d, abs, HSub.hSub

    Proof uses: Exists, Eq, Nonempty, Iff.mp, Fin.pos_iff_nonempty, exists_eq_ciSup_of_finite, Eq.mpr, id, congrArg, Eq.symm, Subtype, iInf, Imo2007P1.d.eq_1, propext, nonempty_subtype, Exists.intro, le_refl, exists_eq_ciInf_of_finite, le_of_not_gt, Trans.trans and 59 more

    146 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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

  3. problem Imo2007P1.imo2007_p1b line 73 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Real, Exists, And, Monotone, Eq, HDiv.hDiv, iSup, Imo2007P1.d, abs, HSub.hSub

    Proof uses: Nonempty, Iff.mp, Fin.pos_iff_nonempty, Eq.mpr, id, congrArg, rfl, Subtype, LE.le, Exists.intro, sub_le_sub_right, propext, nonempty_subtype, le_refl, ciSup_le_iff, Finite.bddAbove_range, Finite.le_ciSup, Subtype.mk, le_trans, Subtype.prop and 66 more

    154 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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