Adapted from jtraverso/turan-stability (Palomar-registered source).
Proofs of the statements in Challenge.lean #
The proofs are in StabilityLib/: Furedi.lean (Füredi's greedy maximum-degree partition and
Mathlib's Turán bound), CliqueCounting.lean (induction on the clique size with good
neighbourhoods, generalising Mathlib's triangle counting lemma), CliqueRemoval.lean (Szemerédi's
regularity lemma and Mathlib's reduced graph, generalising Mathlib's triangle removal lemma),
Embedding.lean (greedy embedding) and StabilityGeneral.lean (the reduced graph of an L-free
graph is K_{p+1}-free by the embedding lemma, and Füredi's theorem applied to it).
Füredi's partition inequality. Every K_{p+1}-free finite graph has a partition into
p parts (the fibres of f) such that the number of edges of G plus the number of edges of
G inside the parts is at most the number of edges of the complete p-partite graph on these
parts.
Füredi's theorem (2015). If G is a K_{p+1}-free graph on n vertices with at least
turanNumber n p - t edges, then G has a p-colourable (i.e. p-partite) subgraph H with
at least e(G) - t edges.
Füredi's theorem, edit-distance form. Under the hypotheses of furedi, there is a
partition into p parts with at most t edges of G inside the parts, and G differs from the
complete p-partite graph on these parts in at most 3 t edges.
Erdős–Simonovits stability theorem for cliques (Erdős 1967, Simonovits 1968), in the
form obtained from Füredi's theorem: for every ε > 0 there is δ > 0 such that every
K_{p+1}-free graph on n vertices with at least (1 - 1/p) n² / 2 - δ n² edges differs from
some complete p-partite graph on the same vertices in at most ε n² edges.
Clique counting lemma, robust-density form. If any two of the parts s i, s j
(i ≠ j) have edge density at least d between all subsets of relative size at least η,
η ≤ 1 and 2 r η ≤ d ^ (r - 1), then at least d ^ (r choose 2) / 2 ^ r of the tuples in
∏ i, s i are cliques. (Without η ≤ 1 the hypothesis on subsets would be vacuous.)
Clique counting lemma, uniform form. If every pair of distinct parts is ε-uniform with
edge density at least d + ε, and 2 r ε ≤ d ^ (r - 1), then at least
d ^ (r choose 2) / 2 ^ r of the tuples in ∏ i, s i are cliques.
Clique counting lemma. If s : Fin r → Finset α are pairwise disjoint sets of vertices,
every two of them ε-uniform with edge density at least d + ε, and 2 r ε ≤ d ^ (r - 1),
then G has at least d ^ (r choose 2) / 2 ^ r · ∏ i, #(s i) cliques of size r.
Clique removal lemma, far form. For every r and ε > 0 there is δ > 0 such that a
finite graph on n vertices that is ε n²-far from being K_r-free (in the sense of Mathlib's
SimpleGraph.DeleteFar) has at least δ n^r cliques of size r.
Clique removal lemma. For every r and ε > 0 there is δ > 0 such that every finite
graph on n vertices with fewer than δ n^r cliques of size r has a K_r-free subgraph
obtained by deleting fewer than ε n² edges.
Embedding lemma, robust-density form. Let L be a graph on a finite type β with
k = card β vertices and a proper colouring c : β → Fin r. Suppose that for all colours
i ≠ j, all subsets A ⊆ s i, B ⊆ s j with #A ≥ η #(s i) and #B ≥ η #(s j) have edge
density at least d, where 0 < η ≤ 1, 0 < d ≤ 1, 2 k η ≤ d ^ k, and every part has at least
2 k / d ^ k vertices. Then there is an injective map f : β → α sending each x into s (c x)
and edges of L to edges of G.
Embedding lemma, uniform form. Under the hypotheses of exists_embedding, with the
robust density condition replaced by: every pair of distinct parts is ε-uniform with edge
density at least d + ε, and 2 k ε ≤ d ^ k.
Embedding lemma, containment form. Under the hypotheses of
exists_embedding_of_isUniform, L is contained in G (L ⊑ G, Mathlib's
SimpleGraph.IsContained).
Erdős–Simonovits stability theorem. Let L be a finite graph that is
(p + 1)-colourable. For every ε > 0 there are δ > 0 and n₀ such that every graph G on
n ≥ n₀ vertices that does not contain L and has at least (1 - 1/p) n² / 2 - δ n² edges
differs from some complete p-partite graph on the same vertices in at most ε n² edges.