def RamseyAlteration.alterationBound (n k : ℕ) : ℕ

The alteration bound: expected number of monochromatic $k$-cliques in a uniformly random 2-coloring of $K_n$, namely $\binom{n}{k} \cdot 2 / 2^{\binom{k}{2}}$.

theorem RamseyAlteration.exists_le_div {α : Type u_1} [Fintype α] [Nonempty α] (f : α → ℕ) (total : ℕ) (hsum : ∑ x : α, f x ≤ total) : ∃ (x : α), f x ≤ total / Fintype.card α

Averaging principle: if $\sum_x f(x) \le \text{total}$ over a nonempty finite type, then some $x$ satisfies $f(x) \le \text{total} / |\alpha|$.

theorem RamseyAlteration.sum_indicator_eq_monoSet (n : ℕ) (S : Finset (Fin n)) (b : Bool) : (∑ c : RamseyLowerBound.Edge n → Bool, if ∀ e ∈ RamseyLowerBound.edgesWithin n S, c e = b then 1 else 0) = 2 ^ (n.choose 2 - S.card.choose 2)

Counting indicator sums over colorings: the number of colorings making $S$ monochromatic with value $b$ equals $2^{\binom{n}{2} - \binom{|S|}{2}}$.

theorem RamseyAlteration.total_div_card_eq (n k : ℕ) (hkn : k ≤ n) : n.choose k * 2 * 2 ^ (n.choose 2 - k.choose 2) / Fintype.card (RamseyLowerBound.Edge n → Bool) = alterationBound n k

Simplification: dividing $\binom{n}{k} \cdot 2 \cdot 2^{\binom{n}{2} - \binom{k}{2}}$ by the total number of 2-colorings gives the alteration bound.

theorem RamseyAlteration.exists_coloring_few_mono (n k : ℕ) (hk : 2 ≤ k) (hkn : k ≤ n) : ∃ (c : RamseyLowerBound.Edge n → Bool), {S ∈ Finset.powersetCard k Finset.univ | (∀ e ∈ RamseyLowerBound.edgesWithin n S, c e = true) ∨ ∀ e ∈ RamseyLowerBound.edgesWithin n S, c e = false}.card ≤ alterationBound n k

By averaging, there exists a 2-coloring of $K_n$ with at most alterationBound n k monochromatic $k$-subsets.

theorem RamseyAlteration.ramsey_alteration_bound (n k : ℕ) (hk : 2 ≤ k) (hkn : k ≤ n) : ∃ m ≥ n - alterationBound n k, ∃ (G : SimpleGraph (Fin m)), G.CliqueFree k ∧ Gᶜ.CliqueFree k

(Theorem 1.1.6, Ramsey lower bound via the alteration method) For every $n, k$ with $k \le n$, there exists an $m \ge n - \text{alterationBound}(n, k)$ and a graph on $m$ vertices with no $k$-clique in $G$ or in $G^c$.