noncomputable def ErdosKleitmanRothschild.triangleFreeCount (n : ℕ) : ℕ

The number of triangle-free (labelled) simple graphs on the vertex set $\{1, \dots, n\}$.

theorem ErdosKleitmanRothschild.subgraph_count_le (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : Nat.card { H : SimpleGraph (Fin n) // H ≤ G } ≤ 2 ^ G.edgeFinset.card

The number of subgraphs of a finite simple graph $G$ is at most $2^{|E(G)|}$, since each subgraph corresponds to a subset of $E(G)$.

theorem ErdosKleitmanRothschild.triangleFreeCount_upper_bound (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), triangleFreeCount n ≤ ⌈↑n ^ (C * ↑n ^ (3 / 2))⌉₊ * 2 ^ ⌈(1 / 4 + ε) * ↑n ^ 2⌉₊

Upper bound on the number of triangle-free graphs derived from the container theorem: for every $\varepsilon > 0$ there is $C > 0$ such that $\#\{\text{triangle-free graphs on }[n]\} \leq n^{C n^{3/2}} \cdot 2^{(1/4 + \varepsilon) n^2}$.

def ErdosKleitmanRothschild.bipartiteGraphOf (n : ℕ) (S : Finset (Fin (n / 2) × Fin (n - n / 2))) : SimpleGraph (Fin n)

The bipartite graph on $\{0, \dots, n-1\}$ with bipartition $\{0, \dots, \lfloor n/2 \rfloor - 1\} \sqcup \{\lfloor n/2 \rfloor, \dots, n-1\}$ whose edges are determined by the chosen subset $S$ of the bipartite edge set. Used as the lower bound construction matching $2^{n^2/4}$ triangle-free graphs.