structure HypergraphContainers.ThreeUniformHypergraph (V : Type u_1) [Fintype V] [DecidableEq V] : Type u_1

A 3-uniform hypergraph on a finite vertex type $V$: a finite family of 3-element subsets of $V$.

• edges : Finset (Finset V)
• edges_card (e : Finset V) : e ∈ self.edges → e.card = 3

noncomputable def HypergraphContainers.ThreeUniformHypergraph.vertexCount {V : Type u_1} [Fintype V] [DecidableEq V] : ThreeUniformHypergraph V → ℕ

The number of vertices of a 3-uniform hypergraph, equal to the cardinality of $V$.

noncomputable def HypergraphContainers.ThreeUniformHypergraph.vertexDegree {V : Type u_1} [Fintype V] [DecidableEq V] (H : ThreeUniformHypergraph V) (v : V) : ℕ

The degree of a vertex $v$ in a 3-uniform hypergraph $H$: the number of edges of $H$ that contain $v$.

noncomputable def HypergraphContainers.ThreeUniformHypergraph.averageDegree {V : Type u_1} [Fintype V] [DecidableEq V] (H : ThreeUniformHypergraph V) : ℝ

The average vertex degree of a 3-uniform hypergraph, $\bar d(H) = 3|E(H)|/|V|$.

noncomputable def HypergraphContainers.ThreeUniformHypergraph.maxDegree {V : Type u_1} [Fintype V] [DecidableEq V] (H : ThreeUniformHypergraph V) : ℕ

The maximum vertex degree $\Delta_1(H)$ of a 3-uniform hypergraph.

noncomputable def HypergraphContainers.ThreeUniformHypergraph.pairCodegree {V : Type u_1} [Fintype V] [DecidableEq V] (H : ThreeUniformHypergraph V) (u v : V) : ℕ

The pair codegree $d_H(u,v)$: the number of edges of $H$ containing both $u$ and $v$.

noncomputable def HypergraphContainers.ThreeUniformHypergraph.maxPairCodegree {V : Type u_1} [Fintype V] [DecidableEq V] (H : ThreeUniformHypergraph V) : ℕ

The maximum pair codegree $\Delta_2(H) = \max_{u \neq v} d_H(u, v)$.

def HypergraphContainers.ThreeUniformHypergraph.IsIndependentSet {V : Type u_1} [Fintype V] [DecidableEq V] (H : ThreeUniformHypergraph V) (I : Finset V) : Prop

A set $I \subseteq V$ is independent in a 3-uniform hypergraph $H$ if no edge of $H$ is contained in $I$.

def HypergraphContainers.Nat.chooseLe (n k : ℕ) : ℕ

$\sum_{i=0}^{k} \binom{n}{i}$, an upper bound for the number of subsets of an $n$-element set of size at most $k$.

theorem HypergraphContainers.container_theorem_three_uniform (c : ℝ) (hc : c > 0) : ∃ δ > 0, ∀ (V : Type) [inst : Fintype V] [inst_1 : DecidableEq V] (H : ThreeUniformHypergraph V) (d : ℝ), H.averageDegree = d → d ≥ δ⁻¹ → ↑H.maxDegree ≤ c * d → ↑H.maxPairCodegree ≤ c * √d → ∃ (C : Finset (Finset V)), C.card ≤ Nat.chooseLe (Fintype.card V) ⌊↑(Fintype.card V) / √d⌋₊ ∧ (∀ (I : Finset V), H.IsIndependentSet I → ∃ S ∈ C, I ⊆ S) ∧ ∀ S ∈ C, ↑S.card ≤ (1 - δ) * ↑(Fintype.card V)

Theorem 11.3.1 (Container theorem for 3-uniform hypergraphs). For every $c > 0$ there exists $\delta > 0$ such that for every 3-uniform hypergraph $H$ with average degree $d \geq \delta^{-1}$, maximum vertex degree $\Delta_1 \leq c d$ and maximum pair codegree $\Delta_2 \leq c \sqrt{d}$, there is a family $\mathcal{C}$ of containers with

• $|\mathcal{C}| \leq \sum_{i \leq n/\sqrt{d}} \binom{n}{i}$;
• every independent set $I$ of $H$ is contained in some $S \in \mathcal{C}$;
• every container satisfies $|S| \leq (1 - \delta) n$.