Tournaments and score sequences

DefinitionTournament#✓fully proved

A tournament on the players \(1, \dots, n\) is a binary relation \(T\), where \(T(i, j)\) means that \(i\) beats \(j\), such that no player beats itself and for any two distinct players \(i\) and \(j\) exactly one of \(T(i, j)\) and \(T(j, i)\) holds.

def IsTournament {n : ℕ} (T : Fin n → Fin n → Bool) :
    Prop :=
  (∀ i, T i i = false) ∧ ∀ i j, i ≠ j → T i j ≠ T j i

Used by 3

Used byMoon's count of circular triads · Moon's reducibility criterion · Landau's theorem on score sequences

DefinitionScore of a player#✓fully proved

Let \(T\) be a binary relation on the players \(1, \dots, n\), where \(T(i, j)\) means that \(i\) beats \(j\). The score of a player \(i\) is the number of players \(j\) such that \(T(i, j)\) holds, that is, the number of players that \(i\) beats.

In a tournament this is the outdegree of \(i\).

def score {n : ℕ} (T : Fin n → Fin n → Bool) (i : Fin n) :
    ℕ :=
  (Finset.univ.filter (fun j => T i j)).card

Used by 3

Used byMoon's count of circular triads · Moon's reducibility criterion · Landau's theorem on score sequences

DefinitionReducible tournament#✓fully proved

A tournament is reducible if some nonempty proper set of players loses all games against the complement.

def IsReducible {n : ℕ} (T : Fin n → Fin n → Bool) :
    Prop :=
  ∃ S : Finset (Fin n), S.Nonempty ∧ S ≠ Finset.univ ∧
    ∀ i ∈ S, ∀ j, j ∉ S → T i j = false

Used by 1

Used byMoon's reducibility criterion

DefinitionCircular triad#✓fully proved

Let \(T\) be a binary relation on the players \(1, \dots, n\), where \(T(i, j)\) means that \(i\) beats \(j\). A set \(S\) of players is a circular triad of \(T\) if \(S\) has exactly three elements and every \(i \in S\) beats exactly one \(j \in S\).

In a tournament this means that the three players form a directed \(3\)-cycle.

def IsCircularTriad {n : ℕ} (T : Fin n → Fin n → Bool)
    (S : Finset (Fin n)) : Prop :=
  S.card = 3 ∧
    ∀ i ∈ S, (S.filter (fun j => T i j)).card = 1

Used by 1

Used byMoon's count of circular triads

TheoremExponential generating function of a shifted binomial sequence#●ready to prove

For natural numbers \(a\) and \(b\), let \(g(n) = n! \binom{n-a+b}{b}\) for \(n \ge a\) and \(g(n) = 0\) for \(n < a\), and let \(A(x) = \sum_{n \ge 0} g(n) x^n / n!\) be its exponential generating function, a formal power series over \(\mathbb{Q}\). Then \((1 - x)^{b+1} A(x) = x^a\); equivalently, \(A(x) = x^a (1 - x)^{-(b+1)}\).

theorem_wanted egf_factorial_choose (a b : ℕ) :
    (1 - PowerSeries.X) ^ (b + 1) *
        PowerSeries.mk (fun n =>
          if a ≤ n then (Nat.choose (n - a + b) b : ℚ)
          else 0)
      = PowerSeries.X ^ a

Sources

• Ian R. Harris and Ryan P. A. McShane, "Counting Tournaments with a Specified Number of Circular Triads", Theorem 1.

TheoremLandau's theorem on score sequences#●ready to prove

Let \(s_1 \le s_2 \le \dots \le s_n\) be a nondecreasing sequence of natural numbers. There is a tournament on \(n\) players in which player \(i\) has score \(s_i\) for every \(i\) if and only if \(\sum_{i=1}^{k} s_i \ge \binom{k}{2}\) for every \(k\) with \(1 \le k \le n\) and \(\sum_{i=1}^{n} s_i = \binom{n}{2}\).

theorem_wanted landau_score_sequence (n : ℕ)
    (s : Fin n → ℕ)
    (hs : ∀ i j : Fin n, i ≤ j → s i ≤ s j) :
    (∃ T : Fin n → Fin n → Bool, IsTournament T ∧
      ∀ i, score T i = s i) ↔
    (∀ k : ℕ, ∀ hk : k ≤ n, 1 ≤ k →
      Nat.choose k 2 ≤
        ∑ i : Fin k, s (Fin.castLE hk i)) ∧
    (∑ i, s i) = Nat.choose n 2

Sources

• Ian R. Harris and Ryan P. A. McShane, "Counting Tournaments with a Specified Number of Circular Triads", Theorem 4.

Uses 2

Statement usesTournament · Score of a player

TheoremMoon's reducibility criterion#●ready to prove

Let \(T\) be a tournament on \(n\) players in which the score \(s_i\) of player \(i\) satisfies \(s_1 \le s_2 \le \dots \le s_n\). Then \(T\) is reducible if and only if \(\sum_{i=1}^{k} s_i = \binom{k}{2}\) for some integer \(k\) with \(1 \le k < n\).

theorem_wanted isReducible_iff (n : ℕ)
    (T : Fin n → Fin n → Bool) (s : Fin n → ℕ)
    (hT : IsTournament T)
    (hs : ∀ i j : Fin n, i ≤ j → s i ≤ s j)
    (hscore : ∀ i, score T i = s i) :
    IsReducible T ↔
      ∃ k : ℕ, ∃ hk : k ≤ n, 1 ≤ k ∧ k < n ∧
        (∑ i : Fin k, s (Fin.castLE hk i)) =
          Nat.choose k 2

Sources

• Ian R. Harris and Ryan P. A. McShane, "Counting Tournaments with a Specified Number of Circular Triads", Theorem 5.

Uses 3

Statement usesReducible tournament · Tournament · Score of a player

TheoremMoon's count of circular triads#●ready to prove

In a tournament on \(n\) players with scores \(s_1, \dots, s_n\), the number of circular triads is \(\binom{n}{3} - \sum_{i=1}^{n} \binom{s_i}{2}\).

theorem_wanted card_circularTriads (n : ℕ)
    (T : Fin n → Fin n → Bool) (hT : IsTournament T) :
    ((Finset.univ.powersetCard 3).filter
        (IsCircularTriad T)).card =
      Nat.choose n 3 - ∑ i, Nat.choose (score T i) 2

Sources

• Ian R. Harris and Ryan P. A. McShane, "Counting Tournaments with a Specified Number of Circular Triads", Theorem 6.

Uses 3

Statement usesCircular triad · Tournament · Score of a player

4 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.