Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1987P5

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Order.Chebyshev
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Nat.Choose.Cast
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1987, Problem 5

a₁, a₂, ... , aₙ is a sequence of 0s and 1s. T is the number of triples
(aᵢ, aⱼ, aₖ) with i < j < k which are not equal to (0, 1, 0) or (1, 0, 1).
For 1 ≤ i ≤ n, f(i) is the number of j < i with aⱼ = aᵢ plus the number of
j > i with aⱼ ≠ aᵢ. Show that
T = f(1)(f(1) - 1)/2 + f(2)(f(2) - 1)/2 + ... + f(n)(f(n) - 1)/2.
If n is odd, what is the smallest value of T?
-/

namespace Usa1987P5

variable {n : ℕ}

/-- The set of positions `j < i` with `a j = a i`. -/
def eqBefore (a : Fin n → Bool) (i : Fin n) : Finset (Fin n) :=
  Finset.univ.filter fun j ↦ j < i ∧ a j = a i

/-- The set of positions `j > i` with `a j ≠ a i`. -/
def neqAfter (a : Fin n → Bool) (i : Fin n) : Finset (Fin n) :=
  Finset.univ.filter fun j ↦ i < j ∧ a j ≠ a i

/-- The quantity `f(i)` from the problem statement. -/
def f (a : Fin n → Bool) (i : Fin n) : ℕ := (eqBefore a i).card + (neqAfter a i).card

/-- The quantity `T` from the problem statement: the number of triples of
indices `i < j < k` whose values are not `(0, 1, 0)` or `(1, 0, 1)`. -/
def numGoodTriples (a : Fin n → Bool) : ℕ :=
  (Finset.univ.filter fun t : Fin n × Fin n × Fin n ↦
    t.1 < t.2.1 ∧ t.2.1 < t.2.2 ∧
      ¬ ((a t.1 = false ∧ a t.2.1 = true ∧ a t.2.2 = false) ∨
         (a t.1 = true ∧ a t.2.1 = false ∧ a t.2.2 = true))).card

/-- The alternating sequence `0, 1, 0, 1, ...`. -/
def altSeq (n : ℕ) : Fin n → Bool := fun i ↦ (i : ℕ) % 2 == 1

/- determine -/ abbrev minT : ℕ → ℕ := sorry

theorem usa1987_p5_part1 (a : Fin n → Bool) :
    numGoodTriples a = ∑ i : Fin n, (f a i).choose 2 := sorry

theorem usa1987_p5_part2 (hn : Odd n) :
    IsLeast (Set.range fun a : Fin n → Bool ↦ numGoodTriples a) (minT n) := sorry

end Usa1987P5

File author(s): Kimi K3

This problem has a complete formalized solution.