@[reducible, inline]

abbrev RamseyLowerBound.Edge (n : ℕ) : Type

An edge of the complete graph $K_n$: an unordered, non-diagonal pair of vertices.

theorem RamseyLowerBound.card_edge (n : ℕ) : Fintype.card (Edge n) = n.choose 2

The complete graph $K_n$ has $\binom{n}{2}$ edges.

def RamseyLowerBound.edgesWithin (n : ℕ) (S : Finset (Fin n)) : Finset (Edge n)

edgesWithin n S is the set of edges of $K_n$ whose endpoints both lie in S.

theorem RamseyLowerBound.card_offDiag_sym2 {α : Type u_1} [DecidableEq α] (S : Finset α) : {e ∈ S.sym2 | ¬e.IsDiag}.card = S.card.choose 2

The number of off-diagonal unordered pairs from a finite set $S$ is $\binom{|S|}{2}$.

theorem RamseyLowerBound.card_edgesWithin (n : ℕ) (S : Finset (Fin n)) : (edgesWithin n S).card = S.card.choose 2

The vertex-set $S$ spans exactly $\binom{|S|}{2}$ edges in $K_n$.

noncomputable def RamseyLowerBound.constrainedEquiv {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (b : Bool) : { f : α → Bool // ∀ x ∈ s, f x = b } ≃ ({ x : α // x ∉ s } → Bool)

Equivalence between Boolean labellings of $\alpha$ that are constantly $b$ on $s$ and arbitrary Boolean labellings of the complement $\{x : \alpha \mid x \notin s\}$.

theorem RamseyLowerBound.card_constrained {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (b : Bool) : Fintype.card { f : α → Bool // ∀ x ∈ s, f x = b } = 2 ^ (Fintype.card α - s.card)

Counting Boolean labellings constrained to take value $b$ on a set $s$: there are exactly $2^{|\alpha| - |s|}$ such labellings.

theorem RamseyLowerBound.card_monoSet (n : ℕ) (S : Finset (Fin n)) (b : Bool) : {c : Edge n → Bool | ∀ e ∈ edgesWithin n S, c e = b}.card = 2 ^ (n.choose 2 - S.card.choose 2)

The number of 2-colorings of $K_n$ that are constant of value $b$ on the edges inside $S$ is $2^{\binom{n}{2} - \binom{|S|}{2}}$.

theorem RamseyLowerBound.hyp_to_nat {n k : ℕ} (h : ↑(n.choose k) * 2 ^ (1 - ↑(k.choose 2)) < 1) : n.choose k * 2 < 2 ^ k.choose 2

Converts the real-valued Erdős–Ramsey hypothesis $\binom{n}{k} 2^{1-\binom{k}{2}} < 1$ into the natural-number inequality $2 \binom{n}{k} < 2^{\binom{k}{2}}$.

theorem RamseyLowerBound.bound_step {n k : ℕ} (hkn : k ≤ n) (h : n.choose k * 2 < 2 ^ k.choose 2) : n.choose k * 2 * 2 ^ (n.choose 2 - k.choose 2) < 2 ^ n.choose 2

From $2\binom{n}{k} < 2^{\binom{k}{2}}$ deduce $2\binom{n}{k} \cdot 2^{\binom{n}{2} - \binom{k}{2}} < 2^{\binom{n}{2}}$, which expresses that the expected number of monochromatic $k$-cliques is strictly less than the number of 2-colorings.

noncomputable def RamseyLowerBound.coloringToGraph {n : ℕ} (c : Edge n → Bool) : SimpleGraph (Fin n)

The simple graph on $[n]$ whose edges are those colored true by a given 2-coloring c of $K_n$.

theorem RamseyLowerBound.clique_implies_all_true {n : ℕ} {c : Edge n → Bool} {S : Finset (Fin n)} (hclique : (coloringToGraph c).IsClique ↑S) (e : Edge n) : e ∈ edgesWithin n S → c e = true

If $S$ is a clique in coloringToGraph c, then every edge inside $S$ is colored true by c.

theorem RamseyLowerBound.compl_clique_implies_all_false {n : ℕ} {c : Edge n → Bool} {S : Finset (Fin n)} (hclique : (coloringToGraph c)ᶜ.IsClique ↑S) (e : Edge n) : e ∈ edgesWithin n S → c e = false

If $S$ is a clique in the complement graph of coloringToGraph c, then every edge inside $S$ is colored false by c.

theorem RamseyLowerBound.erdos_1947_ramsey_lower_bound (n k : ℕ) (h : ↑(n.choose k) * 2 ^ (1 - ↑(k.choose 2)) < 1) : ∃ (G : SimpleGraph (Fin n)), G.CliqueFree k ∧ Gᶜ.CliqueFree k

(Erdős 1947, Ramsey lower bound) If $\binom{n}{k} \cdot 2^{1 - \binom{k}{2}} < 1$, then there exists a graph on $n$ vertices with no $k$-clique in $G$ or $G^c$, so $R(k, k) > n$.