Monochromatic $k$ -sets: pair-count bound

Proved

Erdos1947.mono_pair_count_le

by sr · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

double-countingprobabilistic-methodramsey-theory

The double-counting bound over all graphs on $N$ vertices. The total number of pairs $(G, s)$ with $s$ a monochromatic $k$ -set in $G$ is at most

\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.

A fixed $k$ -set $s$ is monochromatic in exactly those graphs in which the $\binom{k}{2}$ edges inside $s$ are all present or all absent, while the remaining edges are arbitrary. This is the mass of the "bad events" that the union-bound principle consumes, and it is precisely the quantity that the count estimate bounds below $2^{\binom{N}{2}}$ , the number of all graphs.

Preamble

import Mathlib
import Definitions.Def_erdos1947

Formal statement

namespace Erdos1947

open scoped BigOperators

/-- **Double-counting bound.** Over all graphs on `N` vertices, the total number
of pairs `(G, s)` with `s` a monochromatic `k`-set in `G` is at most

$$\binom{N}{k} \cdot 2^{1 + \binom{N}{2} - \binom{k}{2}}.$$

Reason: a fixed `k`-set is monochromatic in exactly the graphs that make it a
clique or an independent set — all edges inside it are determined (all or none),
the remaining edges are free. -/
theorem mono_pair_count_le (N k : ℕ) :
    (Finset.univ : Finset (SimpleGraph (Fin N))).sum
        (fun G : SimpleGraph (Fin N) => monoCount N k G) ≤
      Nat.choose N k * 2 ^ (1 + Nat.choose N 2 - Nat.choose k 2) := by
  sorry

end Erdos1947

Source

Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4) (1947) 292–294, https://doi.org/10.1090/S0002-9904-1947-08785-X — main construction (the lower bound R(k) > 2^(k/2)).

Human review

Endorsed by Shuze Chen · Sep 5, 2026
Endorsed by sr · Sep 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Monochromatic kkk-sets: pair-count bound

Monochromatic $k$ -sets: pair-count bound