def SharpThresholdColorability.numPossibleEdges (n : ℕ) : ℕ

Number of potential edges in a simple graph on $n$ vertices, i.e. $\binom{n}{2}$.

noncomputable def SharpThresholdColorability.erdosRenyiWeight (n : ℕ) (p : ℝ) (G : SimpleGraph (Fin n)) : ℝ

Erdős-Rényi weight $p^{|E(G)|} (1-p)^{\binom{n}{2} - |E(G)|}$ assigned to a labeled graph $G$ on $\{0, \dots, n-1\}$ in $G(n,p)$.

noncomputable def SharpThresholdColorability.probColorable (n k : ℕ) (p : ℝ) : ℝ

Probability that $G(n,p)$ is $k$-colorable, computed as the Erdős-Rényi-weighted count of labeled $k$-colorable simple graphs on $\{0, \dots, n-1\}$.

theorem SharpThresholdColorability.achlioptas_friedgut (k : ℕ) (hk : k ≥ 3) : ∃ (d_k : ℕ → ℝ), (∀ ε > 0, ∀ (d : ℕ → ℝ), (∀ (n : ℕ), d n > 0) → (∀ᶠ (n : ℕ) in Filter.atTop, d n < d_k n - ε) → Filter.Tendsto (fun (n : ℕ) => probColorable n k (d n / ↑n)) Filter.atTop (nhds 1)) ∧ ∀ ε > 0, ∀ (d : ℕ → ℝ), (∀ (n : ℕ), d n > 0) → (∀ᶠ (n : ℕ) in Filter.atTop, d n > d_k n + ε) → Filter.Tendsto (fun (n : ℕ) => probColorable n k (d n / ↑n)) Filter.atTop (nhds 0)

Theorem 4.3.17 (Achlioptas-Friedgut 2000). For every $k \ge 3$ there is a sharp threshold sequence $d_k(n)$ for $k$-colorability in $G(n, d/n)$: if $d_n < d_k(n) - \varepsilon$ eventually then $\mathbb{P}(G(n, d_n/n) \text{ is } k\text{-colorable}) \to 1$, while if $d_n > d_k(n) + \varepsilon$ eventually then the probability $\to 0$.