mathlib3 documentation

mathlib-archive / imo.imo1975_q1

IMO 1975 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Solution #

Firstly, we expand the squares withing both sums and distribute into separate finite sums. Then, noting that ∑ yᵢ ^ 2 = ∑ zᵢ ^ 2, it remains to prove that ∑ xᵢ * zᵢ ≤ ∑ xᵢ * yᵢ, which is true by the Rearrangement Inequality

theorem imo1975_q1 (n : ℕ) (σ : equiv.perm ℕ) (hσ : {x : ℕ | ⇑σ x ≠ x} ⊆ ↑(finset.Icc 1 n)) (x y : ℕ → ℝ) (hx : antitone_on x ↑(finset.Icc 1 n)) (hy : antitone_on y ↑(finset.Icc 1 n)) :
(finset.Icc 1 n).sum (λ (i : ℕ), (x i - y i) ^ 2) ≤ (finset.Icc 1 n).sum (λ (i : ℕ), (x i - y (⇑σ i)) ^ 2)