Adapted from jtraverso/turan-stability (Palomar-registered source).

The clique counting lemma

This file generalises Mathlib's triangle counting lemma (SimpleGraph.triangle_counting', SimpleGraph.triangle_counting) from triangles to cliques of any size r.

The parts are given by a family s : Fin r → Finset α. A tuple x with x i ∈ s i for every i is a transversal clique if G.Adj (x i) (x j) for all i ≠ j.

• CliqueCounting.card_transversalCliques_ge: counting lemma, robust-density form. If, for all i ≠ j, every pair of subsets A ⊆ s i, B ⊆ s j with #A ≥ η #(s i) and #B ≥ η #(s j) has edge density at least d, η ≤ 1 and 2 r η ≤ d ^ (r - 1), then at least d ^ (r choose 2) / 2 ^ r · ∏ i, #(s i) tuples are transversal cliques.
• CliqueCounting.card_transversalCliques_ge_of_isUniform: counting lemma, uniform form. The same conclusion when every pair (s i, s j) is ε-uniform (SimpleGraph.IsUniform) with edge density at least d + ε, and 2 r ε ≤ d ^ (r - 1).
• CliqueCounting.card_cliqueFinset_ge: clique counting lemma. For pairwise disjoint parts the same lower bound holds for the number of r-cliques of G, #(G.cliqueFinset r).

theorem CliqueCounting.card_badVertices_lt {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] {η d : ℝ} (hd : 0 < d) {S T : Finset α} (hT : η * ↑T.card ≤ ↑T.card) (h : ∀ A ⊆ S, η * ↑S.card ≤ ↑A.card → η * ↑T.card ≤ ↑T.card → d ≤ ↑(G.edgeDensity A T)) : ↑{x ∈ S | ↑{y ∈ T | G.Adj x y}.card < d * ↑T.card}.card < η * ↑S.card

Vertices of S with fewer than d · #T neighbours in T form a set of size < η · #S, provided all large subsets of S have density at least d to T.

def CliqueCounting.CountingStatement {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] (r : ℕ) : Prop

The statement of the counting lemma for r parts, with the extra hypothesis η ≤ 1.

Equations

• One or more equations did not get rendered due to their size.

theorem CliqueCounting.countingStatement_of_le_one {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] {r : ℕ} (hr : r ≤ 1) : CountingStatement G r

theorem CliqueCounting.countingStatement_succ {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] {r : ℕ} (hr : 1 ≤ r) (ih : CountingStatement G r) : CountingStatement G (r + 1)

theorem CliqueCounting.countingStatement {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] (r : ℕ) : CountingStatement G r

theorem CliqueCounting.card_transversalCliques_ge {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] {r : ℕ} (s : Fin r → Finset α) {η d : ℝ} (hη : 0 < η) (hη₁ : η ≤ 1) (hd : 0 < d) (hηd : 2 * ↑r * η ≤ d ^ (r - 1)) (hs : ∀ (i j : Fin r), i ≠ j → ∀ A ⊆ s i, ∀ B ⊆ s j, η * ↑(s i).card ≤ ↑A.card → η * ↑(s j).card ≤ ↑B.card → d ≤ ↑(G.edgeDensity A B)) : d ^ r.choose 2 / 2 ^ r * ∏ i : Fin r, ↑(s i).card ≤ ↑{x ∈ Fintype.piFinset s | ∀ (i j : Fin r), i ≠ j → G.Adj (x i) (x j)}.card

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.)

theorem CliqueCounting.card_transversalCliques_ge_of_isUniform {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] {r : ℕ} (s : Fin r → Finset α) {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hεd : 2 * ↑r * ε ≤ d ^ (r - 1)) (hu : ∀ (i j : Fin r), i ≠ j → G.IsUniform ε (s i) (s j)) (hdens : ∀ (i j : Fin r), i ≠ j → d + ε ≤ ↑(G.edgeDensity (s i) (s j))) : d ^ r.choose 2 / 2 ^ r * ∏ i : Fin r, ↑(s i).card ≤ ↑{x ∈ Fintype.piFinset s | ∀ (i j : Fin r), i ≠ j → G.Adj (x i) (x j)}.card

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.

theorem CliqueCounting.card_cliqueFinset_ge {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] [Fintype α] [DecidableEq α] {r : ℕ} (s : Fin r → Finset α) {ε d : ℝ} (hε : 0 < ε) (hd : 0 < d) (hεd : 2 * ↑r * ε ≤ d ^ (r - 1)) (hdisj : ∀ (i j : Fin r), i ≠ j → Disjoint (s i) (s j)) (hu : ∀ (i j : Fin r), i ≠ j → G.IsUniform ε (s i) (s j)) (hdens : ∀ (i j : Fin r), i ≠ j → d + ε ≤ ↑(G.edgeDensity (s i) (s j))) : d ^ r.choose 2 / 2 ^ r * ∏ i : Fin r, ↑(s i).card ≤ ↑(G.cliqueFinset r).card

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.