noncomputable def ChromaticNumber.muClique (n k : ℕ) : ℝ

Expected number of $k$-cliques in $G(n,1/2)$: $\mu = \binom{n}{k} \cdot 2^{-\binom{k}{2}}$.

noncomputable def ChromaticNumber.k₀ (n : ℕ) : ℕ

The largest $k \le n$ for which the expected number $\mu(n,k)$ of $k$-cliques in $G(n,1/2)$ is still at least $1$.

noncomputable def ChromaticNumber.cliqueNum {n : ℕ} (G : SimpleGraph (Fin n)) : ℕ

Clique number of a finite graph on Fin n: the largest $k \le n$ such that $G$ contains a clique of size $k$.

noncomputable def ChromaticNumber.probGnHalf (n : ℕ) (A : SimpleGraph (Fin n) → Prop) : ℝ

Probability of an event $A$ on graphs sampled from $G(n,1/2)$, computed combinatorially as the fraction of graphs on $\{1,\dots,n\}$ satisfying $A$.

noncomputable def ChromaticNumber.deltaClique (n k : ℕ) : ℝ

The $\Delta$ quantity from Janson's inequality applied to the $k$-clique event in $G(n,1/2)$: a sum over the shared-vertex parameter $s \in [2, k-1]$ that bounds the correlation between pairs of overlapping $k$-cliques.

theorem ChromaticNumber.k₀_le (n : ℕ) : k₀ n ≤ n

The threshold clique-size $k_0(n)$ is at most $n$, since it is the greatest such value in $\{0, \dots, n\}$.

theorem ChromaticNumber.cliqueNum_lt_iff_cliqueFree {n : ℕ} (G : SimpleGraph (Fin n)) (m : ℕ) (hm : m ≤ n) (hm0 : 0 < m) : cliqueNum G < m ↔ G.CliqueFree m

Dual characterization of cliqueNum: for $0 < m \le n$, the clique number of $G$ is strictly less than $m$ iff $G$ contains no $m$-clique.

theorem ChromaticNumber.janson_clique_parametric_bound (n k : ℕ) (hμ : 0 < muClique n k) (hΔ : muClique n k ≤ deltaClique n k) (q : ℝ) : 0 ≤ q → q ≤ 1 → (probGnHalf n fun (G : SimpleGraph (Fin n)) => G.CliqueFree k) ≤ Real.exp (-q * muClique n k + q ^ 2 * deltaClique n k / 2)

Parametric form of Janson's inequality applied to the $k$-clique event: for each $q \in [0,1]$, $\Pr_{G(n,1/2)}(G \text{ is } K_k\text{-free}) \le \exp(-q\mu + q^2 \Delta / 2)$, with $\mu = $ muClique n k and $\Delta = $ deltaClique n k.

theorem ChromaticNumber.janson_clique_bound (n k : ℕ) (hμ : 0 < muClique n k) (hΔ : muClique n k ≤ deltaClique n k) : (probGnHalf n fun (G : SimpleGraph (Fin n)) => G.CliqueFree k) ≤ Real.exp (-muClique n k ^ 2 / (2 * deltaClique n k))

Optimized Janson bound for the $k$-clique event, obtained by minimizing the parametric bound over $q$: $\Pr(G \text{ is } K_k\text{-free}) \le \exp(-\mu^2 / (2\Delta))$.

theorem ChromaticNumber.factorial_le_two_pow_choose (L : ℕ) : L.factorial ≤ 2 ^ L.choose 2

Elementary bound $L! \le 2^{\binom{L}{2}}$, used in estimating the asymptotics of the clique-counting quantities.

theorem ChromaticNumber.mu_lower_bound (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (3 - ε) ≤ muClique n (k₀ n - 3)

Asymptotic lower bound on the expected clique count at the shifted threshold: for any $\varepsilon > 0$, eventually $\mu(n, k_0(n) - 3) \ge n^{3 - \varepsilon}$.

theorem ChromaticNumber.delta_mu_sq_bound (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, deltaClique n (k₀ n - 3) ≤ muClique n (k₀ n - 3) ^ 2 * ↑n ^ (-2 + ε)

Asymptotic upper bound on $\Delta$ relative to $\mu^2$: for any $\varepsilon > 0$, eventually $\Delta(n, k_0(n) - 3) \le \mu(n, k_0(n) - 3)^2 \cdot n^{-2 + \varepsilon}$.

theorem ChromaticNumber.delta_s2_ratio_ge_one : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ ↑((k₀ n - 3).choose 2) * ↑((n - (k₀ n - 3)).choose (k₀ n - 3 - 2)) * 2 ^ (1 - ↑((k₀ n - 3).choose 2))

Eventually the dominant $s = 2$ term of $\Delta / \mu$ is at least $1$: $\binom{k}{2}\binom{n-k}{k-2} \cdot 2^{1 - \binom{k}{2}} \ge 1$ at $k = k_0(n) - 3$.

theorem ChromaticNumber.k0_eventually_ge_six : ∀ᶠ (n : ℕ) in Filter.atTop, 6 ≤ k₀ n

Eventually $k_0(n) \ge 6$: the threshold clique size grows without bound, in particular it surpasses every fixed constant.

theorem ChromaticNumber.delta_ge_mu_eventually : ∀ᶠ (n : ℕ) in Filter.atTop, muClique n (k₀ n - 3) ≤ deltaClique n (k₀ n - 3)

Eventually $\Delta \ge \mu$ at the shifted threshold, since the $s = 2$ summand of $\Delta$ alone dominates $\mu$.

theorem ChromaticNumber.mu_pos_eventually : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < muClique n (k₀ n - 3)

Eventually $\mu(n, k_0(n) - 3) > 0$, immediate from the asymptotic lower bound.

theorem ChromaticNumber.mu_sq_over_delta_bound (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (2 - ε) ≤ muClique n (k₀ n - 3) ^ 2 / (2 * deltaClique n (k₀ n - 3))

Asymptotic lower bound $n^{2-\varepsilon} \le \mu^2 / (2\Delta)$ at the shifted threshold, which is the exponent appearing inside Janson's inequality.

theorem ChromaticNumber.cliqueFree_prob_bound (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, (probGnHalf n fun (G : SimpleGraph (Fin n)) => G.CliqueFree (k₀ n - 3)) ≤ Real.exp (-↑n ^ (2 - ε))

Sub-Gaussian decay of the $K_{k_0 - 3}$-free probability: for every $\varepsilon > 0$, $\Pr(G(n,1/2) \text{ is } K_{k_0(n)-3}\text{-free}) \le \exp(-n^{2-\varepsilon})$.

theorem ChromaticNumber.clique_number_lower_bound (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, (probGnHalf n fun (G : SimpleGraph (Fin n)) => cliqueNum G < k₀ n - 3) ≤ Real.exp (-↑n ^ (2 - ε))

Theorem 8.3.2 (Bollobás 1988), one direction: with very high probability the clique number of $G(n,1/2)$ is at least $k_0(n) - 3$, the threshold value. The complementary probability is at most $\exp(-n^{2-\varepsilon})$.