A flow meeting the exact Dross demand #
The source cut has capacity equal to demand. The exact lower bound for all cuts and max-flow/min-cut therefore produce a flow of that value.
theorem
LeanPool.DrossFractionalTriangleDecomposition.srcCut_capacity
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(wΔ : ℝ)
:
The source cut has capacity exactly the network demand.
theorem
LeanPool.DrossFractionalTriangleDecomposition.exists_flow_M_exact
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(h : 9 * Fintype.card V ≤ 10 * G.minDegree)
(wΔ : ℝ)
(hwΔ : 0 < wΔ)
(hbal : ∑ e ∈ G.edgeFinset, (↑(triThrough G e) * wΔ - 1) = 0)
(δ : ℝ)
(hδ0 : 0 < δ)
(hδ1 : δ ≤ 1 / 10)
(hn20 : 20 ≤ Fintype.card V)
(hmd2 : 2 ≤ G.minDegree)
(hδ_eq : ↑(Fintype.card V) - ↑G.minDegree = δ * ↑(Fintype.card V))
(hmbound :
2 * ↑G.edgeFinset.card ≤ (1 - δ + 2 * δ ^ 2) * ↑(Fintype.card V) ^ 2 + 4 + ↑(Fintype.card V) - 6 * δ * ↑(Fintype.card V))
:
∃ (F : Contrib.MaxFlowMinCut.Flow (drossNet G wΔ)), F.value = demand G wΔ
The auxiliary network has a flow whose value is exactly its demand.