CoreGapBlowUp

Triangle hyperedges and their vertex sets

A hyperedge of Nibble.YusterE.triangleHypergraphE is the set of the three edges of a triangle. Nibble.AX1.vtxSet recovers the three vertices, so that sums over the triangle hypergraph can be rewritten as sums over cliqueFinset 3.

def Nibble.AX1.vtxSet {X : Type} [DecidableEq X] (T : Finset (Finset X)) : Finset X

The set of vertices covered by a set of edges.

Equations

• Nibble.AX1.vtxSet T = T.biUnion id

theorem Nibble.AX1.vtxSet_powersetCard_two {X : Type} [DecidableEq X] {t : Finset X} (ht : 2 ≤ t.card) : vtxSet (Finset.powersetCard 2 t) = t

The vertex set of the edge set of a set with at least two elements is the set itself.

theorem Nibble.AX1.sum_triangleHypergraphE {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (f : Finset (Finset V) → ℝ) : ∑ T ∈ YusterE.triangleHypergraphE G, f T = ∑ t ∈ G.cliqueFinset 3, f (Finset.powersetCard 2 t)

A sum over the triangle hypergraph is a sum over the triangles.

theorem Nibble.AX1.sum_triangleHypergraphE_filter {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {e : Finset V} (he : e.card = 2) (f : Finset (Finset V) → ℝ) : ∑ T ∈ YusterE.triangleHypergraphE G with e ∈ T, f T = ∑ t ∈ G.cliqueFinset 3 with e ⊆ t, f (Finset.powersetCard 2 t)

A sum over the triangle hyperedges through a fixed edge is a sum over the triangles containing that edge.

The blow-up

def Nibble.AX1.blowUp {W : Type} (H : SimpleGraph W) (q : ℕ) : SimpleGraph (W × Fin q)

The q-blow-up of H: every vertex is replaced by q copies, and two copies are adjacent exactly when the vertices they lie above are.

Equations

• Nibble.AX1.blowUp H q = SimpleGraph.comap Prod.fst H

@[instance_reducible]

instance Nibble.AX1.instDecidableRelBlowUpAdj {W : Type} (H : SimpleGraph W) [DecidableRel H.Adj] (q : ℕ) : DecidableRel (blowUp H q).Adj

Equations

• Nibble.AX1.instDecidableRelBlowUpAdj H q x y = Nibble.AX1.instDecidableRelBlowUpAdj._aux_1 H q x y

@[simp]

theorem Nibble.AX1.blowUp_adj {W : Type} {H : SimpleGraph W} {q : ℕ} {x y : W × Fin q} : (blowUp H q).Adj x y ↔ H.Adj x.1 y.1

theorem Nibble.AX1.isNClique_image_fst {W : Type} [DecidableEq W] {H : SimpleGraph W} {q : ℕ} {t' : Finset (W × Fin q)} (ht' : (blowUp H q).IsNClique 3 t') : H.IsNClique 3 (Finset.image Prod.fst t')

The projection of a triangle of the blow-up is a triangle of H.

theorem Nibble.AX1.card_blowUp_fiber {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (q : ℕ) {t : Finset W} (ht : H.IsNClique 3 t) : {t' ∈ (blowUp H q).cliqueFinset 3 | Finset.image Prod.fst t' = t}.card = q ^ 3

The fibre of the projection has q³ elements: a triangle of H is the projection of exactly q³ triangles of the blow-up.

theorem Nibble.AX1.card_blowUp_fiber_edge {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (q : ℕ) {t : Finset W} (ht : H.IsNClique 3 t) {x y : W × Fin q} (hne : x.1 ≠ y.1) (hx : x.1 ∈ t) (hy : y.1 ∈ t) : {t' ∈ (blowUp H q).cliqueFinset 3 | Finset.image Prod.fst t' = t ∧ {x, y} ⊆ t'}.card = q

The fibre of the projection through a fixed blow-up edge has q elements.

Lifting a fractional packing to the blow-up

noncomputable def Nibble.AX1.liftWeight {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (q : ℕ) (w : Finset (Finset W) → ℝ) : Finset (Finset (W × Fin q)) → ℝ

The lift of a weight function on the triangles of H to the triangles of the blow-up: the weight of a triangle is 1/q of the weight of the triangle below it.

Equations

• Nibble.AX1.liftWeight H q w T' = if T' ∈ Nibble.YusterE.triangleHypergraphE (Nibble.AX1.blowUp H q) then w (Finset.powersetCard 2 (Finset.image Prod.fst (Nibble.AX1.vtxSet T'))) / ↑q else 0

theorem Nibble.AX1.isFracPacking_liftWeight {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {q : ℕ} (hq : 0 < q) {w : Finset (Finset W) → ℝ} (hw : YusterE.IsFracPacking H w) : YusterE.IsFracPacking (blowUp H q) (liftWeight H q w)

The lift of a fractional packing is a fractional packing.

theorem Nibble.AX1.sum_liftWeight {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {q : ℕ} (hq : 0 < q) (w : Finset (Finset W) → ℝ) : ∑ T' ∈ YusterE.triangleHypergraphE (blowUp H q), liftWeight H q w T' = ↑q ^ 2 * ∑ T ∈ YusterE.triangleHypergraphE H, w T

The value of the lift is q² times the value.

theorem Nibble.AX1.nu3star_blowUp_ge {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {q : ℕ} (hq : 0 < q) : ↑q ^ 2 * YusterE.nu3star H ≤ YusterE.nu3star (blowUp H q)

The blow-up bound q²·ν₃*(H) ≤ ν₃*(H[q]).

theorem Nibble.AX1.blowUp_filter_pair {W : Type} [DecidableEq W] {H : SimpleGraph W} {q : ℕ} {a b : W} {t' : Finset (W × Fin q)} (ht' : (blowUp H q).IsNClique 3 t') (hsub : {a, b} ⊆ Finset.image Prod.fst t') : ∃ (i : Fin q) (j : Fin q), {v ∈ t' | v.1 = a ∨ v.1 = b} = {(a, i), (b, j)} ∧ {(a, i), (b, j)} ⊆ t'

A triangle of the blow-up whose projection contains the edge {a, b} contains exactly one vertex over a and one over b.

Projecting a fractional packing of the blow-up

noncomputable def Nibble.AX1.projWeight {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (q : ℕ) (w' : Finset (Finset (W × Fin q)) → ℝ) : Finset (Finset W) → ℝ

The projection of a weight function on the triangles of the blow-up: a triangle of H receives 1/q² of the total weight of the triangles above it.

Equations

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

theorem Nibble.AX1.isFracPacking_projWeight {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {q : ℕ} (hq : 0 < q) {w' : Finset (Finset (W × Fin q)) → ℝ} (hw' : YusterE.IsFracPacking (blowUp H q) w') : YusterE.IsFracPacking H (projWeight H q w')

The projection of a fractional packing is a fractional packing.

theorem Nibble.AX1.sum_projWeight {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {q : ℕ} (hq : 0 < q) (w' : Finset (Finset (W × Fin q)) → ℝ) : ↑q ^ 2 * ∑ T ∈ YusterE.triangleHypergraphE H, projWeight H q w' T = ∑ T' ∈ YusterE.triangleHypergraphE (blowUp H q), w' T'

The value of the projection is 1/q² of the value.

theorem Nibble.AX1.nu3star_blowUp_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {q : ℕ} (hq : 0 < q) : YusterE.nu3star (blowUp H q) ≤ ↑q ^ 2 * YusterE.nu3star H

The blow-up bound ν₃*(H[q]) ≤ q²·ν₃*(H).

theorem Nibble.AX1.nu3star_blowUp {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {q : ℕ} (hq : 0 < q) : YusterE.nu3star (blowUp H q) = ↑q ^ 2 * YusterE.nu3star H

The blow-up scaling of the fractional triangle packing number.

Axiom check

YusterBridgeFrac

def Nibble.YusterE.IsTriangleFracPacking {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (w : Finset V → ℝ) : Prop

PaperIII-style fractional triangle packing, with weights on vertex-sets.

Equations

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

theorem Nibble.YusterE.triangle_powersetCard_two_injOn {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Set.InjOn (fun (t : Finset V) => Finset.powersetCard 2 t) ↑(G.cliqueFinset 3)

Taking all two-element subsets is injective on triangles.

theorem Nibble.YusterE.triangle_powersetCard_two_sup {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {t : Finset V} (ht : G.IsNClique 3 t) : (Finset.powersetCard 2 t).sup id = t

The union of the two-element subsets of a triangle recovers its vertices.

theorem Nibble.YusterE.mem_powersetCard_two_iff_subset {V : Type u_1} {e t : Finset V} (he : e.card = 2) : e ∈ Finset.powersetCard 2 t ↔ e ⊆ t

For a two-element set e, membership among a triangle's edges is inclusion in the triangle.

theorem Nibble.YusterE.triangleHypergraphE_filter_eq_image {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (e : Finset V) (he : e.card = 2) : {T ∈ triangleHypergraphE G | e ∈ T} = Finset.image (fun (t : Finset V) => Finset.powersetCard 2 t) ({t ∈ G.cliqueFinset 3 | e ⊆ t})

Filtering the edge-set triangle hypergraph at an edge is the image of the vertex-set triangles containing that edge.

theorem Nibble.YusterE.sum_triangleHypergraphE_sup {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (w : Finset V → ℝ) : ∑ T ∈ triangleHypergraphE G, w (T.sup id) = ∑ t ∈ G.cliqueFinset 3, w t

Reindex the fractional objective from triangle vertex-sets to triangle edge-sets.

theorem Nibble.YusterE.sum_clique_powersetCard_two {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (w : Finset (Finset V) → ℝ) : ∑ t ∈ G.cliqueFinset 3, w (Finset.powersetCard 2 t) = ∑ T ∈ triangleHypergraphE G, w T

Reindex the fractional objective from triangle edge-sets to triangle vertex-sets.

theorem Nibble.YusterE.fracPacking_to_triangleFracPacking {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {w' : Finset (Finset V) → ℝ} (hw' : IsFracPacking G w') : (IsTriangleFracPacking G fun (t : Finset V) => w' (Finset.powersetCard 2 t)) ∧ ∑ t ∈ G.cliqueFinset 3, w' (Finset.powersetCard 2 t) = ∑ T ∈ triangleHypergraphE G, w' T

A fractional packing on triangle edge-sets transports to one on triangle vertex-sets, preserving its objective.

theorem Nibble.YusterE.triangleFracPacking_to_fracPacking {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {w : Finset V → ℝ} (hw : IsTriangleFracPacking G w) : have w' := fun (T : Finset (Finset V)) => if T ∈ triangleHypergraphE G then w (T.sup id) else 0; IsFracPacking G w' ∧ ∑ T ∈ triangleHypergraphE G, w' T = ∑ t ∈ G.cliqueFinset 3, w t

A fractional packing on triangle vertex-sets transports to one on triangle edge-sets, preserving its objective.

theorem Nibble.YusterE.nu3star_eq_triangleFrac_sSup {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : nu3star G = sSup {x : ℝ | ∃ (w : Finset V → ℝ), IsTriangleFracPacking G w ∧ x = ∑ t ∈ G.cliqueFinset 3, w t}

The Nibble edge-set fractional triangle-packing optimum is exactly the PaperIII-style optimum over weights on triangle vertex-sets.

CoreGapPackingSplit

def Nibble.AX1.partClass {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (t : Finset V) : Finset (Finset V)

The set of parts of P met by t. For a triangle of a regularity-reduced graph this is a triple of distinct parts.

Equations

• Nibble.AX1.partClass P t = Finset.image P.part t

theorem Nibble.AX1.mem_partClass_iff {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (t U : Finset V) : U ∈ partClass P t ↔ ∃ x ∈ t, P.part x = U

theorem Nibble.AX1.partClass_subset_parts {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (t : Finset V) : partClass P t ⊆ P.parts

theorem Nibble.AX1.partClass_mem_powersetCard_three {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) {t : Finset V} (h3 : (partClass P t).card = 3) : partClass P t ∈ Finset.powersetCard 3 P.parts

theorem Nibble.AX1.partClass_card_three_of_isNClique {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {t : Finset V} (ht : (SimpleGraph.regularityReduced P G ep de).IsNClique 3 t) : (partClass P t).card = 3

In a regularity-reduced graph every triangle meets exactly three parts: this is the hypothesis of Nibble.AX1.sum_split_partClass, discharged.

theorem Nibble.AX1.sum_split_partClass {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (f : Finset V → ℝ) (hdist : ∀ t ∈ G.cliqueFinset 3, (partClass P t).card = 3) : ∑ S ∈ Finset.powersetCard 3 P.parts, ∑ t ∈ G.cliqueFinset 3 with partClass P t = S, f t = ∑ t ∈ G.cliqueFinset 3, f t

The objective splits along the triples of parts. If every triangle of G meets three distinct parts of P — which is the case for a regularity-reduced graph, by Nibble.AX1.regularityReduced_triangle_parts — then the sum of any weight function over the triangles is the sum, over triples of parts, of its weight on that triple.

theorem Nibble.AX1.sum_pair_classes_le {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {w : Finset (Finset V) → ℝ} (hw : YusterE.IsFracPacking G w) (hdist : ∀ t ∈ G.cliqueFinset 3, (partClass P t).card = 3) {U W : Finset V} (hUW : U ≠ W) : ∑ S ∈ Finset.powersetCard 3 P.parts with U ∈ S ∧ W ∈ S, ∑ t ∈ G.cliqueFinset 3 with partClass P t = S, w (Finset.powersetCard 2 t) ≤ ↑(G.interedges U W).card

The per-pair LP constraint. For two distinct parts U ≠ W, a fractional triangle packing puts total weight at most e(U, W) on the triangles whose triple of parts contains both U and W.

CoreGapClusterHost

The cluster graph

def Nibble.AX1.hostGraph {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) : SimpleGraph ↥P.parts

The cluster graph of G along P at scales ep, de: the vertices are the parts of P and two distinct parts are joined when the pair is ep-uniform of density at least de.

Equations

• Nibble.AX1.hostGraph G P ep de = { Adj := fun (S T : ↥P.parts) => ↑S ≠ ↑T ∧ G.IsUniform ep ↑S ↑T ∧ de ≤ ↑(G.edgeDensity ↑S ↑T), symm := ⋯, loopless := ⋯ }

@[instance_reducible]

noncomputable instance Nibble.AX1.hostGraph.instDecidableRelAdj {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) : DecidableRel (hostGraph G P ep de).Adj

Equations

• Nibble.AX1.hostGraph.instDecidableRelAdj G P ep de = Classical.decRel (Nibble.AX1.hostGraph G P ep de).Adj

theorem Nibble.AX1.hostGraph_adj {V : Type} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {P : Finpartition Finset.univ} {ep de : ℝ} {S T : ↥P.parts} : (hostGraph G P ep de).Adj S T ↔ ↑S ≠ ↑T ∧ G.IsUniform ep ↑S ↑T ∧ de ≤ ↑(G.edgeDensity ↑S ↑T)

theorem Nibble.AX1.card_hostGraph_vertices {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) : Fintype.card ↥P.parts = P.parts.card

The number of vertices of the cluster graph is the number of clusters.

def Nibble.AX1.clusterOf {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (v : V) : ↥P.parts

The cluster of a vertex, as a vertex of the cluster graph.

Equations

• Nibble.AX1.clusterOf P v = ⟨P.part v, ⋯⟩

def Nibble.AX1.hostTri {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (t : Finset V) : Finset ↥P.parts

The cluster triple of a triangle.

Equations

• Nibble.AX1.hostTri P t = Finset.image (Nibble.AX1.clusterOf P) t

theorem Nibble.AX1.image_hostTri {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) (t : Finset V) : Finset.image Subtype.val (hostTri P t) = partClass P t

theorem Nibble.AX1.hostTri_mem_cliqueFinset {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {t : Finset V} (ht : t ∈ (SimpleGraph.regularityReduced P G ep de).cliqueFinset 3) : hostTri P t ∈ (hostGraph G P ep de).cliqueFinset 3

A triangle of a regularity-reduced graph has a cluster triple that is a triangle of the cluster graph at the same scales.

theorem Nibble.AX1.exists_edge_of_mem_hostTri {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) {t : Finset V} {S T : ↥P.parts} (hST : S ≠ T) (hS : S ∈ hostTri P t) (hT : T ∈ hostTri P t) : ∃ x ∈ ↑S, ∃ y ∈ ↑T, {x, y} ∈ Finset.powersetCard 2 t

Two clusters of the cluster triple of a triangle are joined by an edge of the triangle.

The aggregation

theorem Nibble.AX1.nu3star_regularityReduced_le_host {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {c : ℝ} (hc : 0 < c) (hcap : ∀ S ∈ P.parts, ∀ T ∈ P.parts, S ≠ T → ↑(G.interedges S T).card ≤ c) : YusterE.nu3star (SimpleGraph.regularityReduced P G ep de) ≤ c * YusterE.nu3star (hostGraph G P ep de)

Aggregating the LP along the cluster triples. If every cluster pair of P carries at most c edges of G, then the fractional triangle packing number of the regularity-reduced graph is at most c times that of the cluster graph.

The aggregated weighting gives a cluster triple the total weight of the triangles lying on it, scaled by 1/c; the capacity constraint of a cluster pair (Nibble.AX1.sum_fracPacking_cluster_pair_le) is exactly the edge constraint of the aggregate.

Axiom check