Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Definition 3

Given an edge colouring, we write \(N_i(u)\) to denote the neighbourhood of vertex \(u\) in colour \(i\).

LaTeX Lean

Definition 6

Define \(\cosh \sqrt{x}\) via its Taylor expansion

\[ \cosh \sqrt{x} = \sum _{n = 0}^\infty \frac{x^n}{(2n)!}. \]

LaTeX Lean

Definition 2

An edge colouring of a graph \(G\) with colours \(C\) is a map from the edge set \(E(G)\) to \(C\).

LaTeX Lean

Definition 10

Let \(r \in \mathbb {N}\).

\begin{equation} \label{eq:f} f(x_1,\dots ,x_r) = \sum _{j = 1}^r x_j \prod _{i \ne j} \big( 2 + \cosh \sqrt{x_i} \big). \end{equation}

LaTeX Lean

Definition 4

Let \(r, n\in \mathbb {N}\). Given sets \(X,Y \subset V(K_n)\) and a colour \(i \in [r]\), define

\[ p_i(X,Y) = \min \bigg\{ \frac{|N_i(x) \cap Y|}{|Y|} : x \in X \bigg\} , \]

LaTeX Lean

Lemma 20Lemma 4.3 in Balister et al.

If \(t \ge \lambda _0\) and \(\delta \le 1/4\), then

\[ |\mathcal{B}_i(s)| \le \frac{4 \log (1/\delta )}{\lambda _0} \cdot t \]

for every \(i \in [r]\) and \(s \in \mathbb {N}\).

LaTeX

Lemma 9

\(-1 \le \cosh \sqrt{x} \le 1\) for every \(x {\lt} 0\).

LaTeX Lean

Lemma 8

\(x \le 2 + \cosh \sqrt{x} \le 3 e^{\sqrt{x}}\) for every \(x {\gt} 0\).

LaTeX Lean

Lemma 25Lemma 5.2 in Balister et al.

Given \(n,r \in \mathbb {N}\) and \(\varepsilon {\gt} 0\), and an \(r\)-colouring of \(E(K_n)\), the following holds. There exist disjoint sets of vertices \(S_1,\dots ,S_r\) and \(W\) such that, for every \(i \in [r]\),

\[ |W| \ge \bigg( \frac{1+\varepsilon }{r} \bigg)^{\sum _{j = 1}^r |S_j|} n \qquad \text{and} \qquad |N_i(w) \cap W| \ge \bigg( \frac{1}{r} - \varepsilon \bigg) |W| - 1 \]

for every \(w \in W\), and \((S_i,W)\) is a monochromatic book in colour \(i\).

LaTeX

Lemma 15Geometric lemma (Lemma 3.1 in Balister et al.)

Let \(r, n\in \mathbb {N}\). Set \(\beta = 3^{-4r}\) and \(C = 4r^{3/2}\).

Let \(U\) and \(U'\) be i.i.d. random variables taking values in a finite set \(X\), and let \(\sigma _1,\ldots ,\sigma _r \colon X \rightarrow \mathbb {R}^n\) be arbitrary functions. There exists \(\lambda \ge -1\) and \(i\in [r]\) such that

\[ \mathbb {P}\Big( \big\langle \sigma _i(U),\sigma _i(U') \big\rangle \ge \lambda \, \text{ and } \, \big\langle \sigma _j(U), \sigma _j(U') \big\rangle \ge -1 \, \text{ for all } \, j \ne i \Big) \ge \beta e^{- C\sqrt{\lambda + 1}}. \]

LaTeX Lean

Lemma 16Key lemma (Lemma 2.2 in Balister et al.)

Let \(r, n\in \mathbb {N}\). Set \(\beta = 3^{-4r}\) and \(C = 4r^{3/2}\).

Let \(\chi \) be an \(r\)-colouring of \(E(K_n)\), let \(X,Y_1,\ldots ,Y_r \subset V(K_n)\) be non-empty sets of vertices, and let \(\alpha _1,\ldots ,\alpha _r {\gt} 0\). There exists a vertex \(x \in X\), a colour \(\ell \in [r]\), sets \(X' \subset X\) and \(Y'_1,\ldots ,Y'_r\, \) with \(Y'_i \subset N_i(x) \cap Y_i\, \) for each \(i \in [r]\), and \(\lambda \ge -1\), such that

\begin{equation} \label{eq:key:ell} \beta e^{- C \sqrt{\lambda + 1}} |X| \le |X'| \qquad \text{and} \qquad p_\ell (X,Y_\ell ) + \lambda \alpha _\ell \le p_\ell ( X', Y'_\ell ) , \end{equation}

and moreover

\begin{equation} \label{eq:key:alli} |Y'_i| = p_i(X,Y_i) |Y_i| \qquad \text{and} \qquad p_i(X,Y_i) - \alpha _i \le p_i( X', Y'_i ) \end{equation}

for every \(i \in [r]\).

LaTeX Lean

Lemma 7

For all \(x \in \mathbb {R}\), it is \(1 \le 2 + \cosh \sqrt{x}\).

LaTeX Lean

Lemma 26Lemma 5.3 in Balister et al.

Let \(k,r \ge 2\) and \(\varepsilon \in (0,1)\). We have

\[ R_r\big( k - s_1, \ldots , k - s_r \big) \le e^{-\varepsilon ^3 k / 2} \bigg( \frac{1+\varepsilon }{r} \bigg)^s r^{rk} \]

for every \(s_1,\ldots ,s_r \in [k]\) with \(s = s_1 + \cdots + s_r \ge \varepsilon ^2 k\).

LaTeX

Lemma 12Moments Lemma (Lemma 3.2 in Balister et al.)

Let \(U\) and \(U'\) be i.i.d. random variables taking values in a finite set \(X\), and let \(\sigma _1,\ldots ,\sigma _r \colon X \rightarrow \mathbb {R}^n\) be arbitrary functions. Then

\[ \mathbb {E}\Big[ \big\langle \sigma _1(U),\sigma _1(U') \big\rangle ^{\ell _1} \cdots \big\langle \sigma _r(U),\sigma _r(U') \big\rangle ^{\ell _r} \Big] \ge 0. \]

for every \((\ell _1,\dots ,\ell _r) \in \mathbb {Z}^r\) with \(\ell _1,\dots ,\ell _r \ge 0\).

LaTeX Lean

Lemma 5Lemma A.1 in Balister et al.

For each \(k,t,r \in \mathbb {N}\) with \(3 \le t \le k\), we have

\[ \binom {rk-t}{k,\dots ,k,k-t} \le e^{-(r-1)t^2/3rk} r^{rk-t}. \]

LaTeX

Lemma 18Lemma 4.1 in Balister et al.

For each \(i \in [r]\) and \(s \in \mathbb {N}\),

\begin{equation} \label{eq:pi:lower:bound} p_i(s) - p_0 + \delta \, \ge \, \delta \cdot \bigg( 1 - \frac{1}{t} \bigg)^{t} \prod _{j \in \mathcal{B}_i(s)} \bigg( 1 + \frac{\lambda (j)}{t} \bigg). \end{equation}

LaTeX

Lemma 19Lemma 4.2 in Balister et al.

If \(t \ge 2\), then

\[ p_i(s) \, \ge \, p_0 - \frac{3\delta }{4} \qquad \text{and} \qquad \alpha _i(s) \, \ge \, \frac{\delta }{4t} \]

for every \(i \in [r]\) and \(s \in \mathbb {N}\).

LaTeX

Lemma 13Special-function lemma (Part 1 of Lemma 3.3 in Balister et al.)

Let \(r \in \mathbb {N}\). If \(x_i \ge - 3r\) for all \(i \in [r]\), the function \(f \colon \mathbb {R}^r \rightarrow \mathbb {R}\) defined in 1 satisfies

\[ f(x_1,\dots ,x_r) \le 3^r r \exp \bigg( \displaystyle \sum _{i = 1}^r \sqrt{ x_i + 3r } \bigg) \]

LaTeX Lean

Lemma 14Special-function lemma (Part 2 of Lemma 3.3 in Balister et al.)

Let \(r \in \mathbb {N}\). If there exists an \(i \in [r]\) with \(x_i \le - 3r\), the function \(f \colon \mathbb {R}^r \rightarrow \mathbb {R}\) defined in 1 satisfies

\[ f(x_1,\dots ,x_r) \le -1 \]

LaTeX Lean

Lemma 23Lemma 4.6 in Balister et al.

If \(t \ge \lambda _0 / \delta {\gt} 0\) and \(\delta \le 1/4\), then

\[ \sum _{j \in \mathcal{B}(s)} \sqrt{\lambda (j)} \le \frac{7r \log (1/\delta )}{\sqrt{\lambda _0}} \cdot t \]

for every \(s \in \mathbb {N}\).

LaTeX

Lemma 11

All of the coefficients of the Taylor expansion of \(f\) are non-negative.

LaTeX

Lemma 22Lemma 4.5 in Balister et al.

For each \(s \in \mathbb {N}\),

\begin{equation} \label{eq:X:lower:bound} |X(s)| \ge \varepsilon ^{rt + |\mathcal{B}(s)|} \exp \bigg( - C \sum _{j \in \mathcal{B}(s)} \sqrt{\lambda (j)+1}\, \, \bigg) |X(0)| - rt. \end{equation}

LaTeX

Lemma 21Lemma 4.4 in Balister et al.

If \(t \ge 2\), then

\[ |Y_i(s)| \ge \bigg( p_0 - \frac{3\delta }{4} \bigg)^{t + |\mathcal{B}_i(s)|} |Y_i(0)| \]

for every \(i \in [r]\) and \(s \in \mathbb {N}\).

LaTeX

Theorem 24

Let \(\chi \) be an \(r\)-colouring of \(E(K_n)\), and let \(X,Y_1,\ldots ,Y_r \subset V(K_n)\). For every \(p {\gt} 0\) and \(\mu \ge 2^{10} r^3\), and every \(t,m \in \mathbb {N}\) with \(t \ge \mu ^5 / p\), the following holds. If

\[ |N_i(x) \cap Y_i| \ge p|Y_i| \]

for every \(x \in X\) and \(i \in [r]\), and moreover

\[ |X| \ge \bigg( \frac{\mu ^2}{p} \bigg)^{\mu r t} \qquad \text{and} \qquad |Y_i| \ge \bigg( \frac{e^{2^{13} r^3 / \mu ^2}}{p} \bigg)^t \, m, \]

then \(\chi \) contains a monochromatic \((t,m)\)-book.

LaTeX

Theorem 1

For each \(r \ge 2\), there exists \(\delta = \delta (r) {\gt} 0\) such that

\begin{equation*} R_r(k) \le e^{-\delta k} r^{rk} \end{equation*}

for all sufficiently large \(k \in \mathbb {N}\).

LaTeX

Theorem 27Theorem 5.1 in Balister et al.

Let \(r \ge 2\), and set \(\delta = 2^{-160} r^{-12}\). Then

\begin{equation*} R_r(k) \le e^{-\delta k} r^{rk} \end{equation*}

for every \(k \in \mathbb {N}\) with \(k \ge 2^{160} r^{16}\).

LaTeX