CoreGapPackingEdges #
theorem
Nibble.AX1.sum_fracPacking_over_edges_le
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
{w : Finset (Finset V) → ℝ}
(hw : YusterE.IsFracPacking G w)
(E : Finset (Finset V))
:
The LP weight on the triangles through a set of edges is at most the number of edges.
Each triangle counted on the left contains at least one e ∈ E, and the packing constraint at e
caps the weight through e by 1.
theorem
Nibble.AX1.nu3star_le_of_edgeCover
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(E : Finset (Finset V))
(hcov : ∀ T ∈ YusterE.triangleHypergraphE G, ∃ e ∈ E, e ∈ T)
:
A triangle edge cover bounds ν₃*. If every triangle of G uses an edge from E, then
ν₃*(G) ≤ #E. (With E the whole edge set this is weaker than Nibble.YusterE.nu3star_le; the
point is the localised version, applied to the edges between two clusters.)