Documentation

LeanPool.DrossFractionalTriangleDecomposition.Basic

Fractional triangle decompositions #

The edge weights in the decomposition equation are exactly one. This is the public statement model for the Dross threshold; auxiliary flow and cut structures remain internal.

source
def LeanPool.DrossFractionalTriangleDecomposition.triEdges {V : Type u_1} [DecidableEq V] (t : Finset V) :
Finset (Sym2 V)

The non-loop edges spanned by a finite set of vertices.

Equations
Instances For
    source
    theorem LeanPool.DrossFractionalTriangleDecomposition.triEdges_card_of_isNClique {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {t : Finset V} (ht : G.IsNClique 3 t) :
    (triEdges t).card = 3

    A triangle has three edges.

    source
    theorem LeanPool.DrossFractionalTriangleDecomposition.triEdges_subset_edgeFinset {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {t : Finset V} (ht : t ∈ G.cliqueFinset 3) :
    triEdges t ⊆ G.edgeFinset

    Every edge of a graph triangle belongs to the graph.

    source
    def LeanPool.DrossFractionalTriangleDecomposition.FractionalTriangleDecomp {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
    Prop

    Nonnegative weights on triangles which give every graph edge total weight one.

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