CoreGapRegularCover

The triangle support

noncomputable def Nibble.AX1.triangleSupport {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : SimpleGraph V

The spanning subgraph of the edges of G that lie in at least one triangle.

Equations

• Nibble.AX1.triangleSupport G = Nibble.AX1.edgeSelect G fun (e : Finset V) => 0 < Nibble.AX1.edgeTriangleDegree G e

@[instance_reducible]

noncomputable instance Nibble.AX1.instDecidableRelTriangleSupport {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : DecidableRel (triangleSupport G).Adj

Equations

• Nibble.AX1.instDecidableRelTriangleSupport G = Nibble.AX1.instDecidableRelEdgeSelect G fun (e : Finset V) => 0 < Nibble.AX1.edgeTriangleDegree G e

theorem Nibble.AX1.triangleSupport_le {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : triangleSupport G ≤ G

theorem Nibble.AX1.cliqueFinset_three_triangleSupport {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (triangleSupport G).cliqueFinset 3 = G.cliqueFinset 3

The triangle support has the same triangles as G: each edge of a triangle lies in one.

theorem Nibble.AX1.nu3star_congr_hypergraph {V : Type} [Fintype V] [DecidableEq V] (G₁ G₂ : SimpleGraph V) [DecidableRel G₁.Adj] [DecidableRel G₂.Adj] (h : YusterE.triangleHypergraphE G₁ = YusterE.triangleHypergraphE G₂) : YusterE.nu3star G₁ = YusterE.nu3star G₂

Equal triangle hypergraphs give equal fractional optima.

theorem Nibble.AX1.nu3star_triangleSupport {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : YusterE.nu3star (triangleSupport G) = YusterE.nu3star G

The triangle support carries the whole fractional optimum.

The union of a family

def Nibble.AX1.unionFamily {V : Type} (H : ℕ → SimpleGraph V) (k : ℕ) : SimpleGraph V

The union of the first k members of a family of graphs.

Equations

• Nibble.AX1.unionFamily H k = { Adj := fun (x y : V) => ∃ i < k, (H i).Adj x y, symm := ⋯, loopless := ⋯ }

@[instance_reducible]

noncomputable instance Nibble.AX1.instDecidableRelUnionFamily {V : Type} (H : ℕ → SimpleGraph V) (k : ℕ) : DecidableRel (unionFamily H k).Adj

Equations

• Nibble.AX1.instDecidableRelUnionFamily H k x✝¹ x✝ = Classical.dec ((Nibble.AX1.unionFamily H k).Adj x✝¹ x✝)

theorem Nibble.AX1.unionFamily_le {V : Type} {G : SimpleGraph V} {H : ℕ → SimpleGraph V} {k : ℕ} (hle : ∀ i < k, H i ≤ G) : unionFamily H k ≤ G

theorem Nibble.AX1.cliqueFinset_two_unionFamily {V : Type} [Fintype V] [DecidableEq V] (H : ℕ → SimpleGraph V) (k : ℕ) : (unionFamily H k).cliqueFinset 2 = (Finset.range k).biUnion fun (i : ℕ) => (H i).cliqueFinset 2

The 2-cliques of a union are the union of the 2-cliques.

theorem Nibble.AX1.card_cliqueFinset_two_unionFamily {V : Type} [Fintype V] [DecidableEq V] (H : ℕ → SimpleGraph V) (k : ℕ) (hdisj : EdgeDisjointFamily H k) : ↑((unionFamily H k).cliqueFinset 2).card = ∑ i ∈ Finset.range k, ↑((H i).cliqueFinset 2).card

For an edge-disjoint family, the edge count of the union is the sum of the edge counts.

The covering criterion

theorem Nibble.AX1.hasNearRegularFamily_of_cover {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε μ η d₀ : ℝ} {k : ℕ} {H : ℕ → SimpleGraph V} {d : ℕ → ℝ} {D : Finset (Finset V)} (hle : ∀ i < k, H i ≤ triangleSupport G) (hdisj : EdgeDisjointFamily H k) (hd : ∀ i < k, d₀ ≤ d i) (hhi : ∀ i < k, ∀ e ∈ (H i).cliqueFinset 2, ↑(edgeTriangleDegree (H i) e) ≤ (1 + μ) * d i) (hlo : ∀ i < k, ∃ (Exc : Finset (Finset V)), ↑Exc.card ≤ η * ↑((H i).cliqueFinset 2).card ∧ ∀ e ∈ (H i).cliqueFinset 2, e ∉ Exc → (1 - μ) * d i ≤ ↑(edgeTriangleDegree (H i) e)) (hcov : ∀ e ∈ (triangleSupport G).cliqueFinset 2, e ∈ D ∨ ∃ i < k, e ∈ (H i).cliqueFinset 2) (hD : ↑D.card ≤ ε * ↑(Fintype.card V) ^ 2) : HasNearRegularFamily G ε μ η d₀

The covering criterion. An edge-disjoint family of near-regular subgraphs of the triangle support of G, covering all but at most ε|V|² of the edges of that support, is a near-regular family for G in the sense of Nibble.AX1.HasNearRegularFamily.

Indeed the fractional optimum of G is that of its triangle support (Nibble.AX1.nu3star_triangleSupport); passing from the support to the union of the family costs at most the number of uncovered edges (Nibble.AX1.nu3star_le_add_deleted); and the fractional optimum of the union is at most a third of its edge count (Nibble.YusterE.nu3star_le), which for an edge-disjoint family is a third of the sum of the members' edge counts.

The cluster structure of a regularity-reduced graph

def Nibble.AX1.GoodTriple {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) (U W X : Finset V) : Prop

A good triple of clusters: three distinct parts of P, pairwise ep-uniform in G with density at least de. These are the triples that can carry a triangle of the reduced graph.

Equations

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

theorem Nibble.AX1.regularityReduced_triangle_parts {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {x y z : V} (hxy : (SimpleGraph.regularityReduced P G ep de).Adj x y) (hxz : (SimpleGraph.regularityReduced P G ep de).Adj x z) (hyz : (SimpleGraph.regularityReduced P G ep de).Adj y z) : ∃ (U : Finset V) (W : Finset V) (X : Finset V), GoodTriple G P ep de U W X ∧ x ∈ U ∧ y ∈ W ∧ z ∈ X

Every triangle of a regularity-reduced graph lives on a good triple of clusters: its three vertices lie in three distinct parts, which are pairwise uniform and dense.

theorem Nibble.AX1.triangleSupport_regularityReduced_goodTriple {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {x y : V} (hxy : (triangleSupport (SimpleGraph.regularityReduced P G ep de)).Adj x y) : ∃ (U : Finset V) (W : Finset V) (X : Finset V) (z : V), GoodTriple G P ep de U W X ∧ x ∈ U ∧ y ∈ W ∧ z ∈ X ∧ (SimpleGraph.regularityReduced P G ep de).Adj x z ∧ (SimpleGraph.regularityReduced P G ep de).Adj y z

Every edge that the covering residual has to cover lies on a good triple. An edge of the triangle support of a regularity-reduced graph joins two clusters of a good triple, the third cluster containing a common neighbour.

Why the covering criterion is not the residual

Nibble.AX1.hasNearRegularFamily_of_cover is a sufficient condition, and it is strictly stronger than what is needed: requiring that all but ε|V|² of the triangle-carrying edges be covered by near-regular classes is in general impossible. Near-regularity forces a class inside a cluster triple to carry roughly equally many edges in each of the triple's three pairs (the triangles of the class are counted once from each pair), so a triple whose three pairs have very different densities — say 1, 1/10, 1/10 — can have only about 3/10 of its edges covered, the rest of the dense pair remaining uncovered even though each of its edges lies in a triangle. For such a graph the fractional optimum is correspondingly small, which is exactly why Nibble.AX1.HasNearRegularFamily (and hence the residual Nibble.AX1.ReducedFamilyResidual) compares the covered edge count with ν₃* rather than with the total number of edges.

The covering criterion remains useful as a tool: applied to a subgraph G' ≤ G together with Nibble.AX1.HasNearRegularFamily.mono_of_le, it discharges the ν₃* bookkeeping whenever the construction does cover the chosen subgraph.