def GraphContainers.IsHFree {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) : Prop

IsHFree G H says that the graph $G$ contains no copy of $H$ as a subgraph.

noncomputable def GraphContainers.hFreeGraphs {W : Type u_2} (H : SimpleGraph W) (n : ℕ) : Finset (SimpleGraph (Fin n))

The finset of all $H$-free labelled graphs on the vertex set $\{1, \dots, n\}$.

noncomputable def GraphContainers.extremalNumber {W : Type u_2} (H : SimpleGraph W) (n : ℕ) : ℕ

The extremal number $\mathrm{ex}(n, H)$: the maximum number of edges in an $H$-free graph on $n$ vertices.

theorem GraphContainers.count_hFreeGraphs_nonBipartite {W : Type u_3} (H : SimpleGraph W) [Fintype W] [DecidableEq W] [DecidableRel H.Adj] (hH : ¬H.IsBipartite) (ε : ℝ) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, (hFreeGraphs H n).card ≤ 2 ^ ⌈(1 + ε) * ↑(extremalNumber H n)⌉₊ ∧ 2 ^ ⌊(1 - ε) * ↑(extremalNumber H n)⌋₊ ≤ (hFreeGraphs H n).card

Theorem 11.2.1 (Graph container theorem, non-bipartite case). For any non-bipartite graph $H$ and every $\varepsilon > 0$, eventually the number of $H$-free graphs on $n$ vertices is $2^{(1 \pm \varepsilon) \mathrm{ex}(n, H)}$.

theorem GraphContainers.conjecture_hFreeGraphs_bipartite {W : Type u_3} (H : SimpleGraph W) [Fintype W] [DecidableEq W] [DecidableRel H.Adj] (hbip : H.IsBipartite) (hcycle : ¬H.IsAcyclic) : ∃ (C : ℕ), ∀ (n : ℕ), (hFreeGraphs H n).card ≤ 2 ^ (C * extremalNumber H n)

Conjectured bipartite analogue of the container theorem: for every bipartite $H$ with a cycle there is a constant $C$ such that the number of $H$-free graphs on $n$ vertices is at most $2^{C \cdot \mathrm{ex}(n, H)}$.

theorem GraphContainers.erdos_stone_simonovits {W : Type u_3} (H : SimpleGraph W) [Fintype W] [DecidableEq W] [DecidableRel H.Adj] (hH : ¬H.IsBipartite) : Filter.Tendsto (fun (n : ℕ) => ↑(extremalNumber H n) / ↑(n.choose 2)) Filter.atTop (nhds (1 - 1 / (↑H.chromaticNumber.toNat - 1)))

Erdős–Stone–Simonovits theorem: for a non-bipartite graph $H$, $\mathrm{ex}(n, H) / \binom{n}{2} \to 1 - 1/(\chi(H) - 1)$ as $n \to \infty$.

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

The average degree $2|E(G)| / |V(G)|$ of a finite graph.

theorem GraphContainers.container_algorithm_output {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) (hc : c > 0) (hmaxdeg : ↑G.maxDegree ≤ c * averageDegree G) (havgpos : averageDegree G > 0) (I : Set V) (hI : G.IsIndepSet I) : ∃ (fp : Finset V) (avail : Finset V), ↑fp ⊆ I ∧ I ⊆ ↑(fp ∪ avail) ∧ ↑fp.card ≤ 2 * (1 / (4 * c + 2)) * ↑(Fintype.card V) / averageDegree G ∧ ↑(fp ∪ avail).card ≤ (1 - 1 / (4 * c + 2)) * ↑(Fintype.card V)

Container algorithm output. Given a graph $G$ with bounded max-to-average-degree ratio and an independent set $I$, there exist a small fingerprint $\mathrm{fp} \subseteq I$ and an available set such that $I$ is contained in $\mathrm{fp} \cup \mathrm{avail}$, with quantitative size bounds in terms of $\bar d(G)$.

theorem GraphContainers.container_algorithm_deterministic {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℝ) (hc : c > 0) (hmaxdeg : ↑G.maxDegree ≤ c * averageDegree G) (havgpos : averageDegree G > 0) (I I' : Set V) (hI : G.IsIndepSet I) (hI' : G.IsIndepSet I') (hfp_eq : ⋯.choose = ⋯.choose) : ⋯.choose = ⋯.choose

The container algorithm's available-set output depends only on the fingerprint: two independent sets producing the same fingerprint yield the same available set. This is the determinism property needed to encode the algorithm with the fingerprint alone.

theorem GraphContainers.graph_container_fingerprints (c : ℝ) (hc : c > 0) : ∃ δ > 0, ∀ (V : Type u_3) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], ↑G.maxDegree ≤ c * averageDegree G → averageDegree G > 0 → ∃ (S : { I : Set V // G.IsIndepSet I } → Finset V) (A : Finset V → Finset V), ∀ (I : Set V) (hI : G.IsIndepSet I), ↑(S ⟨I, hI⟩) ⊆ I ∧ I ⊆ ↑(S ⟨I, hI⟩) ∪ ↑(A (S ⟨I, hI⟩)) ∧ ↑(S ⟨I, hI⟩).card ≤ 2 * δ * ↑(Fintype.card V) / averageDegree G ∧ ↑(S ⟨I, hI⟩ ∪ A (S ⟨I, hI⟩)).card ≤ (1 - δ) * ↑(Fintype.card V)

Theorem 11.2.3 (Graph container fingerprints). There is $\delta > 0$ such that for every graph $G$ with bounded max-to-average-degree ratio, every independent set $I$ is determined by a small fingerprint $S(I) \subseteq I$ together with an available set $A(S(I))$ depending only on the fingerprint, with $|S(I)| \le 2\delta |V|/\bar d(G)$ and $|S(I) \cup A(S(I))| \le (1 - \delta)|V|$.

noncomputable def GraphContainers.erdosRenyiMeasure (n : ℕ) (p : ℝ) : MeasureTheory.Measure (SimpleGraph (Fin n))

The Erdős–Rényi measure $G(n, p)$ on simple graphs on the vertex set $\{1, \dots, n\}$: each potential edge is independently present with probability $p$, and the weight of a graph $G$ is $p^{|E(G)|}(1-p)^{m - |E(G)|}$ with $m = \binom{n}{2}$.

def GraphContainers.badEvent (n : ℕ) (threshold : ℝ) : Set (SimpleGraph (Fin n))

The "bad" event in the random graph $G(n, p)$: there exists a triangle-free subgraph $H \le G$ with more than threshold edges.

theorem GraphContainers.triangleFreeContainerLemma (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), ∃ (𝒞 : Finset (SimpleGraph (Fin n))), ↑𝒞.card ≤ ↑n ^ (C * ↑n ^ (3 / 2)) ∧ (∀ G ∈ 𝒞, ↑G.edgeFinset.card ≤ (1 / 4 + ε) * ↑n ^ 2) ∧ ∀ (H : SimpleGraph (Fin n)), H.CliqueFree 3 → ∃ G ∈ 𝒞, H ≤ G

Container lemma for triangle-free graphs: there is a small collection $\mathcal C$ of "containers", each with at most $(1/4 + \varepsilon) n^2$ edges, such that every triangle-free graph on $n$ vertices is a subgraph of some container.

theorem GraphContainers.chernoff_erdosRenyi_container (ε : ℝ) (hε : 0 < ε) : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ) (p : ℝ), 0 < p → p ≤ 1 → ∀ (C_graph : SimpleGraph (Fin n)), ↑C_graph.edgeFinset.card ≤ (1 / 4 + ε) * ↑n ^ 2 → (erdosRenyiMeasure n p) {G : SimpleGraph (Fin n) | ↑(C_graph ⊓ G).edgeFinset.card > (1 / 4 + 2 * ε) * p * ↑n ^ 2} ≤ ENNReal.ofReal (Real.exp (-c * ↑n ^ 2 * p))

Chernoff bound for the number of edges of a fixed container intersected with a $G(n,p)$ sample: with high probability the intersection has at most $(1/4 + 2\varepsilon) p n^2$ edges.

theorem GraphContainers.badEvent_subset_container_union (n : ℕ) (ε : ℝ) (𝒞 : Finset (SimpleGraph (Fin n))) (hcover : ∀ (H : SimpleGraph (Fin n)), H.CliqueFree 3 → ∃ G ∈ 𝒞, H ≤ G) (p : ℝ) : badEvent n ((1 / 4 + 2 * ε) * p * ↑n ^ 2) ⊆ ⋃ C ∈ 𝒞, {G : SimpleGraph (Fin n) | ↑(C ⊓ G).edgeFinset.card > (1 / 4 + 2 * ε) * p * ↑n ^ 2}

Combining the container cover with the bad event: every realization of the bad event lies in the union over containers $C$ of the events "$C \cap G$ has too many edges".

theorem GraphContainers.unionBound_containerChernoff (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 0 < c ∧ ∀ (n : ℕ) (p : ℝ), 0 < p → p ≤ 1 → ((erdosRenyiMeasure n p) (badEvent n ((1 / 4 + 2 * ε) * p * ↑n ^ 2))).toReal ≤ ↑n ^ (C * ↑n ^ (3 / 2)) * Real.exp (-c * ↑n ^ 2 * p)

Union bound combined with the container chernoff bound: the probability of the bad event in $G(n, p)$ is at most $n^{C n^{3/2}} \exp(-c n^2 p)$ for universal constants $C, c > 0$.

theorem GraphContainers.asymptotic_bound_pointwise (C c b : ℝ) (hc : 0 < c) (n : ℕ) (pn : ℝ) (hn2 : 2 < n) (hn : (C + 1) / c ≤ pn * ↑n ^ (1 / 2) / Real.log ↑n) (hlarge : -↑n ^ (3 / 2) * Real.log ↑n ≤ b) : C * ↑n ^ (3 / 2) * Real.log ↑n - c * ↑n ^ 2 * pn ≤ b

Pointwise inequality used in the asymptotic analysis: when $p_n n^{1/2}/\log n$ is large enough, the expression $C n^{3/2} \log n - c n^2 p_n$ is bounded above by any prescribed $b$.

theorem GraphContainers.exponent_tends_to_neg_inf (C c : ℝ) (_hC : 0 < C) (hc : 0 < c) (p : ℕ → ℝ) (hp_growth : Filter.Tendsto (fun (n : ℕ) => p n * ↑n ^ (1 / 2) / Real.log ↑n) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => C * ↑n ^ (3 / 2) * Real.log ↑n - c * ↑n ^ 2 * p n) Filter.atTop Filter.atBot

If $p_n \cdot n^{1/2} / \log n \to \infty$, then the exponent $C n^{3/2} \log n - c n^2 p_n$ tends to $-\infty$.

theorem GraphContainers.mantel_in_random_graphs (p : ℕ → ℝ) (hp_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < p n) (hp_le : ∀ᶠ (n : ℕ) in Filter.atTop, p n ≤ 1) (hp_growth : Filter.Tendsto (fun (n : ℕ) => p n * ↑n ^ (1 / 2) / Real.log ↑n) Filter.atTop Filter.atTop) (ε : ℝ) (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => ((erdosRenyiMeasure n (p n)) (badEvent n ((1 / 4 + 2 * ε) * p n * ↑n ^ 2))).toReal) Filter.atTop (nhds 0)

Mantel-in-random-graphs corollary: if $p_n n^{1/2}/\log n \to \infty$, then with probability tending to $1$ every triangle-free subgraph of $G(n, p_n)$ has at most $(1/4 + 2\varepsilon) p_n n^2$ edges.