noncomputable def BoundedDiffLemma.unionBoundTerm (n t : ℕ) (p : ℝ) : ℝ

A single term in the union-bound used in Lemma 9.3.5: the expected number of vertex subsets of size $t$ in $G(n, p)$ that contain at least $\lceil 3t/2 \rceil$ edges, bounded by $\binom{n}{t}\binom{t(t-1)/2}{3t/2} p^{3t/2}$.

noncomputable def BoundedDiffLemma.unionBoundSum (n : ℕ) (p : ℝ) (k : ℕ) : ℝ

Sum of the union-bound terms over subset sizes $t = 4, 5, \dots, k+3$.

noncomputable def BoundedDiffLemma.numTerms (C : ℝ) (n : ℕ) : ℕ

The number of subset sizes $t$ to sum over in the union bound: $\lfloor C\sqrt{n} \rfloor - 3$.

noncomputable def BoundedDiffLemma.gnpNon3ColorableSmallSubsetProb (n : ℕ) (p C : ℝ) : ℝ

The probability that the random graph $G(n,p)$ contains a non-3-colorable subset of size at most $C\sqrt{n}$.

theorem BoundedDiffLemma.unionBound_upper_bound (n : ℕ) (p C : ℝ) : gnpNon3ColorableSmallSubsetProb n p C ≤ unionBoundSum n p (numTerms C n)

The union-bound upper estimate: the probability of having a non-3-colorable subset of size $\leq C\sqrt{n}$ is bounded by the union-bound sum.

theorem BoundedDiffLemma.unionBoundSum_lt_of_large (α : ℝ) (hα : α > 5 / 6) (C : ℝ) (hC : 0 < C) (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ n ≥ N, ∀ (p : ℝ), 0 ≤ p → p ≤ (↑n).rpow (-α) → unionBoundSum n p (numTerms C n) < ε

For $\alpha > 5/6$ and $p \leq n^{-\alpha}$, the union-bound sum vanishes as $n \to \infty$: for any $\varepsilon > 0$ there exists $N$ such that for all $n \geq N$ the sum is $< \varepsilon$.

theorem BoundedDiffLemma.small_subset_three_colorable (α : ℝ) (hα : α > 5 / 6) (C : ℝ) (hC : 0 < C) (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ n ≥ N, ∀ (p : ℝ), 0 ≤ p → p ≤ (↑n).rpow (-α) → gnpNon3ColorableSmallSubsetProb n p C < ε

Lemma 9.3.5: for $\alpha > 5/6$, $p \leq n^{-\alpha}$, and large enough $n$, every subset of $\leq C\sqrt{n}$ vertices in $G(n,p)$ is 3-colorable with high probability.