CoreGapUniformCodegree #
Counting edges fibrewise #
The number of edges between two finsets is the sum over the first of the degrees into the second.
The edge density as a real number.
The one-sided degree lemmas #
Few vertices have small degree into a large subset. If (B, C) is ε-uniform and
C' ⊆ C has |C'| ≥ ε|C|, then at most ε|B| vertices y ∈ B have fewer than θ|C'|
neighbours in C', for any θ ≤ d(B,C) − ε.
Few vertices have large degree into a large subset. The mirror image of
Nibble.AX1.card_filter_lt_le.
Ingredient 1: near-regular triangle degrees across a uniform triple #
The number of common neighbours of x and y inside C.
Instances For
Ingredient 1 — per-edge triangle counting in a uniform triple. If (A, C) and (B, C)
are ε-uniform pairs of density at least 2ε, then all but at most 4ε|A||B| of the pairs
(x, y) ∈ A × B have
(d(A,C) − ε)(d(B,C) − 2ε)|C| ≤ |N(x) ∩ N(y) ∩ C| ≤ (d(A,C) + ε)(d(B,C) + 2ε)|C|,
i.e. the triangle degree of an edge of the pair (A, B) into C is already near-regular, at the
scale d(A,C)·d(B,C)·|C|.
The proof is the standard two-sided count: all but 2ε|A| vertices x ∈ A have
|N(x) ∩ C| = (d(A,C) ± ε)|C| (Nibble.AX1.card_filter_lt_le with C' = C), and for such an x
the set N(x) ∩ C is large enough that uniformity of (B, C) applies to it, so all but 2ε|B|
vertices y ∈ B have |N(y) ∩ N(x) ∩ C| = (d(B,C) ± 2ε)|N(x) ∩ C|.
CoreGapTripleDegrees #
The triangle degree of an edge is a codegree #
The triangle degree of an edge is the number of common neighbours of its endpoints.
The tripartite graph carried by a triple of parts #
The tripartite subgraph carried by a triple of parts: the edges of G joining two
different parts of (U, W, X).
Equations
- Nibble.AX1.tripleGraph G U W X = { Adj := fun (x y : V) => G.Adj x y ∧ Nibble.AX1.crossAdj U W X x y, symm := ⋯, loopless := ⋯ }
Instances For
Equations
- Nibble.AX1.instDecidableRelTripleGraph G U W X x✝¹ x✝ = Classical.dec ((Nibble.AX1.tripleGraph G U W X).Adj x✝¹ x✝)
The tripartite graph does not depend on the order of the three parts.
The tripartite graph does not depend on the order of the three parts.
The triangle degree of a U–W edge of the triple is the codegree into X.
Near-regular triangle degrees on one pair of the triple #
Ingredient 1, in triangle-degree form. If the pairs (U, X) and (W, X) are ε-uniform
of density at least 2ε, then all but at most 4ε|U||W| of the edges of tripleGraph G U W X
joining U to W have triangle degree (d(U,X) ± ε)(d(W,X) ± 2ε)|X|.
The equalised triple #
Near-regular triangle degrees on a whole cluster triple. Suppose the three pairs of the
triple (U, W, X) are ε-uniform of density at least 2ε, and that the three triangle-degree
scales d(U,X)d(W,X)|X| (for the U–W edges), d(U,W)d(W,X)|W| (for the U–X edges) and
d(U,W)d(U,X)|U| (for the W–X edges) all lie in [(1−μ)d, (1+μ)d], even after the ε-slack of
Nibble.AX1.tripleGraph_near_regular_pair is taken into account. Then all but at most
4ε(|U||W| + |U||X| + |W||X|) of the edges of the tripartite graph tripleGraph G U W X have
triangle degree in [(1−μ)d, (1+μ)d].
This is the near-regular member the Haxell–Rödl construction attaches to a cluster triple, before the exceptional edges are deleted; the equalisation hypotheses are what the sparsification of the three pairs to a common density is for.