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

The average degree of a finite simple graph, $\bar d(G) = 2|E(G)|/|V(G)|$.

def GraphContainers.binomialSum (n k : ℕ) : ℕ

The partial binomial sum $\sum_{i=0}^{k} \binom{n}{i}$, bounding the number of subsets of an $n$-element set of size at most $k$.

theorem GraphContainers.container_algorithm_claim (c : ℝ) : 0 < c → ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ ∀ (V : Type u_1) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], ↑G.maxDegree ≤ c * avgDegree G → ∃ (container : Finset V → Finset V), (∀ (S : Finset V), ↑S.card ≤ 2 * δ * ↑(Fintype.card V) / avgDegree G → ↑(container S).card ≤ (1 - δ) * ↑(Fintype.card V)) ∧ ∀ (I : Finset V), G.IsIndepSet ↑I → ∃ S ⊆ I, I ⊆ container S ∧ ↑S.card ≤ 2 * δ * ↑(Fintype.card V) / avgDegree G

Container algorithm (fingerprint version, Theorem 11.2.3). For every $c > 0$ there exists $0 < \delta < 1$ such that for every graph $G$ with $\Delta(G) \leq c \, \bar d(G)$ there is a function container mapping each small "fingerprint" $S$ to a vertex set with $|container(S)| \leq (1 - \delta) |V|$, and every independent set $I$ has a fingerprint $S \subseteq I$ of size $\leq 2\delta |V|/\bar d(G)$ with $I \subseteq container(S)$.

theorem GraphContainers.independent_set_container (c : ℝ) : 0 < c → ∃ (δ : ℝ), 0 < δ ∧ ∀ (V : Type u_1) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], ↑G.maxDegree ≤ c * avgDegree G → ∃ (𝒞 : Finset (Finset V)), ↑𝒞.card ≤ ↑(binomialSum (Fintype.card V) ⌊2 * δ * ↑(Fintype.card V) / avgDegree G⌋₊) ∧ (∀ (I : Finset V), G.IsIndepSet ↑I → ∃ C ∈ 𝒞, I ⊆ C) ∧ ∀ C ∈ 𝒞, ↑C.card ≤ (1 - δ) * ↑(Fintype.card V)

Theorem 11.2.1 (Container theorem for independent sets in graphs). For every $c > 0$ there exists $\delta > 0$ such that for every finite graph $G$ with $\Delta(G) \leq c \, \bar d(G)$, there is a family $\mathcal{C}$ of "containers" such that

• $|\mathcal{C}| \leq \sum_{i \leq 2\delta n / \bar d(G)} \binom{n}{i}$;
• every independent set of $G$ is contained in some $C \in \mathcal{C}$;
• every container has $|C| \leq (1 - \delta) n$.