def ListChromatic.IsKChoosable (n k : ℕ) : Prop

IsKChoosable n k says that the complete bipartite graph $K_{n,n}$ is $k$-choosable in the combinatorial sense: for any color set $C$ and any pair of list assignments $L, R : [n] \to \binom{C}{\ge k}$, there exist representatives $cL_i \in L_i$ and $cR_j \in R_j$ with $cL_i \ne cR_j$ for all $i, j$.

theorem ListChromatic.exists_good_subset {n k : ℕ} {C : Type} [Fintype C] [DecidableEq C] (L R : Fin n → Finset C) (hL : ∀ (i : Fin n), k ≤ (L i).card) (hR : ∀ (j : Fin n), k ≤ (R j).card) (hn : n < 2 ^ (k - 1)) : ∃ (A : Finset C), (∀ (i : Fin n), (L i ∩ A).Nonempty) ∧ ∀ (j : Fin n), (R j \ A).Nonempty

Key combinatorial lemma behind Theorem 1.4.2: when $n < 2^{k-1}$ and all lists have size at least $k$, there exists a subset $A$ of colors hitting every left list and missing at least one element of every right list.

theorem ListChromatic.knn_choosable (n k : ℕ) (_hk : 0 < k) (hn : n < 2 ^ (k - 1)) : IsKChoosable n k

(Theorem 1.4.2) If $n < 2^{k-1}$ and $k \ge 1$, then $K_{n,n}$ is $k$-choosable.

theorem ListChromatic.hypergraph_implies_not_choosable {V : Type u_1} [Fintype V] [DecidableEq V] (k n : ℕ) (_hk : 2 ≤ k) (E : TwoColorableHypergraph.Hypergraph V) (hE_unif : TwoColorableHypergraph.IsKUniform E k) (hE_edges : Finset.card E = n) (hE_not_2col : ¬TwoColorableHypergraph.IsTwoColorable E) : ¬IsKChoosable n k

Translation lemma used for the lower bound on $ch(K_{n,n})$: a $k$-uniform hypergraph on $n$ edges that is not 2-colorable witnesses that $K_{n,n}$ is not $k$-choosable.

@[reducible, inline]

abbrev SimpleGraph.ListAssignment (V : Type u_2) (C : Type u_3) : Type (max u_2 u_3)

A list assignment on a vertex set V is a function assigning each vertex a finite list of available colors.

def SimpleGraph.IsListColorable' {V : Type u_1} (G : SimpleGraph V) {C : Type u_2} (L : ListAssignment V C) : Prop

G.IsListColorable' L says that there is a proper coloring of G choosing each vertex's color from its list L v.

def SimpleGraph.IsKChoosable' {V : Type u_1} (G : SimpleGraph V) (k : ℕ) : Prop

A graph is $k$-choosable if every list assignment with lists of size at least $k$ admits a proper list coloring.

noncomputable def SimpleGraph.listChromaticNumber {V : Type u_1} (G : SimpleGraph V) : ℕ∞

The list chromatic number $ch(G)$ of a graph $G$: the smallest $k$ for which $G$ is $k$-choosable, as an element of $\mathbb{N} \cup \{\infty\}$.

noncomputable def SimpleGraph.averageDegree {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] : ℝ

The average degree of a finite graph $G$, i.e. $\frac{1}{|V|} \sum_{v} \deg(v)$ (or $0$ when $V$ is empty).

theorem SimpleGraph.saxton_thomason (ε : ℝ) : 0 < ε → ∃ (D : ℝ), 0 < D ∧ ∀ (V : Type) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.averageDegree ≥ D → G.listChromaticNumber ≥ ↑⌈(1 - ε) * (Real.log G.averageDegree / Real.log 2)⌉₊

(Theorem 1.4.5, Saxton–Thomason 2015) For every $\varepsilon > 0$ there is a $D > 0$ such that every graph $G$ with average degree at least $D$ satisfies $ch(G) \ge (1 - \varepsilon) \log_2 \bar d(G)$.

@[implicit_reducible]

instance instDecidableRelAdjCompleteBipartiteGraph {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] : DecidableRel (completeBipartiteGraph V W).Adj

Decidability of adjacency in the complete bipartite graph, when both vertex types have decidable equality.

theorem completeBipartiteGraph_degree_eq (n : ℕ) (v : Fin n ⊕ Fin n) : (completeBipartiteGraph (Fin n) (Fin n)).degree v = n

Every vertex of $K_{n,n}$ has degree exactly $n$.

theorem completeBipartiteGraph_averageDegree (n : ℕ) (hn : 0 < n) : (completeBipartiteGraph (Fin n) (Fin n)).averageDegree = ↑n

The average degree of $K_{n,n}$ is $n$.

theorem ch_knn_lower_bound (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (completeBipartiteGraph (Fin n) (Fin n)).listChromaticNumber ≥ ↑⌈(1 - ε) * (Real.log ↑n / Real.log 2)⌉₊

Lower bound on $ch(K_{n,n})$ obtained by applying the Saxton–Thomason theorem to $K_{n,n}$ (whose average degree is $n$).

theorem ch_knn_asymptotic_lower (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (completeBipartiteGraph (Fin n) (Fin n)).listChromaticNumber ≥ ↑⌈(1 - ε) * (Real.log ↑n / Real.log 2)⌉₊

(Half of Corollary 1.4.4, lower direction) Asymptotic lower bound $ch(K_{n,n}) \ge (1 - \varepsilon) \log_2 n$ for all sufficiently large $n$.

theorem knn_IsKChoosable'_of_IsKChoosable (n k : ℕ) (h : ListChromatic.IsKChoosable n k) : (completeBipartiteGraph (Fin n) (Fin n)).IsKChoosable' k

The combinatorial IsKChoosable n k condition implies that $K_{n,n}$ is $k$-choosable in the graph-theoretic sense.

theorem SimpleGraph.listChromaticNumber_le_of_isKChoosable' {V : Type u_1} (G : SimpleGraph V) (k : ℕ) (h : G.IsKChoosable' k) : G.listChromaticNumber ≤ ↑k

If $G$ is $k$-choosable then its list chromatic number is at most $k$.

theorem aux_n_lt_pow_ceil_sub_one {n : ℕ} {ε : ℝ} (hε : 0 < ε) (hn_gt_one : 1 < n) (hlogn_large : 1 / ε < Real.log ↑n / Real.log 2) : n < 2 ^ (⌈(1 + ε) * (Real.log ↑n / Real.log 2)⌉₊ - 1)

Auxiliary inequality: for $n > 1$ with $\log_2 n > 1/\varepsilon$, we have $n < 2^{\lceil (1 + \varepsilon)\log_2 n \rceil - 1}$, allowing application of the $k$-choosability bound.

theorem ch_knn_asymptotic_upper (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (completeBipartiteGraph (Fin n) (Fin n)).listChromaticNumber ≤ ↑⌈(1 + ε) * (Real.log ↑n / Real.log 2)⌉₊

(Half of Corollary 1.4.4, upper direction) Asymptotic upper bound $ch(K_{n,n}) \le (1 + \varepsilon) \log_2 n$ for all sufficiently large $n$.

theorem ch_knn_asymptotic (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ↑⌈(1 - ε) * (Real.log ↑n / Real.log 2)⌉₊ ≤ (completeBipartiteGraph (Fin n) (Fin n)).listChromaticNumber ∧ (completeBipartiteGraph (Fin n) (Fin n)).listChromaticNumber ≤ ↑⌈(1 + ε) * (Real.log ↑n / Real.log 2)⌉₊

(Corollary 1.4.4) $ch(K_{n,n}) = (1 + o(1)) \log_2 n$; both asymptotic bounds combined.