noncomputable def CliqueNumber.expectedKCliques (n k : ℕ) : ℝ

Expected number of $k$-cliques in the random graph $G(n, 1/2)$, equal to $\binom{n}{k} \cdot 2^{-\binom{k}{2}}$.

theorem CliqueNumber.expectedKCliques_eq_div (n k : ℕ) : expectedKCliques n k = ↑(n.choose k) / 2 ^ k.choose 2

Rewrites the expected number of $k$-cliques as the quotient $\binom{n}{k} / 2^{\binom{k}{2}}$.

noncomputable def CliqueNumber.probCliqueGe (n k : ℕ) : ℝ

Probability under the uniform measure on simple graphs on $\{1,\dots,n\}$ (equivalently $G(n, 1/2)$) that the graph contains a clique of size at least $k$.

theorem CliqueNumber.probCliqueGe_nonneg (n k : ℕ) : 0 ≤ probCliqueGe n k

The probability probCliqueGe n k is nonnegative.

theorem CliqueNumber.ba_sup_inf_right {α : Type u_1} [BooleanAlgebra α] {a H K : α} (hH : H ≤ a) (hK : K ≤ aᶜ) : (H ⊔ K) ⊓ a = H

In a Boolean algebra, if $H \le a$ and $K \le a^c$, then $(H \sqcup K) \sqcap a = H$.

theorem CliqueNumber.ba_sup_inf_compl {α : Type u_1} [BooleanAlgebra α] {a H K : α} (hH : H ≤ a) (hK : K ≤ aᶜ) : (H ⊔ K) ⊓ aᶜ = K

In a Boolean algebra, if $H \le a$ and $K \le a^c$, then $(H \sqcup K) \sqcap a^c = K$.

noncomputable def CliqueNumber.boolAlgDecomp {α : Type u_1} [BooleanAlgebra α] (a : α) : α ≃ ↑(Set.Iic a) × ↑(Set.Iic aᶜ)

Equivalence decomposing a Boolean algebra $\alpha$ as the product $[\bot, a] \times [\bot, a^c]$ via the map $x \mapsto (x \sqcap a, x \sqcap a^c)$.

noncomputable def CliqueNumber.iciEquivIicCompl {α : Type u_1} [BooleanAlgebra α] (a : α) : ↑(Set.Ici a) ≃ ↑(Set.Iic aᶜ)

Equivalence between the upper set $[a, \top]$ and the lower set $[\bot, a^c]$ in a Boolean algebra, given by complementation.

theorem CliqueNumber.card_eq_Iic_mul_Ici {α : Type u_1} [BooleanAlgebra α] [Fintype α] (a : α) : Fintype.card α = Fintype.card ↑(Set.Iic a) * Fintype.card ↑(Set.Ici a)

In a finite Boolean algebra, the cardinality factors as $|\alpha| = |[\bot, a]| \cdot |[a, \top]|$.

noncomputable def CliqueNumber.iicEquivBoolFn {V : Type u_1} [Fintype V] [DecidableEq V] (a : SimpleGraph V) : ↑(Set.Iic a) ≃ (↥a.edgeFinset → Bool)

Equivalence between subgraphs of a simple graph $a$ on $V$ and Boolean functions on its edge set: a subgraph corresponds to the indicator on whether each edge is kept.

theorem CliqueNumber.card_Iic_eq_pow_edgeFinset {V : Type u_1} [Fintype V] [DecidableEq V] (a : SimpleGraph V) : Fintype.card ↑(Set.Iic a) = 2 ^ a.edgeFinset.card

The number of subgraphs of a simple graph $a$ equals $2^{|E(a)|}$, the number of subsets of its edge set.

theorem CliqueNumber.markov_bound (n k : ℕ) : probCliqueGe n k ≤ expectedKCliques n k

Markov's (first moment) inequality for the clique number in $G(n, 1/2)$: $\Pr[\omega(G) \ge k] \le \mathbb{E}[X_k] = \binom{n}{k} 2^{-\binom{k}{2}}$, where $X_k$ counts the $k$-cliques.

theorem CliqueNumber.clique_number_first_moment_bound (k : ℕ → ℕ) (hf : Filter.Tendsto (fun (n : ℕ) => expectedKCliques n (k n)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => probCliqueGe n (k n)) Filter.atTop (nhds 0)

First moment direction of the two-point concentration (cf. Theorem 4.4.3): if the expected number of $k(n)$-cliques tends to $0$, then with high probability $G(n, 1/2)$ has no clique of size $k(n)$.

theorem CliqueNumber.clique_number_second_moment_bound (k : ℕ → ℕ) (hf : Filter.Tendsto (fun (n : ℕ) => expectedKCliques n (k n)) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => probCliqueGe n (k n)) Filter.atTop (nhds 1)

Second moment direction (Theorem 4.4.2): if the expected number of $k(n)$-cliques tends to infinity, then $G(n, 1/2)$ contains a $k(n)$-clique with probability tending to $1$.

theorem CliqueNumber.clique_number_two_point_concentration (k₀ : ℕ → ℕ) (hf_low : Filter.Tendsto (fun (n : ℕ) => expectedKCliques n (k₀ n - 1)) Filter.atTop Filter.atTop) (hf_high : Filter.Tendsto (fun (n : ℕ) => expectedKCliques n (k₀ n + 1)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => probCliqueGe n (k₀ n - 1) - probCliqueGe n (k₀ n + 1)) Filter.atTop (nhds 1)

Two-point concentration of the clique number (Theorem 4.4.3): if at $k_0(n) - 1$ the expected number of cliques diverges and at $k_0(n) + 1$ it tends to $0$, then with high probability the clique number of $G(n, 1/2)$ is exactly $k_0(n)$.