Product multicommodity networks and sparsest cuts

Lax455465.ProductNetwork · concepts/Lax455465/ProductNetwork.lean · lax-455465

definition

Loading review…

Natural Language Statement

Definition

A product multicommodity network has nonnegative edge capacities and a nonnegative weight $\pi(v)$ at each vertex. In an undirected network, the demand between distinct vertices $u,v$ is $\pi(u)\pi(v)$ , shared equally between the two directions. In a directed network, the demand from $u$ to $v$ is $\pi(u)\pi(v)$ in each direction separately. Uniform demands are the case $\pi\equiv1$ .

The ratio cost of a cut $(S,\overline S)$ is

\frac{C(S,\overline S)}{\pi(S)\pi(\overline S)}.

Its numerator counts each undirected crossing edge once, or only arcs leaving $S$ in the directed case. The sparsest-cut value is the infimum of these ratios over cuts of positive demand. Write $p$ for the number of vertices of positive weight.

Concept map

1 concept

100%

DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.Finset.Powerset
2	import Mathlib.Data.NNReal.Basic
3	import Mathlib.Analysis.SpecialFunctions.Log.Basic
4
5	/-!
6	---
7	title: Product multicommodity networks and sparsest cuts
8	type: definition
9	---
10	A product multicommodity network has nonnegative edge capacities and a
11	nonnegative weight $\pi(v)$ at each vertex. In an undirected network, the
12	demand between distinct vertices $u,v$ is $\pi(u)\pi(v)$ , shared equally
13	between the two directions. In a directed network, the demand from $u$ to $v$
14	is $\pi(u)\pi(v)$ in each direction separately. Uniform demands are the case
15	$\pi\equiv1$ .
16
17	The ratio cost of a cut $(S,\overline S)$ is
18	$\frac{C(S,\overline S)}{\pi(S)\pi(\overline S)}.$
19	Its numerator counts each undirected crossing edge once, or only arcs leaving
20	$S$ in the directed case. The sparsest-cut value is the infimum of these
21	ratios over cuts of positive demand. Write $p$ for the number of vertices
22	of positive weight.
23
24	# Formalization notes
25
26	Vertices are `Fin n`. A capacity matrix represents parallel edges by their
27	total capacity and absent edges by zero; loops are excluded. An undirected
28	network has a symmetric capacity matrix. The same cut formula applies in
29	both cases. Cuts of zero demand are excluded, including empty cuts. When
30	$p\ge2$ , the set of admissible cuts is finite and nonempty, so its infimum
31	is a minimum. The theorems impose this hypothesis explicitly.
32
33	The logarithmic factor is $\log_2 p$ , as in the paper. Stating product
34	bounds in terms of $p$ also handles the two-terminal case, where the
35	paper's shorthand $\log k$ vanishes because $k=\binom p2=1$ .
36	-/
37
38	open scoped BigOperators NNReal
39
40	namespace Lax455465.ProductNetwork
41
42	/-- Whether capacities are shared by both directions of an edge or belong
43	to individual directed arcs. -/
44	inductive EdgeKind
45	/-- One capacity shared by both directions of an undirected edge. -/
46	\| undirected
47	/-- A separate capacity for each directed arc. -/
48	\| directed
49	deriving DecidableEq
50
51	/-- A finite loopless network with nonnegative capacities. -/
52	structure Network (n : ℕ) where
53	/-- The capacity of an edge or arc, with zero denoting absence. -/
54	capacity : Fin n → Fin n → ℝ≥0
55	/-- Loops are absent. -/
56	loopless : ∀ v, capacity v v = 0
57
58	/-- An undirected network has the same capacity in both directions. -/
59	def Network.IsUndirected {n : ℕ} (N : Network n) : Prop :=
60	∀ u v, N.capacity u v = N.capacity v u
61
62	/-- The nonnegative weights whose products specify the demands. -/
63	abbrev VertexWeight (n : ℕ) := Fin n → ℝ≥0
64
65	/-- The number of vertices with positive weight. -/
66	noncomputable def supportCount {n : ℕ} (π : VertexWeight n) : ℕ :=
67	(Finset.univ.filter fun v => 0 < π v).card
68
69	/-- The total vertex weight in a set. -/
70	def mass {n : ℕ} (π : VertexWeight n) (S : Finset (Fin n)) : ℝ≥0 :=
71	∑ v ∈ S, π v
72
73	/-- A cut separates positive total weight on both sides. -/
74	def AdmissibleCut {n : ℕ} (π : VertexWeight n) (S : Finset (Fin n)) : Prop :=
75	0 < mass π S ∧ 0 < mass π Sᶜ
76
77	/-- The capacity leaving a cut; symmetric capacities count an undirected
78	edge exactly once. -/
79	def cutCapacity {n : ℕ} (N : Network n) (S : Finset (Fin n)) : ℝ≥0 :=
80	∑ u ∈ S, ∑ v ∈ Sᶜ, N.capacity u v
81
82	/-- The ratio of cut capacity to separated product demand. -/
83	noncomputable def ratioCost {n : ℕ} (N : Network n) (π : VertexWeight n)
84	(S : Finset (Fin n)) : ℝ≥0 :=
85	cutCapacity N S / (mass π S * mass π Sᶜ)
86
87	/-- The least ratio cost of a cut with positive demand. -/
88	noncomputable def sparsestCut {n : ℕ} (N : Network n) (π : VertexWeight n) : ℝ≥0 :=
89	sInf {r \| ∃ S : Finset (Fin n), AdmissibleCut π S ∧ ratioCost N π S = r}
90
91	/-- The all-one vertex weights defining uniform demand. -/
92	def uniformWeight (n : ℕ) : VertexWeight n := fun _ => 1
93
94	/-- The paper's base-two logarithm. -/
95	noncomputable def logFactor (p : ℕ) : ℝ := Real.log (p : ℝ) / Real.log 2
96
97	end Lax455465.ProductNetwork
98

Formalization notes

Vertices are $Fin n$ . A capacity matrix represents parallel edges by their total capacity and absent edges by zero; loops are excluded. An undirected network has a symmetric capacity matrix. The same cut formula applies in both cases. Cuts of zero demand are excluded, including empty cuts. When $p\ge2$ , the set of admissible cuts is finite and nonempty, so its infimum is a minimum. The theorems impose this hypothesis explicitly.

The logarithmic factor is $\log_2 p$ , as in the paper. Stating product bounds in terms of $p$ also handles the two-terminal case, where the paper's shorthand $\log k$ vanishes because $k=\binom p2=1$ .

Builds on

none

Used by

Lax455465.ConcurrentFlow

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Product multicommodity networks and sparsest cuts

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments