Compfiles/Imo1997P3.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1997, Problem 3

Let $x_1, x_2, \dots, x_n$ be real numbers satisfying the conditions $|x_1 + x_2 + \cdots + x_n| = 1$ and $|x_i| ≤ \frac{n+1}2$ for $i = 1, 2, \dots, n$. Show that there exists a permutation $y_1, y_2, \dots, y_n$ of $x_1, x_2, \dots, x_n$ such that $|y_1 + 2y_2 + \cdots + ny_n| ≤ \frac{n+1}2$.

Imports (5)
Imported by 1 file
  1. def Imo1997P3.S line 55 source

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

    Statement uses: Nat, Fin, Real, Equiv.Perm

    Proof uses: Finset.sum, Finset.univ, HMul.hMul, HAdd.hAdd, OfNat.ofNat

    14 instances, coercions and auxiliary constants left out.

  2. lemma Imo1997P3.sign_eq_of_abs_sub_le line 58 source

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

    Statement uses: Real, LT.lt, HDiv.hDiv, OfNat.ofNat, Nat, abs, LE.le, HSub.hSub, Eq, SignType, OrderHom, SignType.sign

    Proof uses: Or, lt_trichotomy, of_eq_true, Eq.trans, True, congr, congrArg, sign_pos, eq_self, Eq.mpr, False, id, sign_zero, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, inferInstance, AddMonoidWithOne and 84 more

    149 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  3. lemma Imo1997P3.lt_abs_add_of_sign_eq line 64 source

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

    Statement uses: Real, LT.lt, HDiv.hDiv, OfNat.ofNat, Nat, abs, Eq, SignType, OrderHom, SignType.sign, HAdd.hAdd

    Proof uses: Or, lt_trichotomy, Eq.mpr, Neg.neg, id, Eq.trans, congrArg, neg_add_rev, Or.inl, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 84 more

    155 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  4. lemma Imo1997P3.sign_eq_of_contra For fixed nonempty x, assuming the opposite of what is to be proven, the signs of S x p are all the same line 75 source

    Source documentation

    For fixed nonempty x, assuming the opposite of what is to be proven, the signs of S x p are all the same.

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

    Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Real, LE.le, abs, HDiv.hDiv, Equiv.Perm, LT.lt, Imo1997P3.S, Eq, SignType, OrderHom, SignType.sign

    Proof uses: Submonoid.induction_of_closure_eq_top_right, Set.range, Equiv.swap, Fin.castSucc, Fin.succ, Equiv.Perm.mclosure_swap_castSucc_succ, Eq.refl, Membership.mem, Set, HSub.hSub, HMul.hMul, Exists, Eq.mp, congrArg, propext, Set.mem_range, Eq.mpr, Finset.sum, Finset.univ, id and 62 more

    170 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

    lemma sign_eq_of_contra {n : ℕ}
    {x : Fin (n + 1) → ℝ} (hx₂ : ∀ i, |x i| ≤ ((n + 1 : ℕ) + 1) / 2)
    (h : ∀ (p : Equiv.Perm (Fin (n + 1))), ((n + 1 : ℕ) + 1) / 2 < |S x p|) :
    ∀ p, SignType.sign (S x 1) = SignType.sign (S x p) := fun p ↦ by
…

    Mentions: h, Imo1997P3.S

  5. lemma Imo1997P3.S_one_add_S_revPerm line 104 source

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

    Statement uses: Nat, Fin, Real, Eq, abs, Finset.sum, Finset.univ, OfNat.ofNat, HAdd.hAdd, Imo1997P3.S, Equiv.Perm, Fin.revPerm

    Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Imo1997P3.S.eq_1, Eq.symm, Equiv.Perm.sum_comp, of_eq_true, LE.le, Set, Set.ofPred, Ne, Finset, Eq.trans, Not, Fin.rev, Set.univ, True, congr, funext and 25 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  6. problem Imo1997P3.imo1997_p3 line 115 source

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

    Statement uses: Nat, Fin, Real, Eq, abs, Finset.sum, Finset.univ, OfNat.ofNat, LE.le, HDiv.hDiv, HAdd.hAdd, Exists, Equiv.Perm, HMul.hMul

    Proof uses: of_eq_true, Eq.trans, True, congrArg, funext, Inv.inv, congr, Finset.sum_congr, EmptyCollection.emptyCollection, Finset, Finset.univ_eq_empty, Membership.mem, Eq.refl, abs_zero, congrFun', CharP.cast_eq_zero, zero_add, one_div, Decidable.byContradiction, Not and 22 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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