CoreGapClusterCapacity

noncomputable def Nibble.AX1.crossEdges {V : Type} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (U W : Finset V) : Finset (Finset V)

The edges of G crossing the pair (U, W), as vertex sets.

Equations

• Nibble.AX1.crossEdges G U W = Finset.image (fun (p : V × V) => {p.1, p.2}) (G.interedges U W)

theorem Nibble.AX1.card_crossEdges_le {V : Type} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (U W : Finset V) : (crossEdges G U W).card ≤ (G.interedges U W).card

theorem Nibble.AX1.mem_crossEdges_of_mem_triangle {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {U W : Finset V} {T : Finset (Finset V)} (hT : T ∈ YusterE.triangleHypergraphE G) {x y : V} (hx : x ∈ U) (hy : y ∈ W) (hxy : {x, y} ∈ T) : {x, y} ∈ crossEdges G U W

An edge of a triangle of G joining U to W is one of the U–W edges.

theorem Nibble.AX1.sum_fracPacking_cluster_pair_le {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {w : Finset (Finset V) → ℝ} (hw : YusterE.IsFracPacking G w) (U W : Finset V) : ∑ T ∈ YusterE.triangleHypergraphE G with ∃ x ∈ U, ∃ y ∈ W, {x, y} ∈ T, w T ≤ ↑(G.interedges U W).card

The capacity constraint of a cluster pair. A fractional triangle packing puts total weight at most the number of U–W edges on the triangles that use one.

theorem Nibble.AX1.nu3star_le_of_clusterPairCover {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {k : ℕ} (U W : ℕ → Finset V) (hcov : ∀ T ∈ YusterE.triangleHypergraphE G, ∃ i < k, ∃ x ∈ U i, ∃ y ∈ W i, {x, y} ∈ T) : YusterE.nu3star G ≤ ∑ i ∈ Finset.range k, ↑(G.interedges (U i) (W i)).card

The ν₃* form of the capacity constraint. If every triangle of G uses an edge crossing one of the cluster pairs (U i, W i), i < k, then ν₃*(G) is at most the total number of edges across those pairs.