Finite graph connectivity and network flows
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremMax-flow/min-cut theorem#
For nonnegative capacities and distinct terminals, some ordinary
flow has value equal to the capacity of the arrows leaving some vertex set containing s but not
t. By weak duality (TauCeti.Flow.val_le_arrowSum) this flow is maximum and this cut is
minimum.
TauCeti.Flow.exists_val_eq_arrowSum.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w}
[Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K]
{cap : TauCeti.Assignment Q K} {s t : V} [DecidableEq V] (hst : s ≠ t) (hcap : 0 ≤ cap) :
∃ f S, s ∈ S ∧ t ∉ S ∧ f.val = TauCeti.arrowSum cap S Sᶜ
Uses 2 · Used by 1
TheoremMax-flow/min-cut theorem for bounded assignments#
If some bounded s–t assignment
between distinct terminals exists, then some bounded s–t assignment has value equal to the cut
bound of some vertex set containing s but not t. By weak duality
(TauCeti.BoundedFlow.val_le_cutBound) this assignment is maximum and this cut bound is
minimum.
TauCeti.BoundedFlow.exists_val_eq_cutBound.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w}
[Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K]
{lo hi : TauCeti.Assignment Q K} {s t : V} [DecidableEq V] (hst : s ≠ t)
(f : TauCeti.BoundedFlow lo hi s t) : ∃ g S, s ∈ S ∧ t ∉ S ∧ g.val = TauCeti.cutBound lo hi S
Uses 1
TheoremIntegrality of maximum flows#
For nonnegative capacities in an additive subgroup H, some
maximum ordinary flow takes values in H. For distinct terminals, its value is the capacity of
some cut by TauCeti.Flow.IsMaximum.exists_val_eq_arrowSum.
TauCeti.Flow.exists_isMaximum_mem.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w}
[Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K]
{cap : TauCeti.Assignment Q K} {s t : V} (hcap : 0 ≤ cap) (H : AddSubgroup K)
(hcapH : ∀ ⦃v w : V⦄ (e : Q v w), cap e ∈ H) :
∃ f, f.IsMaximum ∧ ∀ ⦃v w : V⦄ (e : Q v w), f.toFun e ∈ H
TheoremPath–cycle decomposition#
Every nonnegative arrow assignment f on a finite arrow family
is a sum of positively weighted directed paths, each from a vertex of negative excess to a vertex
of positive excess, and positively weighted directed cycles. The number of components is at most
the number of arrows on which f is positive, and if the values of f lie in an additive subgroup
H, then so do all weights.
TauCeti.exists_pathCycleDecomposition.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w}
[Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K]
{f : TauCeti.Assignment Q K} (H : AddSubgroup K) (hf : 0 ≤ f)
(hH : ∀ ⦃x y : V⦄ (e : Q x y), f e ∈ H) :
∃ D,
(∀ p ∈ D.paths, p.weight ∈ H) ∧
(∀ c ∈ D.cycles, c.weight ∈ H) ∧ D.paths.length + D.cycles.length ≤ {a | 0 < f a.snd.snd}.card
TheoremAcyclic flows#
Every ordinary s–t flow f has an acyclic ordinary s–t flow of the
same value that is arrowwise at most f.
TauCeti.Flow.exists_isAcyclic.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V]
[(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K]
{cap : TauCeti.Assignment Q K} {s t : V} (f : TauCeti.Flow cap s t) :
∃ g, g.toFun.IsAcyclic ∧ g.val = f.val ∧ g.toFun ≤ f.toFun
DefinitionThe poset of minimum cuts#
For a maximum bounded s–t assignment f between distinct
terminals, the minimum cuts, ordered by inclusion, are order isomorphic to the upper sets of the
poset of free residual components, ordered by inclusion. A minimum cut corresponds to the free
components contained in it, and an upper set to the vertices of its components together with the
vertices forced onto the source side.
TauCeti.BoundedFlow.IsMaximum.minimizersOrderIso.{u, v, w} {V : Type u} {Q : V → V → Type v}
{K : Type w} [Fintype V] [DecidableEq V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K]
[LinearOrder K] [IsOrderedAddMonoid K] {lo hi : TauCeti.Assignment Q K} {s t : V}
{f : TauCeti.BoundedFlow lo hi s t} (hst : s ≠ t) (hf : f.IsMaximum) :
↥(TauCeti.TerminalCut.minimizers ⋯ {s} {t}) ≃o (UpperSet f.FreeComponent)ᵒᵈ
Lean
Formalized in Tau Ceti as TauCeti.BoundedFlow.IsMaximum.minimizersOrderIso.
Sources
Uses 1
TheoremMulti-cut non-crossing lemma#
Let 𝒞 be a pairwise non-crossing family of cuts, each a
minimum cut of a symmetric submodular f between some pair of vertices. If none of them
separates the distinct vertices s and t, then some minimum s–t cut crosses none of
them.
TauCeti.TerminalCut.exists_isMinimum_forall_not_crosses.{u_1, u_2} {V : Type u_1} {K : Type u_2}
[Fintype V] [DecidableEq V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K]
{f : Finset V → K} (hf : TauCeti.IsSymmSubmodular f) {𝒞 : Set (Finset V)}
(h𝒞 : 𝒞.Pairwise fun Y Z => ¬Y.Crosses Z)
(hmin : ∀ Y ∈ 𝒞, ∃ a b, TauCeti.TerminalCut.IsMinimum f {a} {b} Y) {s t : V} (hst : s ≠ t)
(hsep : ∀ Y ∈ 𝒞, s ∈ Y ↔ t ∈ Y) :
∃ X, TauCeti.TerminalCut.IsMinimum f {s} {t} X ∧ ∀ Y ∈ 𝒞, ¬X.Crosses Y
Lean
Formalized in Tau Ceti as TauCeti.TerminalCut.exists_isMinimum_forall_not_crosses.
Sources
Used by 1
TheoremUltrametric inequality for minimum cut values#
every cut separating s from t
separates s from v or v from t. The intermediate vertex v is arbitrary.
TauCeti.TerminalCut.min_pairMinimumValue_le.{u_1, u_3} {V : Type u_1} {K : Type u_3} [Finite V]
[Zero K] [LinearOrder K] (f : Finset V → K) {s t : V} (hst : s ≠ t) (v : V) :
min (TauCeti.TerminalCut.pairMinimumValue f s v) (TauCeti.TerminalCut.pairMinimumValue f v t) ≤
TauCeti.TerminalCut.pairMinimumValue f s t
Used by 1
TheoremGraph.isBridge_iff_forall_cycle_notMem#
An actual edge is a bridge exactly when it lies on no cycle.
Graph.isBridge_iff_forall_cycle_notMem.{u, v} {α : Type u} {β : Type v} {G : Graph α β} {e : β}
(he : e ∈ G.edgeSet) : G.IsBridge e ↔ ∀ ⦃u : α⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges
Uses 1
TheoremBridges by component counts#
With finitely many connected components, an edge is a bridge exactly when deleting it increases the number of connected components by one.
Graph.isBridge_iff_componentCount_deleteEdges_eq_add_one.{u, v} {α : Type u} {β : Type v}
{G : Graph α β} {e : β} [Finite G.ConnectedComponent] :
G.IsBridge e ↔ (G.deleteEdges {e}).componentCount = G.componentCount + 1
Lean
Formalized in Tau Ceti as Graph.isBridge_iff_componentCount_deleteEdges_eq_add_one.
Sources
Uses 1
DefinitionTauCeti.residualUpdate#
The residual update of f by a residual assignment r: the value on each arrow e is
f e + r e⁺ - r e⁻, where e⁺ = Sum.inl e and e⁻ = Sum.inr e are its residual copies.
TauCeti.residualUpdate.{u, v, w} {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K]
(f : TauCeti.Assignment Q K) (r : TauCeti.Assignment (TauCeti.ResidualHom Q) K) :
TauCeti.Assignment Q K
Used by 9
DefinitionTauCeti.ArrowWalk.splitEquiv#
Lifting identifies the walks from s to t with the walks in the split network from the
entrance of s to the entrance (b = false) or exit (b = true) of t; the inverse is
projection.
TauCeti.ArrowWalk.splitEquiv.{u, v} {V : Type u} (Q : V → V → Type v) (s t : V) (b : Bool) :
TauCeti.ArrowWalk Q s t ≃ TauCeti.ArrowWalk (TauCeti.SplitHom Q) (s, false) (t, b)
DefinitionTauCeti.AuxTerminalHom#
The arrow family of Q with auxiliary terminals for the vertex sets A and B, on the
vertex type V ⊕ Bool. The arrows between original vertices Sum.inl v and Sum.inl w are those
of Q v w; the fresh source σ = Sum.inr false has one arrow to each Sum.inl a with a ∈ A; the
fresh sink τ = Sum.inr true has one arrow from each Sum.inl b with b ∈ B; and there are no
other arrows.
TauCeti.AuxTerminalHom.{u, v} {V : Type u} (Q : V → V → Type v) (A B : Finset V) :
V ⊕ Bool → V ⊕ Bool → Type v
InductiveGraph.Walk#
An edge-labelled walk in a multigraph. Each step records an edge together with its incidence; a zero-length walk may be based at any ambient point.
Graph.Walk.{u, v} {α : Type u} {β : Type v} (G : Graph α β) : α → α → Type (max u v)
DefinitionSimpleGraph.walkEquivOfSimpleGraph#
Walks in a simple graph are equivalent to edge-labelled walks in its associated Graph.
SimpleGraph.walkEquivOfSimpleGraph.{u} {α : Type u} (H : SimpleGraph α) (x y : α) :
H.Walk x y ≃ (Graph.ofSimpleGraph H).Walk x y
Uses 1
TheoremGomory–Hu theorem#
Every symmetric submodular set function on a nonempty finite vertex type has a cut tree: a weighted tree on the vertices in which the minimum cut value between any two distinct vertices is the minimum weight on the tree path between them, and deleting any tree edge leaves a minimum cut between its ends.
TauCeti.TerminalCut.exists_isCutTree.{u_1, u_2} {V : Type u_1} {K : Type u_2} [Fintype V]
[DecidableEq V] [AddCommMonoid K] [LinearOrder K] [IsOrderedCancelAddMonoid K] {f : Finset V → K}
[Nonempty V] (hf : TauCeti.IsSymmSubmodular f) : ∃ T w, TauCeti.TerminalCut.IsCutTree f T w
Uses 2
TheoremQuery theorem#
If s(u, v) has minimum weight on the tree path from s to t, and s
lies on the side of u, then that side is a minimum s–t cut. Since the two sides of a tree
edge cover the vertices, one of the orientations (u, v) and (v, u) applies.
TauCeti.TerminalCut.IsCutTree.isMinimum_edgeSide_of_mem_edges.{u_1, u_2} {V : Type u_1}
{K : Type u_2} [Fintype V] [Zero K] [LinearOrder K] {f : Finset V → K} {T : SimpleGraph V}
{w : Sym2 V → K} (hT : TauCeti.TerminalCut.IsCutTree f T w) {s t u v : V} {p : T.Walk s t}
(hp : p.IsPath) (huv : s(u, v) ∈ p.edges) (hmin : ∀ e ∈ p.edges, w s(u, v) ≤ w e)
(hs : s ∈ T.edgeSide u v) : TauCeti.TerminalCut.IsMinimum f {s} {t} (T.edgeSide u v)
Lean
Formalized in Tau Ceti as TauCeti.TerminalCut.IsCutTree.isMinimum_edgeSide_of_mem_edges.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.