module
public import Mathlib.Algebra.AffineMonoid.Basic
public import Mathlib.Algebra.Polynomial.Coeff
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Analysis.Normed.Ring.Lemmas
public import Mathlib.GroupTheory.Perm.Fin
public section
/-!
# USA Mathematical Olympiad 2017, Problem 2
Let $m_1, m_2, \ldots, m_n$ be a collection of $n$ positive integers, not necessarily
distinct. For any sequence of integers $A = (a_1, \ldots, a_n)$ and any permutation
$w = w_1 w_2 \cdots w_n$ of $m_1, \ldots, m_n$, define an $A$-inversion of $w$ to be a
pair of entries $w_i, w_j$ with $i < j$ for which one of the following conditions holds:
* $a_i \ge w_i > w_j$,
* $w_j > a_i \ge w_i$, or
* $w_i > w_j > a_i$.
Show that, for any two sequences of integers $A = (a_1, \ldots, a_n)$ and
$B = (b_1, \ldots, b_n)$, and for any positive integer $k$, the number of permutations of
$m_1, \ldots, m_n$ having exactly $k$ A-inversions is equal to the number of permutations
of $m_1, \ldots, m_n$ having exactly $k$ B-inversions.
-/
namespace Usa2017P2
open Finset Polynomial Equiv
/-- **USA Mathematical Olympiad 2017, Problem 2.** The number of permutations of
`m₁, …, mₙ` with exactly `k` `A`-inversions equals the number with exactly `k`
`B`-inversions. Permutations are counted with multiplicity (as positional permutations
`σ : Equiv.Perm (Fin n)`), which is equivalent to the count over distinct arrangements:
each distinct arrangement corresponds to the same positive number `∏ (multiplicity)!` of
positional permutations, independently of `A`, `B` and `k`. Note: the positivity
hypothesis `hm` is actually not needed for the conclusion. -/
theorem usa2017_p2 {n : ℕ} (m : Fin n → ℕ) (hm : ∀ i, 0 < m i) (A B : Fin n → ℤ) (k : ℕ) :
(univ.filter (fun σ : Perm (Fin n) => ainvCount (fun i => (m i : ℤ)) A σ = k)).card =
(univ.filter (fun σ : Perm (Fin n) => ainvCount (fun i => (m i : ℤ)) B σ = k)).card := sorry
end Usa2017P2
This problem has a complete formalized solution.