Dross's auxiliary network

The nodes are graph edges, a source, and a sink. We use Lean Pool's existing finite max-flow/min-cut structures rather than porting a second copy of that development.

def LeanPool.DrossFractionalTriangleDecomposition.triThrough {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (e : Sym2 V) : ℕ

The number of graph triangles containing an edge.

Equations

• LeanPool.DrossFractionalTriangleDecomposition.triThrough G e = {t ∈ G.cliqueFinset 3 | e ∈ LeanPool.DrossFractionalTriangleDecomposition.triEdges t}.card

inductive LeanPool.DrossFractionalTriangleDecomposition.Ghat (V : Type u_2) : Type u_2

An edge node, source, or sink in Dross's auxiliary network.

• src {V : Type u_2} : Ghat V
• snk {V : Type u_2} : Ghat V
• edge {V : Type u_2} : Sym2 V → Ghat V

def LeanPool.DrossFractionalTriangleDecomposition.instDecidableEqGhat.decEq {V✝ : Type u_2} [DecidableEq V✝] (x✝ x✝¹ : Ghat V✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.DrossFractionalTriangleDecomposition.instDecidableEqGhat.decEq LeanPool.DrossFractionalTriangleDecomposition.Ghat.src LeanPool.DrossFractionalTriangleDecomposition.Ghat.src = isTrue ⋯
• LeanPool.DrossFractionalTriangleDecomposition.instDecidableEqGhat.decEq LeanPool.DrossFractionalTriangleDecomposition.Ghat.src LeanPool.DrossFractionalTriangleDecomposition.Ghat.snk = isFalse ⋯
• LeanPool.DrossFractionalTriangleDecomposition.instDecidableEqGhat.decEq LeanPool.DrossFractionalTriangleDecomposition.Ghat.snk LeanPool.DrossFractionalTriangleDecomposition.Ghat.src = isFalse ⋯
• LeanPool.DrossFractionalTriangleDecomposition.instDecidableEqGhat.decEq LeanPool.DrossFractionalTriangleDecomposition.Ghat.snk LeanPool.DrossFractionalTriangleDecomposition.Ghat.snk = isTrue ⋯

@[instance_reducible]

instance LeanPool.DrossFractionalTriangleDecomposition.instDecidableEqGhat {V✝ : Type u_2} [DecidableEq V✝] : DecidableEq (Ghat V✝)

Equations

• LeanPool.DrossFractionalTriangleDecomposition.instDecidableEqGhat = LeanPool.DrossFractionalTriangleDecomposition.instDecidableEqGhat.decEq

@[instance_reducible]

instance LeanPool.DrossFractionalTriangleDecomposition.instFintypeGhat {V : Type u_1} [DecidableEq V] [Fintype V] : Fintype (Ghat V)

Equations

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

def LeanPool.DrossFractionalTriangleDecomposition.K4pair {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (e₁ e₂ : Sym2 V) : Prop

Two disjoint graph edges whose four endpoints form a clique.

Equations

• LeanPool.DrossFractionalTriangleDecomposition.K4pair G e₁ e₂ = ∃ (a : V) (b : V) (c : V) (d : V), e₁ = s(a, b) ∧ e₂ = s(c, d) ∧ {a, b, c, d}.card = 4 ∧ G.IsNClique 4 {a, b, c, d}

@[instance_reducible]

instance LeanPool.DrossFractionalTriangleDecomposition.instDecidableK4pairOfDecidableRelAdj {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (e₁ e₂ : Sym2 V) : Decidable (K4pair G e₁ e₂)

Equations

• LeanPool.DrossFractionalTriangleDecomposition.instDecidableK4pairOfDecidableRelAdj G e₁ e₂ = id inferInstance

noncomputable def LeanPool.DrossFractionalTriangleDecomposition.cc {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) : ℝ

Per-arc capacity on the edge-to-edge arcs.

Equations

• LeanPool.DrossFractionalTriangleDecomposition.cc G wΔ = 2 * wΔ / (3 * ↑G.minDegree - 3)

noncomputable def LeanPool.DrossFractionalTriangleDecomposition.dcap {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) : Ghat V → Ghat V → ℝ

Capacities of the auxiliary network.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.DrossFractionalTriangleDecomposition.dcap G wΔ x✝¹ x✝ = 0

noncomputable def LeanPool.DrossFractionalTriangleDecomposition.drossNet {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) : Contrib.MaxFlowMinCut.Network (Ghat V)

Dross's network in the already pooled finite-network API.

Equations

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

noncomputable def LeanPool.DrossFractionalTriangleDecomposition.demand {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) : ℝ

Total source-arc capacity, the demand that a maximum flow must meet.

Equations

• LeanPool.DrossFractionalTriangleDecomposition.demand G wΔ = ∑ e ∈ G.edgeFinset, max (↑(LeanPool.DrossFractionalTriangleDecomposition.triThrough G e) * wΔ - 1) 0

theorem LeanPool.DrossFractionalTriangleDecomposition.handshake {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∑ e ∈ G.edgeFinset, triThrough G e = 3 * (G.cliqueFinset 3).card

Summing the number of triangles through each edge counts each triangle three times.

theorem LeanPool.DrossFractionalTriangleDecomposition.balance {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {wΔ : ℝ} (hT : 0 < (G.cliqueFinset 3).card) (hwΔ : wΔ = ↑G.edgeFinset.card / (3 * ↑(G.cliqueFinset 3).card)) : ∑ e ∈ G.edgeFinset, (↑(triThrough G e) * wΔ - 1) = 0

The balanced initial weight makes the signed source excess sum to zero.

theorem LeanPool.DrossFractionalTriangleDecomposition.sum_Ghat {V : Type u_1} [DecidableEq V] [Fintype V] (f : Ghat V → ℝ) : ∑ v : Ghat V, f v = f Ghat.src + f Ghat.snk + ∑ e : Sym2 V, f (Ghat.edge e)

A sum over network nodes splits into source, sink, and edge nodes.

theorem LeanPool.DrossFractionalTriangleDecomposition.triThrough_eq_zero_of_notMem {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {e : Sym2 V} (he : e ∉ G.edgeFinset) : triThrough G e = 0

A nonedge lies in no graph triangle.

theorem LeanPool.DrossFractionalTriangleDecomposition.value_eq_source_sum {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) : F.value = ∑ e : Sym2 V, F.f Ghat.src (Ghat.edge e)

The flow value is the sum of the source-to-edge flows.

theorem LeanPool.DrossFractionalTriangleDecomposition.source_saturated {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) (hF : F.value = demand G wΔ) (e : Sym2 V) : F.f Ghat.src (Ghat.edge e) = max (↑(triThrough G e) * wΔ - 1) 0

If total source flow meets demand, every source arc is saturated.

theorem LeanPool.DrossFractionalTriangleDecomposition.value_eq_sink_sum {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (wΔ : ℝ) (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)) : F.value = ∑ e : Sym2 V, F.f (Ghat.edge e) Ghat.snk

The flow value also equals the total flow into the sink from edge nodes.