Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2020P6

module

public import Mathlib.Algebra.BigOperators.Fin
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Fintype.Perm

public section


/-!
# USA Mathematical Olympiad 2020 Problem 6

Let n ≥ 2 be an integer. Let x₁ ≥ x₂ ≥ ⋯ ≥ xₙ and y₁ ≥ y₂ ≥ ⋯ ≥ yₙ be 2n real
numbers such that

0 = x₁ + x₂ + ⋯ + xₙ = y₁ + y₂ + ⋯ + yₙ,

and

1 = x₁² + x₂² + ⋯ + xₙ² = y₁² + y₂² + ⋯ + yₙ².

Prove that

∑_{i=1}^{n} (xᵢyᵢ − xᵢyₙ₊₁₋ᵢ) ≥ 2/√(n−1).
-/

namespace Usa2020P6

open Finset Nat

/-- USA Mathematical Olympiad 2020, Problem 6. -/
theorem usa2020_p6 {n : ℕ} (hn : 2 ≤ n) (x y : Fin n → ℝ)
    (hx : Antitone x) (hy : Antitone y)
    (hxs : ∑ i, x i = 0) (hys : ∑ i, y i = 0)
    (hx2 : ∑ i, x i ^ 2 = 1) (hy2 : ∑ i, y i ^ 2 = 1) :
    ∑ i, (x i * y i - x i * y (Fin.rev i)) ≥ 2 / Real.sqrt ((n : ℝ) - 1) := sorry

end Usa2020P6

File author(s): Kimi K3

This problem has a complete formalized solution.