def ChromaticConcentration.DiffOnlyAt {V : Type u_1} (G G' : SimpleGraph V) (v : V) : Prop

Two graphs $G$ and $G'$ on vertex set $V$ differ only at vertex $v$: their adjacency relations agree on all pairs not involving $v$.

theorem ChromaticConcentration.DiffOnlyAt.symm {V : Type u_1} {G G' : SimpleGraph V} {v : V} (h : DiffOnlyAt G G' v) : DiffOnlyAt G' G v

Symmetry of DiffOnlyAt: if $G$ and $G'$ differ only at $v$, so do $G'$ and $G$.

noncomputable def ChromaticConcentration.chromaticNumberReal (n : ℕ) (G : SimpleGraph (Fin n)) : ℝ

The chromatic number of a graph on Fin n, viewed as a real number.

theorem ChromaticConcentration.bdi_upper_tail (n : ℕ) (hn : 2 ≤ n) (p : ↑unitInterval) (ε : ℝ) (hε : 0 ≤ ε) : (SimpleGraph.binomialRandom (Fin n) p).real {G : SimpleGraph (Fin n) | ε ≤ chromaticNumberReal n G - ∫ (G' : SimpleGraph (Fin n)), chromaticNumberReal n G' ∂SimpleGraph.binomialRandom (Fin n) p} ≤ Real.exp (-2 * ε ^ 2 / ↑(n - 1))

Upper-tail bounded differences inequality applied to the chromatic number of $G(n,p)$: $\mathbb{P}(\chi(G) - \mathbb{E}\chi(G) \geq \varepsilon) \leq \exp(-2\varepsilon^2/(n-1))$.

theorem ChromaticConcentration.bdi_lower_tail (n : ℕ) (hn : 2 ≤ n) (p : ↑unitInterval) (ε : ℝ) (hε : 0 ≤ ε) : (SimpleGraph.binomialRandom (Fin n) p).real {G : SimpleGraph (Fin n) | ε ≤ ∫ (G' : SimpleGraph (Fin n)), chromaticNumberReal n G' ∂SimpleGraph.binomialRandom (Fin n) p - chromaticNumberReal n G} ≤ Real.exp (-2 * ε ^ 2 / ↑(n - 1))

Lower-tail bounded differences inequality applied to the chromatic number of $G(n,p)$: $\mathbb{P}(\mathbb{E}\chi(G) - \chi(G) \geq \varepsilon) \leq \exp(-2\varepsilon^2/(n-1))$.

theorem ChromaticConcentration.shamir_spencer (n : ℕ) (hn : 2 ≤ n) (p : ↑unitInterval) (l : ℝ) (hl : 0 ≤ l) : (SimpleGraph.binomialRandom (Fin n) p).real {G : SimpleGraph (Fin n) | l * √↑(n - 1) ≤ |chromaticNumberReal n G - ∫ (G' : SimpleGraph (Fin n)), chromaticNumberReal n G' ∂SimpleGraph.binomialRandom (Fin n) p|} ≤ 2 * Real.exp (-2 * l ^ 2)

Shamir-Spencer concentration of the chromatic number (Theorem 9.3.1, 1987): $\mathbb{P}(|\chi(G(n,p)) - \mathbb{E}\chi(G(n,p))| \geq \lambda\sqrt{n-1}) \leq 2e^{-2\lambda^2}$.