K₄ counting in Dross's deficient-cut argument

def LeanPool.DrossFractionalTriangleDecomposition.codeg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) : ℕ

T_e — the number of triangles through the edge uv, i.e. the common neighbours of u and v.

Equations

• LeanPool.DrossFractionalTriangleDecomposition.codeg G u v = (G.neighborFinset u ∩ G.neighborFinset v).card

noncomputable def LeanPool.DrossFractionalTriangleDecomposition.numK4Through {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u v : V) : ℕ

The number of K₄'s containing edge uv: edges of G both of whose endpoints are common neighbours of u and v (each such edge {w,x} completes {u,v,w,x} to a K₄).

Equations

• LeanPool.DrossFractionalTriangleDecomposition.numK4Through G u v = {e ∈ G.edgeFinset | ∀ x ∈ e, x ∈ G.neighborFinset u ∩ G.neighborFinset v}.card

theorem LeanPool.DrossFractionalTriangleDecomposition.k4_lower_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {u v : V} (d : ℕ) (hd : ∀ (w : V), Fintype.card V - G.degree w ≤ d) : codeg G u v * (codeg G u v - d) ≤ 2 * numK4Through G u v

A6 — K₄ counting lower bound. If every vertex fails to be adjacent to at most d other vertices (the complement of the min-degree hypothesis δ(G) ≥ |V| − d), then the edge uv lies in at least T_e·(T_e − d)/2 copies of K₄.