EdmondsKarpDistance.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Bounded shortest-path labels for Edmonds--Karp

An unreachable vertex has label n. Reachable vertices have their actual shortest distance, at most n-1. These labels are obtained from the already proved breadth-first search, independently of its deterministic tie rule.

def OAI.ContingencyTables.EdmondsKarpDistance.distance line 17
lemma OAI.ContingencyTables.EdmondsKarpDistance.distance_of_some line 20
lemma OAI.ContingencyTables.EdmondsKarpDistance.distance_of_none line 24
lemma OAI.ContingencyTables.EdmondsKarpDistance.distance_le line 28
lemma OAI.ContingencyTables.EdmondsKarpDistance.distance_lt_of_some line 36
lemma OAI.ContingencyTables.EdmondsKarpDistance.distance_source line 43
lemma OAI.ContingencyTables.EdmondsKarpDistance.distance_route line 50
lemma OAI.ContingencyTables.EdmondsKarpDistance.distance_edge line 56
lemma OAI.ContingencyTables.EdmondsKarpDistance.route_potential line 70
lemma OAI.ContingencyTables.EdmondsKarpDistance.potential_le_distance line 84
Source documentation
Every bounded potential increasing by at most one on each edge lies below the shortest-path labels. This also covers unreachable vertices.
```
lemma potential_le_distance (E : Fin n→Fin n→Bool) (s : Fin n) (d : Fin n→ℕ)
    (hzero : d s=0) (hbound : ∀ v,d v ≤ n)
    (hedge : ∀ u v,E u v=true → d v ≤ d u+1) (v : Fin n) :
    d v ≤ distance E s v := by
…
```
Mentions: OAI.ContingencyTables.EdmondsKarpDistance.distance

lemma OAI.ContingencyTables.EdmondsKarpDistance.tight_sequence line 96

Source documentation

A unit-Lipschitz sequence attaining its maximal endpoint slope has unit slope at every intermediate index.

lemma tight_sequence {k : ℕ} (d : Fin (k+1)→ℕ) (hzero : d 0=0)
    (hlast : d (Fin.last k)=k)
    (hstep : ∀ i : Fin k,d i.succ ≤ d i.castSucc+1) :
    ∀ i : Fin (k+1),d i=i.val := by
…

def OAI.ContingencyTables.EdmondsKarpDistance.label line 121
lemma OAI.ContingencyTables.EdmondsKarpDistance.label_le line 124
lemma OAI.ContingencyTables.EdmondsKarpDistance.label_source line 127
lemma OAI.ContingencyTables.EdmondsKarpDistance.label_edge line 130
lemma OAI.ContingencyTables.EdmondsKarpDistance.label_target line 134
theorem OAI.ContingencyTables.EdmondsKarpDistance.label_path line 150
Source documentation
Every vertex of a shortest residual augmenting path has its path index as shortest distance from the source.
```
theorem label_path {c : Capacity n} {f : Flow n} {s t : Fin n} {k : ℕ}
    {p : Fin (k+1)→Fin n} (hp : ResidualPath c f s t k p)
    (hshort : ∀ l q,ResidualPath c f s t l q → k ≤ l) (i : Fin (k+1)) :
    label c f s (p i)=i.val := by
…
```
Mentions: OAI.ContingencyTables.EdmondsKarpDistance.label
lemma OAI.ContingencyTables.EdmondsKarpDistance.label_path_lt line 161