structure TournamentHamiltonCycles.Tournament (n : ℕ) : Type

A tournament on $n$ vertices: an irreflexive Boolean edge relation such that exactly one of $\mathrm{edge}(i, j)$ or $\mathrm{edge}(j, i)$ is true for $i \ne j$.

• edge : Fin n → Fin n → Bool
• irrefl (i : Fin n) : self.edge i i = false
• tournament (i j : Fin n) : i ≠ j → (self.edge i j = true ↔ self.edge j i = false)

def TournamentHamiltonCycles.IsHamiltonCycle {n : ℕ} (T : Tournament n) (σ : Equiv.Perm (Fin n)) : Prop

A permutation $\sigma$ encodes a Hamilton cycle of $T$ iff every directed edge $i \to \sigma(i)$ exists in $T$ and $\sigma$ is a single $n$-cycle.

noncomputable def TournamentHamiltonCycles.Tournament.numHamiltonCycles {n : ℕ} (T : Tournament n) : ℕ

The number of Hamilton cycles of $T$, counted as cycle-permutations on $\mathrm{Fin}\, n$.

def TournamentHamiltonCycles.Tournament.outDeg {n : ℕ} (T : Tournament n) (i : Fin n) : ℕ

Out-degree of vertex $i$ in $T$: the number of $j$ with $T.\mathrm{edge}(i, j)$ true.

theorem TournamentHamiltonCycles.bregman_theorem {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : ∀ (i j : Fin n), A i j = 0 ∨ A i j = 1) (d : Fin n → ℕ) (hd : ∀ (i : Fin n), {j : Fin n | A i j = 1}.card = d i) (hd_pos : ∀ (i : Fin n), d i > 0) : A.permanent ≤ ∏ i : Fin n, ↑(d i).factorial ^ (1 / ↑(d i))

Brégman's theorem on the permanent of a $0/1$-matrix: if row $i$ has exactly $d_i$ ones, then $\mathrm{perm}(A) \le \prod_i (d_i!)^{1/d_i}$.

theorem TournamentHamiltonCycles.factorial_rpow_log_concave (m : ℕ) (hm : m ≥ 1) : ↑m.factorial ^ (1 / ↑m) * ↑(m + 2).factorial ^ (1 / ↑(m + 2)) ≥ (↑(m + 1).factorial ^ (1 / ↑(m + 1))) ^ 2

The sequence $m \mapsto (m!)^{1/m}$ is log-concave: $a_m \cdot a_{m+2} \ge a_{m+1}^2$. Used in the smoothing step of the proof of Alon's Hamilton-cycle bound.

theorem TournamentHamiltonCycles.smoothing_stirling_bound : ∃ C > 0, ∀ n ≥ 3, ∀ (d : Fin n → ℕ), (∀ (i : Fin n), d i > 0) → ∑ i : Fin n, d i = n * (n - 1) / 2 → ∏ i : Fin n, ↑(d i).factorial ^ (1 / ↑(d i)) ≤ C * √↑n * (↑n.factorial / 2 ^ n)

Smoothing + Stirling bound: for positive degrees $d_i$ summing to $\binom{n}{2}$, $\prod_i (d_i!)^{1/d_i} \le C \sqrt{n} \cdot n! / 2^n$ for some absolute constant $C$.

theorem TournamentHamiltonCycles.bregman_bound_for_tournament {n : ℕ} (T : Tournament n) (hn : n ≥ 3) : ↑T.numHamiltonCycles ≤ ∏ i : Fin n, ↑(T.outDeg i).factorial ^ (1 / ↑(T.outDeg i))

Brégman bound applied to the adjacency matrix of a tournament: the number of Hamilton cycles is bounded by $\prod_i (\mathrm{outDeg}(i)!)^{1/\mathrm{outDeg}(i)}$.

theorem TournamentHamiltonCycles.tournament_sum_outDeg {n : ℕ} (T : Tournament n) : ∑ i : Fin n, T.outDeg i = n * (n - 1) / 2

Handshake identity for tournaments: $\sum_i \mathrm{outDeg}(i) = \binom{n}{2}$.

theorem TournamentHamiltonCycles.outDeg_pos_of_numHamiltonCycles_pos {n : ℕ} (T : Tournament n) (h : T.numHamiltonCycles > 0) (i : Fin n) : T.outDeg i > 0

If $T$ contains at least one Hamilton cycle, then every vertex has positive out-degree (it has at least one outgoing edge along the cycle).

theorem TournamentHamiltonCycles.tournament_hamilton_cycles_bound : ∃ C > 0, ∀ n ≥ 3, ∀ (T : Tournament n), ↑T.numHamiltonCycles ≤ C * √↑n * (↑n.factorial / 2 ^ n)

Theorem 10.2.6 (Alon 1990 for cycles). There exists $C > 0$ such that every $n$-vertex tournament has at most $C \sqrt{n} \cdot n! / 2^n$ Hamilton cycles.