Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2012P6

module

public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Analysis.Normed.Field.Basic
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2012, Problem 6

For integer n ≥ 2, let x₁, x₂, ..., xₙ be real numbers satisfying
x₁ + x₂ + ... + xₙ = 0 and x₁² + x₂² + ... + xₙ² = 1.
For each subset A ⊆ {1, 2, ..., n}, define S_A = ∑_{i ∈ A} x_i.
(If A is the empty set, then S_A = 0.)
Prove that for any positive number λ, the number of sets A satisfying
S_A ≥ λ is at most 2^(n-3)/λ². For which choices of x₁, x₂, ..., xₙ, λ
does equality hold?
-/

open Finset

namespace Usa2012P6

/-- Equality holds iff `x` is a permutation of `(1 / √2, -1 / √2, 0, ..., 0)`
and `λ = 1 / √2`. -/
/- determine -/ abbrev equality_cases {n : ℕ} (x : Fin n → ℝ) (lam : ℝ) : Prop := sorry

theorem usa2012_p6 {n : ℕ} (hn : 2 ≤ n) (x : Fin n → ℝ)
    (hsum : ∑ i, x i = 0) (hsq : ∑ i, x i ^ 2 = 1)
    (lam : ℝ) (hlam : 0 < lam) :
    ((univ.powerset.filter (fun A => lam ≤ ∑ i ∈ A, x i)).card : ℝ) ≤
      (2 : ℝ) ^ ((n : ℤ) - 3) / lam ^ 2 := sorry

theorem usa2012_p6_equality_cases {n : ℕ} (hn : 2 ≤ n) (x : Fin n → ℝ)
    (hsum : ∑ i, x i = 0) (hsq : ∑ i, x i ^ 2 = 1)
    (lam : ℝ) (hlam : 0 < lam) :
    ((univ.powerset.filter (fun A => lam ≤ ∑ i ∈ A, x i)).card : ℝ) =
        (2 : ℝ) ^ ((n : ℤ) - 3) / lam ^ 2 ↔
      equality_cases x lam := sorry

end Usa2012P6

File author(s): Kimi K3

This problem has a complete formalized solution.