PublishedEdmondsKarp.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Shortest-augmenting-path bound

The finite integral-network specialization of Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2) (1972), 248–264, Theorem 1 (printed page 251). The bound (n³−n)/4 implies the n³ bound for shortest residual augmentations.

Primary text: https://web.eecs.umich.edu/~pettie/matching/Edmonds-Karp-network-flow.pdf

abbrev OAI.ContingencyTables.PublishedEdmondsKarp.Flow line 24
abbrev OAI.ContingencyTables.PublishedEdmondsKarp.Capacity line 25
def OAI.ContingencyTables.PublishedEdmondsKarp.Feasible line 29
Source documentation
Skew flows combine the two antiparallel directions. The upper capacity bound and skew symmetry give both directed residual bounds.
```
def Feasible {n : ℕ} (c : Capacity n) (s t : Fin n) (f : Flow n) : Prop :=
…
```
Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.Capacity, OAI.ContingencyTables.PublishedEdmondsKarp.Flow
def OAI.ContingencyTables.PublishedEdmondsKarp.value line 34
def OAI.ContingencyTables.PublishedEdmondsKarp.IsMaximum line 36
def OAI.ContingencyTables.PublishedEdmondsKarp.ResidualPath line 40
Source documentation
A directed residual path with k arcs and no repeated vertices.
```
def ResidualPath {n : ℕ} (c : Capacity n) (f : Flow n) (s t : Fin n)
    (k : ℕ) (p : Fin (k+1) → Fin n) : Prop :=
…
```
Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.Capacity, OAI.ContingencyTables.PublishedEdmondsKarp.Flow
def OAI.ContingencyTables.PublishedEdmondsKarp.ShortestAugmentation line 49
Source documentation
An actual saturating augmentation along a shortest residual path. The bottleneck is positive, bounded by every residual capacity, and attained by an arc. The displayed update adds it forward and subtracts it backward on precisely the traversed arcs.
```
def ShortestAugmentation {n : ℕ} (c : Capacity n) (s t : Fin n)
    (f g : Flow n) : Prop :=
…
```
Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.Capacity, OAI.ContingencyTables.PublishedEdmondsKarp.Flow
def OAI.ContingencyTables.PublishedEdmondsKarp.AugmentationTrace line 63
Source documentation
A finite initial segment of an actual shortest-augmentation execution. It need not already have reached a maximum flow.
```
def AugmentationTrace {n K : ℕ} (c : Capacity n) (s t : Fin n)
    (F : Fin (K+1) → Flow n) : Prop :=
…
```
Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.Capacity, OAI.ContingencyTables.PublishedEdmondsKarp.Flow
def OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1 line 72
Source documentation
The shortest-augmenting-path bound for integral skew flows. Every finite initial segment has at most n³ augmentations, independently of the rule used to break ties between shortest paths.
```
def EdmondsKarp1972Theorem1 : Prop :=
…
```
theorem OAI.ContingencyTables.PublishedEdmondsKarp.no_long_trace line 78