The discrete $\sigma$-algebra (every subset is measurable) on the finite set of simple graphs on $\{0, 1, \dots, n-1\}$.
Instances For
The Erdős–Rényi random graph measure $G(n, p)$ on simple graphs over $\{0, \dots, n-1\}$, where each edge is included independently with probability $p \in [0, 1]$.
Instances For
The Erdős–Rényi measure $G(n, p)$ is a probability measure on simple graphs.
The chromatic number $\chi(G)$ of a finite simple graph $G$ on $\{0, \dots, n-1\}$ as a
natural number (converted from the ℕ∞-valued chromatic number in Mathlib via ENat.toNat).
Instances For
The probability $\mathbb{P}_{G(n,p)}(E)$ of an event $E$ under the Erdős–Rényi measure
$G(n, p)$, returned as a real number via ENNReal.toReal.
Instances For
If $G[\bar S]$ is $u$-colourable and $G[S]$ is $3$-colourable, then $G$ itself is $(u + 3)$-colourable: combine the two colourings using disjoint palettes.
Corollary of colorable_of_induce_compl_colorable: under the same hypotheses,
$\chi(G) \le u + 3$.
Set-level lemma underlying the Shamir–Spencer concentration argument: the intersection of the three events (existence of a small "deletion set" $S$ making $G[\bar S]$ $u$-colourable, all small $S$ make $G[S]$ $3$-colourable, and $\chi(G) \ge u$) is contained in the event $\{u \le \chi(G) \le u + 3\}$.
Shamir–Spencer four-value concentration of the chromatic number. For sparse Erdős–Rényi graphs $G(n, p)$ with $p < n^{-\alpha}$ and $\alpha > 5/6$, there exists a sequence $u(n)$ such that with probability at least $1 - 3\varepsilon$, $u(n) \le \chi(G) \le u(n) + 3$ for all sufficiently large $n$. The proof combines the Azuma-type bounded-difference inequality with a $3$-colourability property of small induced subgraphs.
Definition 9.2.1 (Martingale). A sequence $(Z_n)_{n \ge 0}$ is a martingale with respect
to a filtration $(\mathcal F_n)$ and probability measure $\mu$ if each $Z_n$ is
$\mathcal F_n$-measurable, integrable, and $\mathbb{E}[Z_{n+1} \mid \mathcal F_n] = Z_n$.
This is a thin wrapper around Mathlib's MeasureTheory.Martingale.
Instances For
Helper for Azuma's inequality: the martingale-difference process $i \mapsto Z_{i+1} - Z_i$ is strongly adapted to the filtration $\mathcal F$.
Helper for Azuma's inequality: the first martingale increment $Z_1 - Z_0$ is sub-Gaussian with parameter $1$ when the increments satisfy $|Z_{i+1} - Z_i| \le 1$.
Helper for Azuma's inequality: each subsequent martingale increment $Z_{i+2} - Z_{i+1}$ is conditionally sub-Gaussian (parameter $1$) given $\mathcal F_i$.
Azuma's inequality (Theorem 9.2.7 / 9.2.8). For a martingale $(Z_n)$ with bounded increments $|Z_{i+1} - Z_i| \le 1$, the upper tail satisfies $\mathbb{P}(Z_n - Z_0 \ge t\sqrt{n}) \le \exp(-t^{2}/2)$ for every $t > 0$.
Azuma's inequality, weighted form. With increments bounded by $|Z_{i+1} - Z_i| \le c_i$ and sub-Gaussian parameters $\sigma_i = c_i^{2}$, one has $\mathbb{P}(Z_n - Z_0 \ge t) \le \exp\!\big({-t^{2} / (2\sum_i c_i^{2})}\big)$ for $t > 0$.
The Hoeffding sub-Gaussian parameter $c^{2}/4$ for a centred random variable bounded in an interval of length $c$, packaged as a non-negative real.
Instances For
Hoeffding's lemma (Lemma 9.2.12). If $X$ is a centred random variable taking values in $[a, a + \ell]$, then its moment generating function satisfies $\mathbb{E}[e^{tX}] \le \exp(t^{2} \ell^{2} / 8)$ for all $t \in \mathbb{R}$.
Azuma–Doob martingale concentration (sub-Gaussian form). For an adapted sequence $(Y_i)$ with sub-Gaussian (resp. conditionally sub-Gaussian given $\mathcal F_i$) MGFs of Hoeffding parameter $c_i^{2}/4$, the partial sum satisfies $\mathbb{P}\!\big(\sum_i Y_i \ge \varepsilon\big) \le \exp\!\big({-2\varepsilon^{2} / \sum_i c_i^{2}}\big)$ for every $\varepsilon \ge 0$.
A centred random variable supported in an interval $[a_0, a_0 + c]$ has a sub-Gaussian MGF with the Hoeffding parameter $c^{2}/4$.
Conditional version of hasSubgaussianMGF_of_bounded: a variable with vanishing conditional
mean given $m$ and contained in an interval $[a(\omega), a(\omega) + c]$ (with $a$ being
$m$-measurable) has a conditionally sub-Gaussian MGF with the Hoeffding parameter $c^{2}/4$.
Azuma's inequality for a Doob martingale (Theorem 9.2.9). If the increments $Y_i$ are centred (conditionally on $\mathcal F_{i-1}$) and lie in intervals of length $c_i$, then $\mathbb{P}\!\big(\sum_i Y_i \ge \varepsilon\big) \le \exp\!\big({-2\varepsilon^{2} / \sum_i c_i^{2}}\big)$.