def Sampling.IsThreeUniform {n : ℕ} (E : Finset (Finset (Fin n))) : Prop

A hypergraph $E$ on $\mathrm{Fin}\,n$ is 3-uniform if every hyperedge has exactly $3$ elements.

def Sampling.IsTetrahedronFree {n : ℕ} (E : Finset (Finset (Fin n))) : Prop

A 3-uniform hypergraph $E$ is tetrahedron-free if no $4$-vertex subset contains $4$ hyperedges (i.e., all four triples in some $4$-set), equivalently every $4$-set spans at most $3$ hyperedges.

theorem Sampling.card_four_supersets {n : ℕ} (e : Finset (Fin n)) (he : e.card = 3) (_hn : 4 ≤ n) : {S ∈ Finset.powersetCard 4 Finset.univ | e ⊆ S}.card = n - 3

For a fixed $3$-element set $e \subseteq \mathrm{Fin}\,n$, the number of $4$-element supersets of $e$ in $\mathrm{Fin}\,n$ equals $n - 3$ (one for each remaining vertex).

theorem Sampling.tetrahedron_free_below {n : ℕ} (E : Finset (Finset (Fin n))) (hUnif : IsThreeUniform E) (hFree : IsTetrahedronFree E) (S : Finset (Fin n)) (hS : S ∈ Finset.powersetCard 4 Finset.univ) : {x ∈ E | x ⊆ S}.card ≤ 3

Translation of the tetrahedron-free condition: for any $4$-set $S$, the number of hyperedges contained in $S$ is at most $3$.

theorem Sampling.cheap_sampling_bound {n : ℕ} (hn : 4 ≤ n) (E : Finset (Finset (Fin n))) (hUnif : IsThreeUniform E) (hFree : IsTetrahedronFree E) : 4 * E.card ≤ 3 * n.choose 3

Cheap sampling bound (Proposition 2.4.2). A tetrahedron-free $3$-uniform hypergraph on $n \geq 4$ vertices has at most $\tfrac{3}{4}\binom{n}{3}$ hyperedges; equivalently $4 |E| \leq 3 \binom{n}{3}$.

def Sampling.ContainsTetrahedron (H : Finset (Finset (Fin 5))) : Prop

A $3$-uniform hypergraph on $\mathrm{Fin}\,5$ contains a tetrahedron if some $4$-vertex subset $T$ has all four of its $3$-element subsets as hyperedges.

def Sampling.IsTetrahedronFree5 (H : Finset (Finset (Fin 5))) : Prop

A $3$-uniform hypergraph on $\mathrm{Fin}\,5$ is tetrahedron-free if it does not contain a tetrahedron.

@[implicit_reducible]

instance Sampling.instDecidableContainsTetrahedron (H : Finset (Finset (Fin 5))) : Decidable (ContainsTetrahedron H)

Decidability of ContainsTetrahedron, exploited for the finite case-check used in Lemma 2.4.3.

@[implicit_reducible]

instance Sampling.instDecidableIsTetrahedronFree5 (H : Finset (Finset (Fin 5))) : Decidable (IsTetrahedronFree5 H)

Decidability of IsTetrahedronFree5.