Compfiles/Imo1975P1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1975, Problem 1

Let x₁, x₂, ... , xₙ and y₁, y₂, ... , yₙ be two sequences of real numbers, such that x₁ ≥ x₂ ≥ ... ≥ xₙ and y₁ ≥ y₂ ≥ ... ≥ yₙ. Prove that if z₁, z₂, ... , zₙ is any permutation of y₁, y₂, ... , yₙ, then ∑ (xᵢ - yᵢ)^2 ≤ ∑ (xᵢ - zᵢ)^2

Imports (5)
Imported by 1 file
  1. problem Imo1975P1.imo1975_p1 line 37 source

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

    Statement uses: Nat, Equiv.Perm, Real, AntitoneOn, Finset, Finset.Icc, OfNat.ofNat, LE.le, Set, Set.ofPred, Ne, Finset.sum, HPow.hPow, HSub.hSub

    Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, id, Eq, congr, congrArg, Eq.trans, Finset.sum_congr, Eq.refl, Membership.mem, sub_sq, Finset.sum_add_distrib, congrFun', Finset.sum_sub_distrib, Eq.symm, Equiv.Perm.sum_comp, propext, add_le_add_iff_right, Function.swap and 6 more

    116 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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