Capacities of undirected cuts on unordered pairs

This file defines the capacity of a cut for a function on unordered vertex pairs and its simple support graph. Diagonal pairs never contribute to a cut and are ignored by the support graph.

Main definitions

• TauCeti.pairCutCapacity: the capacity of a cut for weights on unordered vertex pairs.
• TauCeti.capacitySupport: the simple support graph of a pair-capacity function.

Main result

• TauCeti.isSubmodular_pairCutCapacity: a pair-capacity function nonnegative off the diagonal has a submodular cut function.
• TauCeti.isSymmSubmodular_pairCutCapacity: the same cut function is symmetric submodular.

noncomputable def TauCeti.pairCutCapacity {V : Type u_1} {K : Type u_2} [Fintype V] [AddCommMonoid K] (c : Sym2 V → K) (S : Finset V) : K

The capacity of the undirected cut with source side S for weights on unordered vertex pairs. Each crossing pair is counted once; diagonal pairs never cross.

@[simp]

theorem TauCeti.pairCutCapacity_zero {V : Type u_1} {K : Type u_2} [Fintype V] [AddCommMonoid K] : pairCutCapacity 0 = 0

The zero pair-capacity function assigns zero capacity to every cut.

theorem TauCeti.pairCutCapacity_def {V : Type u_1} {K : Type u_2} [Fintype V] [AddCommMonoid K] (c : Sym2 V → K) (S : Finset V) [DecidablePred fun (p : Sym2 V) => p.Crosses ↑S] : pairCutCapacity c S = ∑ p : Sym2 V, if p.Crosses ↑S then c p else 0

The defining finite-sum formula for pairCutCapacity.

@[simp]

theorem TauCeti.pairCutCapacity_compl {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid K] (c : Sym2 V → K) (S : Finset V) : pairCutCapacity c Sᶜ = pairCutCapacity c S

Pair cut capacity is unchanged when the two sides of the cut are exchanged.

theorem TauCeti.isSubmodular_pairCutCapacity {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid K] [Preorder K] [IsOrderedAddMonoid K] (c : Sym2 V → K) (hc : ∀ (x y : V), x ≠ y → 0 ≤ c s(x, y)) : IsSubmodular (pairCutCapacity c)

The cut function of weights nonnegative on pairs of distinct vertices is submodular. Diagonal weights are unrestricted. Together with pairCutCapacity_compl, this makes it a symmetric submodular set function.

theorem TauCeti.isSymmSubmodular_pairCutCapacity {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid K] [Preorder K] [IsOrderedAddMonoid K] (c : Sym2 V → K) (hc : ∀ (x y : V), x ≠ y → 0 ≤ c s(x, y)) : IsSymmSubmodular (pairCutCapacity c)

The cut function of weights nonnegative on pairs of distinct vertices is symmetric submodular. Diagonal weights are unrestricted.

theorem TauCeti.pairCutCapacity_eq_of_offDiagonal_eq {V : Type u_1} {K : Type u_2} [Fintype V] [AddCommMonoid K] (c d : Sym2 V → K) (h : ∀ (x y : V), x ≠ y → c s(x, y) = d s(x, y)) : pairCutCapacity c = pairCutCapacity d

Diagonal values do not affect pair cut capacities.

theorem TauCeti.pairCutCapacity_singleton_add_singleton {V : Type u_1} {K : Type u_2} [Fintype V] [DecidableEq V] [AddCommMonoid K] (c : Sym2 V → K) {x y : V} (hxy : x ≠ y) : pairCutCapacity c {x} + pairCutCapacity c {y} = pairCutCapacity c {x, y} + c s(x, y) + c s(x, y)

The sum of the two singleton cut capacities is the capacity of their union plus twice the capacity of the pair joining them.

def TauCeti.capacitySupport {V : Type u_1} {K : Type u_2} [Zero K] [LT K] (c : Sym2 V → K) : SimpleGraph V

The simple support graph of a pair-capacity function. Diagonal capacities are ignored.

@[simp]

theorem TauCeti.capacitySupport_adj {V : Type u_1} {K : Type u_2} [Zero K] [LT K] (c : Sym2 V → K) (x y : V) : (capacitySupport c).Adj x y ↔ x ≠ y ∧ 0 < c s(x, y)

theorem TauCeti.capacitySupport_eq_of_offDiagonal_eq {V : Type u_1} {K : Type u_2} [Zero K] [LT K] (c d : Sym2 V → K) (h : ∀ (x y : V), x ≠ y → c s(x, y) = d s(x, y)) : capacitySupport c = capacitySupport d

Changing only diagonal capacities does not change the support graph.