Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2003P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Tactic.NormNum.Ineq

public section


/-!
# USA Mathematical Olympiad 2003, Problem 3

Let n be a positive integer. For every sequence of integers
A = (a₀, a₁, a₂, . . . , aₙ) satisfying 0 ≤ aᵢ ≤ i, for i = 0, . . . , n,
we define another sequence t(A) = (t(a₀), t(a₁), t(a₂), . . . , t(aₙ))
by setting t(aᵢ) to be the number of terms in the sequence A that precede
the term aᵢ and are different from aᵢ. Show that, starting from any
sequence A as above, fewer than n applications of the transformation t
lead to a sequence B such that t(B) = B.
-/

namespace Usa2003P3

/-- The transformation `t`: `t a i` is the number of terms of `a` that precede
the `i`-th term and are different from it.

We model the sequence `A = (a₀, a₁, …, aₙ)` as a function `ℕ → ℕ` where only the
values at `0, 1, …, n` are constrained.  The problem prescribes integer values,
but the constraint `0 ≤ aᵢ` allows us to work with natural numbers throughout. -/
def t (a : ℕ → ℕ) : ℕ → ℕ :=
  fun i => ((Finset.range i).filter (fun j => a j ≠ a i)).card

/-- ## USA Mathematical Olympiad 2003, Problem 3 -/
theorem usa2003_p3 (n : ℕ) (hn : 0 < n) (a : ℕ → ℕ) (ha : ∀ i ≤ n, a i ≤ i) :
    ∃ k, k < n ∧ ∀ i ≤ n, t^[k] a i = t^[k+1] a i := sorry

end Usa2003P3

File author(s): Kimi K3

This problem has a complete formalized solution.