Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2003P5

module

public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.EuclideanDomain.Basic
public import Mathlib.Algebra.EuclideanDomain.Field
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas
public import Mathlib.Tactic.Linarith

public section


/-!
# International Mathematical Olympiad 2003, Problem 5

Given n > 2 and reals x₁ ≤ x₂ ≤ ... ≤ xₙ, show that

  (∑ᵢⱼ |xᵢ - xⱼ|)² ≤ (2/3)(n² - 1) ∑ᵢⱼ (xᵢ - xⱼ)².

Show that we have equality iff the sequence is an arithmetic progression.
-/

namespace Imo2003P5

open Finset

theorem imo2003_p5 (n : ℕ) (hn : 2 < n) (x : ℕ → ℝ) (hx : MonotoneOn x (range n)) :
    (∑ i ∈ range n, ∑ j ∈ range n, |x i - x j|) ^ 2 ≤
      2 / 3 * ((n : ℝ) ^ 2 - 1) * ∑ i ∈ range n, ∑ j ∈ range n, (x i - x j) ^ 2 := sorry

/-- The equality case: equality holds iff the sequence is an arithmetic progression.

For the forward direction, with `y i = x i - m` (so `∑ y = 0`) the equality rewrites as
`(∑ cᵢ yᵢ)² = (∑ cᵢ²)(∑ yᵢ²)` with `cᵢ = 2i + 1 - n`, i.e. equality in Cauchy-Schwarz.
With `t = (∑ cᵢ yᵢ)/(∑ cᵢ²)` we get `∑ (t cᵢ - yᵢ)² = 0`, hence `yᵢ = t cᵢ` for all `i`,
which says exactly that the `xᵢ` form an arithmetic progression. -/
theorem imo2003_p5_equality (n : ℕ) (hn : 2 < n) (x : ℕ → ℝ) (hx : MonotoneOn x (range n)) :
    (∑ i ∈ range n, ∑ j ∈ range n, |x i - x j|) ^ 2 =
      2 / 3 * ((n : ℝ) ^ 2 - 1) * ∑ i ∈ range n, ∑ j ∈ range n, (x i - x j) ^ 2 ↔
    ∃ a d : ℝ, ∀ i ∈ range n, x i = a + d * (i : ℝ) := sorry

end Imo2003P5

File author(s): Kimi K3

This problem has a complete formalized solution.