CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 29. Linear Programming
29.2. Formulating Problems as Linear Programs

Imports

import CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.NetworkFlow
import CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.ShortestPath
import CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.MaximumFlow
import CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.MinimumCostFlow
import CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.MulticommodityFlow

29.2. Formulating Problems as Linear Programs

This section contains the four textbook formulations: shortest path, maximum flow, minimum-cost flow, and multicommodity flow.

Implementation details

              namespace CLRSnamespace Chapter29end Chapter29end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.NetworkFlow

29.2: Common finite-network definitions

CLRS writes its flow linear programs with one nonnegative variable f u v for every ordered pair of vertices. A missing edge is represented by capacity zero. This file records that shared finite-network vocabulary, together with the finite-standard-form encoding helpers used by every §29.2 formulation.

              namespace CLRSnamespace Chapter29open Finsetopen scoped BigOperators

A finite directed capacitated network. Capacities are total; assigning capacity zero to nonedges gives exactly the convention used in CLRS §29.2.

structure FlowNetwork (V : Type*) [Fintype V] where
  source : V
  sink : V
  source_ne_sink : source ≠ sink
  capacity : V → V → ℝ
  capacity_nonnegative : ∀ u v, 0 ≤ capacity u v

namespace FlowNetworkvariable {V : Type*} [Fintype V] (N : FlowNetwork V)

Total flow leaving a vertex.

def outflow (f : V → V → ℝ) (u : V) : ℝ := ∑ v, f u v

Total flow entering a vertex.

def inflow (f : V → V → ℝ) (u : V) : ℝ := ∑ v, f v u

Net flow leaving a vertex.

def netOutflow (f : V → V → ℝ) (u : V) : ℝ := outflow f u - inflow f u

Flow conservation at one vertex.

def ConservesAt (f : V → V → ℝ) (u : V) : Prop := inflow f u = outflow f u

The nonnegativity and capacity inequalities shared by the flow LPs.

def IsCapacityFeasible (f : V → V → ℝ) : Prop :=
  (∀ u v, 0 ≤ f u v) ∧ ∀ u v, f u v ≤ N.capacity u v

A feasible single-commodity flow: capacity constraints everywhere and conservation away from the source and sink.

def IsFlow (f : V → V → ℝ) : Prop :=
  N.IsCapacityFeasible f ∧
    ∀ u, u ≠ N.source → u ≠ N.sink → ConservesAt f u

end FlowNetwork

Finite standard-form encoding helpers

These helpers reindex semantic vectors over a finite type into the Fin-indexed vectors used by StandardLP, and prove the sum identities that the assignment bridges rely on.

namespace FinEncodingvariable {ι : Type*} [Fintype ι]

Lift a semantic vector over a finite type to the Fin-indexed vector of the same coordinates.

noncomputable def lift (x : ι → ℝ) : Fin (Fintype.card ι) → ℝ :=
  x ∘ (Fintype.equivFin ι).symm

Project a Fin-indexed vector back to a semantic vector.

noncomputable def proj (x : Fin (Fintype.card ι) → ℝ) : ι → ℝ :=
  x ∘ (Fintype.equivFin ι)

Lifting then projecting recovers the original vector.

theorem proj_lift (x : ι → ℝ) (a : ι) : proj (lift x) a = x a := by
  simp [proj, lift]

A finite sum over Fin (card ι) reindexes to a sum over ι.

theorem sum_reindex {M : Type*} [AddCommMonoid M] (f : Fin (Fintype.card ι) → M) :
    (∑ i : Fin (Fintype.card ι), f i) = ∑ a : ι, f (Fintype.equivFin ι a) := by
  exact (Equiv.sum_comp (Fintype.equivFin ι) f).symm

The indicator sum that collapses an ι-indicator to its selected coordinate.


theorem sum_indicator [DecidableEq ι] (a : ι) (x : ι → ℝ) :
    (∑ j : Fin (Fintype.card ι),
        (if (Fintype.equivFin ι).symm j = a then 1 else 0) * lift x j) = x a := by
  calc
    (∑ j : Fin (Fintype.card ι),
        (if (Fintype.equivFin ι).symm j = a then 1 else 0) * lift x j)
        = ∑ b : ι, (if b = a then 1 else 0) * x b := by
            rw [sum_reindex]
            simp [lift]
    _ = x a := by
            rw [Finset.sum_eq_single a]
            · simp
            · intro b _ hb; simp [hb]
            · intro h; exact False.elim (h (Finset.mem_univ a))

A direct Fin-indicator sum (no reindexing): the coefficient is nonzero exactly at the selected coordinate.


theorem sum_indicator_fin {n : ℕ} (e : Fin n) (x : Fin n → ℝ) :
    (∑ j : Fin n, (if j = e then 1 else 0) * x j) = x e := by
  rw [Finset.sum_eq_single e]
  · simp
  · intro b _ hb; simp [hb]
  · intro h; exact False.elim (h (Finset.mem_univ e))

Fin.addCases reduces on a left (castAdd) index.

theorem addCases_castAdd {m n : ℕ} {C : Type u} (left : Fin m → C) (right : Fin n → C) (e : Fin m) :
    Fin.addCases left right (Fin.castAdd n e) = left e := by
  simp [Fin.addCases]

Fin.addCases reduces on a right (natAdd) index.

theorem addCases_natAdd {m n : ℕ} {C : Type u} (left : Fin m → C) (right : Fin n → C) (v : Fin n) :
    Fin.addCases left right (Fin.natAdd m v) = right v := by
  simp [Fin.addCases]

Lift a binary vector to the Fin-indexed vector over ordered pairs.

noncomputable def lift₂ {α β : Type*} [Fintype α] [Fintype β] (x : α → β → ℝ) :
    Fin (Fintype.card (α × β)) → ℝ :=
  lift (Function.uncurry x)

Project a Fin-indexed vector over ordered pairs back to a binary vector.

noncomputable def proj₂ {α β : Type*} [Fintype α] [Fintype β]
    (x : Fin (Fintype.card (α × β)) → ℝ) : α → β → ℝ :=
  Function.curry (proj x)

Sum of an indicator on the first coordinate over all ordered pairs.


theorem sum_indicator_fst {α β : Type*} [Fintype α] [Fintype β] [DecidableEq α]
    (a : α) (x : α → β → ℝ) :
    (∑ j : Fin (Fintype.card (α × β)),
        (if ((Fintype.equivFin (α × β)).symm j).1 = a then 1 else 0) * lift₂ x j) =
      ∑ b : β, x a b := by
  calc
    (∑ j : Fin (Fintype.card (α × β)),
        (if ((Fintype.equivFin (α × β)).symm j).1 = a then 1 else 0) * lift₂ x j)
        = ∑ p : α × β, (if p.1 = a then 1 else 0) * x p.1 p.2 := by
            rw [sum_reindex]
            simp [lift₂, lift, Function.uncurry]
    _ = ∑ b : β, x a b := by
            rw [Fintype.sum_prod_type]
            rw [Finset.sum_eq_single a]
            · simp
            · intro c _ hc; simp [hc]
            · intro h; exact False.elim (h (Finset.mem_univ a))

Sum of an indicator on the second coordinate over all ordered pairs.


theorem sum_indicator_snd {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β]
    (a : β) (x : α → β → ℝ) :
    (∑ j : Fin (Fintype.card (α × β)),
        (if ((Fintype.equivFin (α × β)).symm j).2 = a then 1 else 0) * lift₂ x j) =
      ∑ b : α, x b a := by
  calc
    (∑ j : Fin (Fintype.card (α × β)),
        (if ((Fintype.equivFin (α × β)).symm j).2 = a then 1 else 0) * lift₂ x j)
        = ∑ p : α × β, (if p.2 = a then 1 else 0) * x p.1 p.2 := by
            rw [sum_reindex]
            simp [lift₂, lift, Function.uncurry]
    _ = ∑ b : α, x b a := by
            rw [Fintype.sum_prod_type]
            rw [Finset.sum_comm]
            rw [Finset.sum_eq_single a]
            · simp
            · intro c _ hc; simp [hc]
            · intro h; exact False.elim (h (Finset.mem_univ a))

              end FinEncodingend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.ShortestPath

29.2: Shortest paths as a linear program

For a source s and target t, CLRS maximizes d t, subject to d s = 0 and d v ≤ d u + w u v on every edge. Thus every feasible d t is a lower bound on every s-to-t walk; an attained bound is optimal.

This module also records the finite standard-form encoding: the general-form program is reindexed into a concrete StandardLP (one variable per vertex), and feasibility and the objective value are proved to be preserved.

              namespace CLRSnamespace Chapter29namespace ShortestPathLPopen Chapter24open Matrixopen scoped BigOperatorsvariable {V : Type*} [Fintype V] [DecidableEq V]

Feasibility constraints of the CLRS shortest-path LP.

def IsFeasible (G : WeightedGraph V) (s : V) (d : V → ℝ) : Prop :=
  d s = 0 ∧ ∀ u v, (u, v) ∈ G.edges → d v ≤ d u + G.w u v

Optimality for the maximization objective d t.

def IsOptimal (G : WeightedGraph V) (s t : V) (d : V → ℝ) : Prop :=
  IsFeasible G s d ∧ ∀ e, IsFeasible G s e → e t ≤ d t

Every feasible potential is a lower bound on the weight of every walk from the source. This is the core correctness property of the formulation.

theorem feasible_le_walkWeight {G : WeightedGraph V} {s t : V} {d : V → ℝ}
    (hd : IsFeasible G s d) (p : List V) (hp : G.IsWalkFrom s t p) :
    d t ≤ Chapter24.WeightedGraph.walkWeight G.w p := by
  have h := Chapter24.WeightedGraph.le_add_walkWeight_of_potential G d hd.2 s t p hp
  simpa [hd.1] using h

If a feasible potential is attained by an actual source-to-target walk, then it solves the shortest-path LP.

theorem optimal_of_attained_walk {G : WeightedGraph V} {s t : V} {d : V → ℝ}
    (hd : IsFeasible G s d) (p : List V) (hp : G.IsWalkFrom s t p)
    (hweight : Chapter24.WeightedGraph.walkWeight G.w p = d t) : IsOptimal G s t d := by
  refine ⟨hd, ?_⟩
  intro e he
  calc
    e t ≤ Chapter24.WeightedGraph.walkWeight G.w p := feasible_le_walkWeight he p hp
    _ = d t := hweight

Finite standard-form encoding

The type of directed edges that are actually present in the graph.

abbrev Edge (G : WeightedGraph V) := {e : V × V // e ∈ G.edges}

The general-form program for the shortest-path LP: maximize d t subject to d s = 0 and d v - d u ≤ w u v on every edge. All vertices are free variables.

noncomputable def toGeneralLP (G : WeightedGraph V) (s t : V) : GeneralLP where
  n := Fintype.card V
  m := Fintype.card (Edge G) + 1
  maximize := true
  c := fun j => if (Fintype.equivFin V).symm j = t then 1 else 0
  rel := fun i =>
    Fin.cases
      (ConstraintRel.eq)
      (fun _ => ConstraintRel.le)
      i
  A := fun i =>
    Fin.cases
      (fun j => if (Fintype.equivFin V).symm j = s then 1 else 0)
      (fun e j =>
        let uv := (Fintype.equivFin (Edge G)).symm e
        (if (Fintype.equivFin V).symm j = uv.1.2 then 1 else 0) -
          (if (Fintype.equivFin V).symm j = uv.1.1 then 1 else 0))
      i
  b := fun i =>
    Fin.cases
      (0 : ℝ)
      (fun e =>
        let uv := (Fintype.equivFin (Edge G)).symm e
        G.w uv.1.1 uv.1.2)
      i
  free := fun _ => true

The index of the source-equality constraint.

abbrev sourceIndex (G : WeightedGraph V) : Fin (Fintype.card (Edge G) + 1) := 0

The index of the constraint attached to a present edge.

abbrev edgeIndex (G : WeightedGraph V) (e : Fin (Fintype.card (Edge G))) :
    Fin (Fintype.card (Edge G) + 1) :=
  e.succ

              lemma A_source (G : WeightedGraph V) (s t : V) (j : Fin (Fintype.card V)) :
    (toGeneralLP G s t).A (sourceIndex G) j =
      if (Fintype.equivFin V).symm j = s then 1 else 0 := by
  simp [toGeneralLP, sourceIndex]lemma b_source (G : WeightedGraph V) (s t : V) :
    (toGeneralLP G s t).b (sourceIndex G) = 0 := by
  simp [toGeneralLP, sourceIndex]lemma rel_source (G : WeightedGraph V) (s t : V) :
    (toGeneralLP G s t).rel (sourceIndex G) = ConstraintRel.eq := by
  simp [toGeneralLP, sourceIndex]lemma A_edge (G : WeightedGraph V) (s t : V) (e : Fin (Fintype.card (Edge G)))
    (j : Fin (Fintype.card V)) :
    (toGeneralLP G s t).A (edgeIndex G e) j =
      (if (Fintype.equivFin V).symm j = ((Fintype.equivFin (Edge G)).symm e).1.2 then 1 else 0) -
        (if (Fintype.equivFin V).symm j = ((Fintype.equivFin (Edge G)).symm e).1.1 then 1 else 0) := by
  simp [toGeneralLP, edgeIndex]lemma b_edge (G : WeightedGraph V) (s t : V) (e : Fin (Fintype.card (Edge G))) :
    (toGeneralLP G s t).b (edgeIndex G e) =
      G.w ((Fintype.equivFin (Edge G)).symm e).1.1 ((Fintype.equivFin (Edge G)).symm e).1.2 := by
  simp [toGeneralLP, edgeIndex]lemma rel_edge (G : WeightedGraph V) (s t : V) (e : Fin (Fintype.card (Edge G))) :
    (toGeneralLP G s t).rel (edgeIndex G e) = ConstraintRel.le := by
  simp [toGeneralLP, edgeIndex]

The source row of the encoded constraint matrix reads out d s.

lemma mulVec_source (G : WeightedGraph V) (s t : V) (d : V → ℝ) :
    ((toGeneralLP G s t).A *ᵥ FinEncoding.lift d) (sourceIndex G) = d s := by
  calc
    ((toGeneralLP G s t).A *ᵥ FinEncoding.lift d) (sourceIndex G)
        = ∑ j : Fin (Fintype.card V), (toGeneralLP G s t).A (sourceIndex G) j * FinEncoding.lift d j := by rfl
    _ = ∑ j : Fin (Fintype.card V),
          (if (Fintype.equivFin V).symm j = s then 1 else 0) * FinEncoding.lift d j := by
          simp only [A_source]
    _ = d s := FinEncoding.sum_indicator s d

An edge row of the encoded constraint matrix reads out d v - d u.


lemma mulVec_edge (G : WeightedGraph V) (s t : V) (e : Fin (Fintype.card (Edge G)))
    (d : V → ℝ) :
    ((toGeneralLP G s t).A *ᵥ FinEncoding.lift d) (edgeIndex G e) =
      d ((Fintype.equivFin (Edge G)).symm e).1.2 - d ((Fintype.equivFin (Edge G)).symm e).1.1 := by
  calc
    ((toGeneralLP G s t).A *ᵥ FinEncoding.lift d) (edgeIndex G e)
        = ∑ j : Fin (Fintype.card V), (toGeneralLP G s t).A (edgeIndex G e) j * FinEncoding.lift d j := by rfl
    _ = ∑ j : Fin (Fintype.card V),
          ((if (Fintype.equivFin V).symm j = ((Fintype.equivFin (Edge G)).symm e).1.2 then 1 else 0) -
             (if (Fintype.equivFin V).symm j = ((Fintype.equivFin (Edge G)).symm e).1.1 then 1 else 0)) *
            FinEncoding.lift d j := by
          simp only [A_edge]
    _ = (∑ j : Fin (Fintype.card V),
          (if (Fintype.equivFin V).symm j = ((Fintype.equivFin (Edge G)).symm e).1.2 then 1 else 0) * FinEncoding.lift d j) -
          (∑ j : Fin (Fintype.card V),
          (if (Fintype.equivFin V).symm j = ((Fintype.equivFin (Edge G)).symm e).1.1 then 1 else 0) * FinEncoding.lift d j) := by
          simp only [sub_mul, Finset.sum_sub_distrib]
    _ = d ((Fintype.equivFin (Edge G)).symm e).1.2 - d ((Fintype.equivFin (Edge G)).symm e).1.1 := by
          rw [FinEncoding.sum_indicator, FinEncoding.sum_indicator]

Semantic feasibility is exactly encoded general-form feasibility.

Try `simp at hfree` instead of `simpa using hfree`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
theorem feasible_iff_generalLP (G : WeightedGraph V) (s t : V) (d : V → ℝ) :
    IsFeasible G s d ↔ (toGeneralLP G s t).IsFeasible (FinEncoding.lift d) := by
  unfold IsFeasible GeneralLP.IsFeasible
  constructor
  · intro hd
    refine ⟨?_, ?_⟩
    · intro j hfree
      exfalso
      Try `simp at hfree` instead of `simpa using hfree`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [toGeneralLP] using hfree
    · intro i
      exact Fin.cases (motive := fun i => match (toGeneralLP G s t).rel i with
          | ConstraintRel.le => ((toGeneralLP G s t).A *ᵥ FinEncoding.lift d) i ≤ (toGeneralLP G s t).b i
          | ConstraintRel.eq => ((toGeneralLP G s t).A *ᵥ FinEncoding.lift d) i = (toGeneralLP G s t).b i
          | ConstraintRel.ge => (toGeneralLP G s t).b i ≤ ((toGeneralLP G s t).A *ᵥ FinEncoding.lift d) i)
        (by
          rw [rel_source, mulVec_source, b_source]
          exact hd.1)
        (fun e => by
          rw [rel_edge, mulVec_edge, b_edge]
          have h := hd.2 ((Fintype.equivFin (Edge G)).symm e).1.1 ((Fintype.equivFin (Edge G)).symm e).1.2 ((Fintype.equivFin (Edge G)).symm e).2
          linarith)
        i
  · intro h
    refine ⟨?_, ?_⟩
    · have hsource := h.2 (sourceIndex G)
      rw [rel_source] at hsource
      rw [mulVec_source, b_source] at hsource
      exact hsource
    · intro u v huv
      let e : Edge G := ⟨(u, v), huv⟩
      have hedge := h.2 (edgeIndex G (Fintype.equivFin (Edge G) e))
      rw [rel_edge] at hedge
      rw [mulVec_edge, b_edge] at hedge
      have hedge' : d v - d u ≤ G.w u v := by simpa [e] using hedge
      linarith

The general-form objective reads out d t.


lemma objective_generalLP (G : WeightedGraph V) (s t : V) (d : V → ℝ) :
    (toGeneralLP G s t).objective (FinEncoding.lift d) = d t := by
  dsimp [GeneralLP.objective, toGeneralLP]
  simp only [dotProduct]
  rw [FinEncoding.sum_reindex]
  simp only [FinEncoding.lift]
  rw [Finset.sum_eq_single t]
  · simp
  · intro v _ hv; simp [hv]
  · intro h; exact False.elim (h (Finset.mem_univ t))

The finite standard-form program obtained by normalizing the shortest-path general program.

noncomputable def toStandardLP (G : WeightedGraph V) (s t : V) :=
  (toGeneralLP G s t).toStandardLP

The expansion of a potential to the normalized standard-form variable vector.

noncomputable def fullLift (G : WeightedGraph V) (s t : V) (d : V → ℝ) :
    Fin (Fintype.card V + Fintype.card V) → ℝ :=
  (toGeneralLP G s t).lift (FinEncoding.lift d)

The normalized standard-form objective is exactly the shortest-path objective d t.


theorem objective_toStandardLP (G : WeightedGraph V) (s t : V) (d : V → ℝ) :
    (toStandardLP G s t).objective (fullLift G s t d) = d t := by
  unfold toStandardLP fullLift
  rw [GeneralLP.objective_lift]
  rw [objective_generalLP]
  simp [toGeneralLP, GeneralLP.objectiveSign]

Feasibility is exactly preserved under the finite standard-form encoding.


theorem feasible_iff_toStandardLP (G : WeightedGraph V) (s t : V) (d : V → ℝ) :
    IsFeasible G s d ↔ (toStandardLP G s t).IsFeasible (fullLift G s t d) := by
  unfold toStandardLP fullLift
  rw [← GeneralLP.feasible_iff_lift]
  exact feasible_iff_generalLP G s t d

              end ShortestPathLPend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.MaximumFlow

29.2: Maximum flow as a linear program

The variables are the gross directed flows f u v. The constraints are nonnegativity, capacity, and conservation at every vertex other than s,t; the objective is the net flow leaving s, exactly as in CLRS §29.2.

This module also records the finite standard-form encoding: one nonnegative variable per ordered pair, a capacity inequality per ordered pair, and a conservation equality per internal vertex, reindexed into a concrete StandardLP.

              namespace CLRSnamespace Chapter29namespace MaximumFlowLPopen Finsetopen Matrixopen scoped BigOperatorsvariable {V : Type*} [Fintype V] (N : FlowNetwork V)

The constraints of the maximum-flow LP.

def IsFeasible (f : V → V → ℝ) : Prop :=
  (∀ u v, 0 ≤ f u v) ∧
  (∀ u v, f u v ≤ N.capacity u v) ∧
  ∀ u, u ≠ N.source → u ≠ N.sink → FlowNetwork.ConservesAt f u

The textbook maximum-flow objective: source outflow minus source inflow.

def objective (f : V → V → ℝ) : ℝ := FlowNetwork.netOutflow f N.source

A feasible flow maximizing the source outflow.

def IsOptimal (f : V → V → ℝ) : Prop :=
  IsFeasible N f ∧ ∀ g, IsFeasible N g → objective N g ≤ objective N f

The displayed LP constraints are precisely the usual finite-network flow constraints.

theorem isFeasible_iff (f : V → V → ℝ) : IsFeasible N f ↔ N.IsFlow f := by
  simp only [IsFeasible, FlowNetwork.IsFlow, FlowNetwork.IsCapacityFeasible]
  tauto

The LP optimum is precisely a maximum flow under the same objective.

theorem isOptimal_iff (f : V → V → ℝ) :
    IsOptimal N f ↔
      N.IsFlow f ∧ ∀ g, N.IsFlow g →
        FlowNetwork.netOutflow g N.source ≤ FlowNetwork.netOutflow f N.source := by
  simp only [IsOptimal, objective, isFeasible_iff]

Finite standard-form encoding

section Encodingvariable [DecidableEq V]

The internal vertices at which flow is conserved.

abbrev Internal (N : FlowNetwork V) := {u : V // u ≠ N.source ∧ u ≠ N.sink}

The general-form program for the maximum-flow LP: one nonnegative variable per ordered pair, a capacity inequality per ordered pair, and a conservation equality per internal vertex.

noncomputable def toGeneralLP (N : FlowNetwork V) : GeneralLP where
  n := Fintype.card (V × V)
  m := Fintype.card (V × V) + Fintype.card (Internal N)
  maximize := true
  c := fun j =>
    (if ((Fintype.equivFin (V × V)).symm j).1 = N.source then 1 else 0) -
      (if ((Fintype.equivFin (V × V)).symm j).2 = N.source then 1 else 0)
  rel := fun i =>
    Fin.addCases (motive := fun _ => ConstraintRel)
      (fun _ => ConstraintRel.le)
      (fun _ => ConstraintRel.eq)
      i
  A := fun i =>
    Fin.addCases (motive := fun _ => Fin (Fintype.card (V × V)) → ℝ)
      (fun e j => if j = e then 1 else 0)
      (fun u j =>
        let v := ((Fintype.equivFin (Internal N)).symm u).1
        (if ((Fintype.equivFin (V × V)).symm j).1 = v then 1 else 0) -
          (if ((Fintype.equivFin (V × V)).symm j).2 = v then 1 else 0))
      i
  b := fun i =>
    Fin.addCases (motive := fun _ => ℝ)
      (fun e => N.capacity ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2)
      (fun _ => 0)
      i
  free := fun _ => false

The index of the capacity constraint for a directed pair.

abbrev capIndex (N : FlowNetwork V) (e : Fin (Fintype.card (V × V))) :
    Fin (Fintype.card (V × V) + Fintype.card (Internal N)) :=
  Fin.castAdd (Fintype.card (Internal N)) e

The index of the conservation constraint for an internal vertex.

abbrev consIndex (N : FlowNetwork V) (u : Fin (Fintype.card (Internal N))) :
    Fin (Fintype.card (V × V) + Fintype.card (Internal N)) :=
  Fin.natAdd (Fintype.card (V × V)) u

              

lemma A_cap (N : FlowNetwork V) (e : Fin (Fintype.card (V × V))) (j : Fin (Fintype.card (V × V))) :
    (toGeneralLP N).A (capIndex N e) j = if j = e then 1 else 0 := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]

lemma b_cap (N : FlowNetwork V) (e : Fin (Fintype.card (V × V))) :
    (toGeneralLP N).b (capIndex N e) =
      N.capacity ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2 := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]

lemma rel_cap (N : FlowNetwork V) (e : Fin (Fintype.card (V × V))) :
    (toGeneralLP N).rel (capIndex N e) = ConstraintRel.le := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]

lemma A_cons (N : FlowNetwork V) (u : Fin (Fintype.card (Internal N))) (j : Fin (Fintype.card (V × V))) :
    (toGeneralLP N).A (consIndex N u) j =
      (if ((Fintype.equivFin (V × V)).symm j).1 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) -
        (if ((Fintype.equivFin (V × V)).symm j).2 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_natAdd]

lemma b_cons (N : FlowNetwork V) (u : Fin (Fintype.card (Internal N))) :
    (toGeneralLP N).b (consIndex N u) = 0 := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_natAdd]

lemma rel_cons (N : FlowNetwork V) (u : Fin (Fintype.card (Internal N))) :
    (toGeneralLP N).rel (consIndex N u) = ConstraintRel.eq := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_natAdd]

A capacity row reads out the gross flow on its directed pair.

lemma mulVec_cap (N : FlowNetwork V) (e : Fin (Fintype.card (V × V))) (f : V → V → ℝ) :
    ((toGeneralLP N).A *ᵥ FinEncoding.lift₂ f) (capIndex N e) = FinEncoding.lift₂ f e := by
  calc
    ((toGeneralLP N).A *ᵥ FinEncoding.lift₂ f) (capIndex N e)
        = ∑ j : Fin (Fintype.card (V × V)), (toGeneralLP N).A (capIndex N e) j * FinEncoding.lift₂ f j := by rfl
    _ = ∑ j : Fin (Fintype.card (V × V)), (if j = e then 1 else 0) * FinEncoding.lift₂ f j := by
          simp only [A_cap]
    _ = FinEncoding.lift₂ f e := FinEncoding.sum_indicator_fin e (FinEncoding.lift₂ f)

A conservation row reads out the net outflow at its vertex.


lemma mulVec_cons (N : FlowNetwork V) (u : Fin (Fintype.card (Internal N))) (f : V → V → ℝ) :
    ((toGeneralLP N).A *ᵥ FinEncoding.lift₂ f) (consIndex N u) =
      FlowNetwork.outflow f ((Fintype.equivFin (Internal N)).symm u).1 -
        FlowNetwork.inflow f ((Fintype.equivFin (Internal N)).symm u).1 := by
  calc
    ((toGeneralLP N).A *ᵥ FinEncoding.lift₂ f) (consIndex N u)
        = ∑ j : Fin (Fintype.card (V × V)), (toGeneralLP N).A (consIndex N u) j * FinEncoding.lift₂ f j := by rfl
    _ = ∑ j : Fin (Fintype.card (V × V)),
          ((if ((Fintype.equivFin (V × V)).symm j).1 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) -
             (if ((Fintype.equivFin (V × V)).symm j).2 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0)) *
            FinEncoding.lift₂ f j := by
          simp only [A_cons]
    _ = (∑ j : Fin (Fintype.card (V × V)),
          (if ((Fintype.equivFin (V × V)).symm j).1 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) * FinEncoding.lift₂ f j) -
          (∑ j : Fin (Fintype.card (V × V)),
          (if ((Fintype.equivFin (V × V)).symm j).2 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) * FinEncoding.lift₂ f j) := by
          simp only [sub_mul, Finset.sum_sub_distrib]
    _ = (∑ b : V, f ((Fintype.equivFin (Internal N)).symm u).1 b) -
          (∑ b : V, f b ((Fintype.equivFin (Internal N)).symm u).1) := by
          rw [FinEncoding.sum_indicator_fst, FinEncoding.sum_indicator_snd]
    _ = FlowNetwork.outflow f ((Fintype.equivFin (Internal N)).symm u).1 -
          FlowNetwork.inflow f ((Fintype.equivFin (Internal N)).symm u).1 := rfl

Semantic feasibility is exactly encoded general-form feasibility.


theorem feasible_iff_generalLP (N : FlowNetwork V) (f : V → V → ℝ) :
    IsFeasible N f ↔ (toGeneralLP N).IsFeasible (FinEncoding.lift₂ f) := by
  unfold IsFeasible GeneralLP.IsFeasible
  constructor
  · intro hd
    refine ⟨?_, ?_⟩
    · intro j hfree
      simpa [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry] using
        (hd.1 ((Fintype.equivFin (V × V)).symm j).1 ((Fintype.equivFin (V × V)).symm j).2)
    · intro i
      exact Fin.addCases (motive := fun i => match (toGeneralLP N).rel i with
          | ConstraintRel.le => ((toGeneralLP N).A *ᵥ FinEncoding.lift₂ f) i ≤ (toGeneralLP N).b i
          | ConstraintRel.eq => ((toGeneralLP N).A *ᵥ FinEncoding.lift₂ f) i = (toGeneralLP N).b i
          | ConstraintRel.ge => (toGeneralLP N).b i ≤ ((toGeneralLP N).A *ᵥ FinEncoding.lift₂ f) i)
        (fun e => by
          rw [rel_cap, mulVec_cap, b_cap]
          simpa [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry] using
            (hd.2.1 ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2))
        (fun u => by
          rw [rel_cons, mulVec_cons, b_cons]
          have hc := hd.2.2 ((Fintype.equivFin (Internal N)).symm u).1
            ((Fintype.equivFin (Internal N)).symm u).2.1
            ((Fintype.equivFin (Internal N)).symm u).2.2
          unfold FlowNetwork.ConservesAt at hc
          linarith)
        i
  · intro h
    refine ⟨?_, ?_, ?_⟩
    · intro u v
      have hn := h.1 (Fintype.equivFin (V × V) (u, v))
      simpa [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry] using (hn (by simp [toGeneralLP]))
    · intro u v
      have hc := h.2 (capIndex N (Fintype.equivFin (V × V) (u, v)))
      rw [rel_cap] at hc
      rw [mulVec_cap, b_cap] at hc
      simpa [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry] using hc
    · intro u hu hw
      let e : Internal N := ⟨u, ⟨hu, hw⟩⟩
      have hcons := h.2 (consIndex N (Fintype.equivFin (Internal N) e))
      rw [rel_cons] at hcons
      rw [mulVec_cons, b_cons] at hcons
      have hcons' : FlowNetwork.outflow f u - FlowNetwork.inflow f u = 0 := by
        simpa [e] using hcons
      unfold FlowNetwork.ConservesAt
      linarith

The general-form objective is the textbook maximum-flow objective.


lemma objective_generalLP (N : FlowNetwork V) (f : V → V → ℝ) :
    (toGeneralLP N).objective (FinEncoding.lift₂ f) = objective N f := by
  dsimp [GeneralLP.objective, toGeneralLP, objective, FlowNetwork.netOutflow, FlowNetwork.outflow, FlowNetwork.inflow]
  simp only [dotProduct, sub_mul, Finset.sum_sub_distrib]
  rw [FinEncoding.sum_indicator_fst, FinEncoding.sum_indicator_snd]

The finite standard-form program obtained by normalizing the maximum-flow general program.

noncomputable def toStandardLP (N : FlowNetwork V) :=
  (toGeneralLP N).toStandardLP

The expansion of a gross-flow vector to the normalized standard-form variable vector.

noncomputable def fullLift (N : FlowNetwork V) (f : V → V → ℝ) :
    Fin (Fintype.card (V × V) + Fintype.card (V × V)) → ℝ :=
  (toGeneralLP N).lift (FinEncoding.lift₂ f)

The normalized standard-form objective is the maximum-flow objective.


theorem objective_toStandardLP (N : FlowNetwork V) (f : V → V → ℝ) :
    (toStandardLP N).objective (fullLift N f) = objective N f := by
  unfold toStandardLP fullLift
  rw [GeneralLP.objective_lift]
  rw [objective_generalLP]
  simp [toGeneralLP, GeneralLP.objectiveSign]

Feasibility is exactly preserved under the finite standard-form encoding.


theorem feasible_iff_toStandardLP (N : FlowNetwork V) (f : V → V → ℝ) :
    IsFeasible N f ↔ (toStandardLP N).IsFeasible (fullLift N f) := by
  unfold toStandardLP fullLift
  rw [← GeneralLP.feasible_iff_lift]
  exact feasible_iff_generalLP N f

              end Encodingend MaximumFlowLPend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.MinimumCostFlow

29.2: Minimum-cost flow as a linear program

In addition to capacities, a network assigns a unit cost to every directed pair. A demand-d flow has net source outflow d; minimizing the sum of unit cost times flow gives the CLRS minimum-cost-flow formulation.

This module also records the finite standard-form encoding: one nonnegative variable per ordered pair, a capacity inequality per ordered pair, a conservation equality per internal vertex, and one source-demand equality, reindexed into a concrete StandardLP.

              namespace CLRSnamespace Chapter29open Finsetopen Matrixopen scoped BigOperators

A capacitated network with a real unit cost on each directed pair.

structure CostedFlowNetwork (V : Type*) [Fintype V] extends FlowNetwork V where
  cost : V → V → ℝ

namespace MinimumCostFlowLPvariable {V : Type*} [Fintype V] (N : CostedFlowNetwork V) (demand : ℝ)

The capacity, conservation, and exact-demand constraints.

def IsFeasible (f : V → V → ℝ) : Prop :=
  N.toFlowNetwork.IsFlow f ∧
    FlowNetwork.netOutflow f N.source = demand

Total cost Σ_u Σ_v a_uv f_uv.

def objective (f : V → V → ℝ) : ℝ :=
  ∑ u, ∑ v, N.cost u v * f u v

A demand flow of minimum total cost.

def IsOptimal (f : V → V → ℝ) : Prop :=
  IsFeasible N demand f ∧
    ∀ g, IsFeasible N demand g → objective N f ≤ objective N g

The LP constraints are exactly capacity-feasible flow plus the prescribed source demand.

theorem isFeasible_iff (f : V → V → ℝ) :
    IsFeasible N demand f ↔
      N.toFlowNetwork.IsFlow f ∧
        FlowNetwork.netOutflow f N.source = demand := by
  rfl

The minimization specification agrees exactly with minimum-cost demand flow.

theorem isOptimal_iff (f : V → V → ℝ) :
    IsOptimal N demand f ↔
      (N.toFlowNetwork.IsFlow f ∧
        FlowNetwork.netOutflow f N.source = demand) ∧
      ∀ g, (N.toFlowNetwork.IsFlow g ∧
        FlowNetwork.netOutflow g N.source = demand) →
        (∑ u, ∑ v, N.cost u v * f u v) ≤
          ∑ u, ∑ v, N.cost u v * g u v := by
  rfl

Finite standard-form encoding

section Encodingvariable [DecidableEq V]

The internal vertices at which flow is conserved.

abbrev Internal (N : CostedFlowNetwork V) := {u : V // u ≠ N.source ∧ u ≠ N.sink}

The general-form program for the minimum-cost-flow LP: one nonnegative variable per ordered pair, a capacity inequality per ordered pair, a conservation equality per internal vertex, and a source-demand equality. The objective is minimized (cost is the sum of unit cost times flow).

noncomputable def toGeneralLP (N : CostedFlowNetwork V) (demand : ℝ) : GeneralLP where
  n := Fintype.card (V × V)
  m := Fintype.card (V × V) + Fintype.card (Internal N) + 1
  maximize := false
  c := fun j => N.cost ((Fintype.equivFin (V × V)).symm j).1 ((Fintype.equivFin (V × V)).symm j).2
  rel := fun i =>
    Fin.cases
      (ConstraintRel.eq)
      (fun i => Fin.addCases (motive := fun _ => ConstraintRel)
        (fun _ => ConstraintRel.le)
        (fun _ => ConstraintRel.eq)
        i)
      i
  A := fun i =>
    Fin.cases
      (fun j =>
        (if ((Fintype.equivFin (V × V)).symm j).1 = N.source then 1 else 0) -
          (if ((Fintype.equivFin (V × V)).symm j).2 = N.source then 1 else 0))
      (fun i j => Fin.addCases (motive := fun _ => ℝ)
        (fun e => if j = e then 1 else 0)
        (fun u =>
          let v := ((Fintype.equivFin (Internal N)).symm u).1
          (if ((Fintype.equivFin (V × V)).symm j).1 = v then 1 else 0) -
            (if ((Fintype.equivFin (V × V)).symm j).2 = v then 1 else 0))
        i)
      i
  b := fun i =>
    Fin.cases
      (demand)
      (fun i => Fin.addCases (motive := fun _ => ℝ)
        (fun e => N.capacity ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2)
        (fun _ => 0)
        i)
      i
  free := fun _ => false

The index of the source-demand equality constraint.

abbrev demandIndex (N : CostedFlowNetwork V) :
    Fin (Fintype.card (V × V) + Fintype.card (Internal N) + 1) := 0

The index of the capacity constraint for a directed pair.

abbrev capIndex (N : CostedFlowNetwork V) (e : Fin (Fintype.card (V × V))) :
    Fin (Fintype.card (V × V) + Fintype.card (Internal N) + 1) :=
  (Fin.castAdd (Fintype.card (Internal N)) e).succ

The index of the conservation constraint for an internal vertex.

abbrev consIndex (N : CostedFlowNetwork V) (u : Fin (Fintype.card (Internal N))) :
    Fin (Fintype.card (V × V) + Fintype.card (Internal N) + 1) :=
  (Fin.natAdd (Fintype.card (V × V)) u).succ

              lemma A_demand (N : CostedFlowNetwork V) (demand : ℝ) (j : Fin (Fintype.card (V × V))) :
    (toGeneralLP N demand).A (demandIndex N) j =
      (if ((Fintype.equivFin (V × V)).symm j).1 = N.source then 1 else 0) -
        (if ((Fintype.equivFin (V × V)).symm j).2 = N.source then 1 else 0) := by
  simp [toGeneralLP, demandIndex]lemma b_demand (N : CostedFlowNetwork V) (demand : ℝ) :
    (toGeneralLP N demand).b (demandIndex N) = demand := by
  simp [toGeneralLP, demandIndex]lemma rel_demand (N : CostedFlowNetwork V) (demand : ℝ) :
    (toGeneralLP N demand).rel (demandIndex N) = ConstraintRel.eq := by
  simp [toGeneralLP, demandIndex]

lemma A_cap (N : CostedFlowNetwork V) (demand : ℝ) (e : Fin (Fintype.card (V × V))) (j : Fin (Fintype.card (V × V))) :
    (toGeneralLP N demand).A (capIndex N e) j = if j = e then 1 else 0 := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]

lemma b_cap (N : CostedFlowNetwork V) (demand : ℝ) (e : Fin (Fintype.card (V × V))) :
    (toGeneralLP N demand).b (capIndex N e) =
      N.capacity ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2 := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]

lemma rel_cap (N : CostedFlowNetwork V) (demand : ℝ) (e : Fin (Fintype.card (V × V))) :
    (toGeneralLP N demand).rel (capIndex N e) = ConstraintRel.le := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]

lemma A_cons (N : CostedFlowNetwork V) (demand : ℝ) (u : Fin (Fintype.card (Internal N))) (j : Fin (Fintype.card (V × V))) :
    (toGeneralLP N demand).A (consIndex N u) j =
      (if ((Fintype.equivFin (V × V)).symm j).1 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) -
        (if ((Fintype.equivFin (V × V)).symm j).2 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_natAdd]

lemma b_cons (N : CostedFlowNetwork V) (demand : ℝ) (u : Fin (Fintype.card (Internal N))) :
    (toGeneralLP N demand).b (consIndex N u) = 0 := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_natAdd]

lemma rel_cons (N : CostedFlowNetwork V) (demand : ℝ) (u : Fin (Fintype.card (Internal N))) :
    (toGeneralLP N demand).rel (consIndex N u) = ConstraintRel.eq := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_natAdd]

The demand row reads out the source net outflow.


lemma mulVec_demand (N : CostedFlowNetwork V) (demand : ℝ) (f : V → V → ℝ) :
    ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) (demandIndex N) =
      FlowNetwork.netOutflow f N.source := by
  calc
    ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) (demandIndex N)
        = ∑ j : Fin (Fintype.card (V × V)), (toGeneralLP N demand).A (demandIndex N) j * FinEncoding.lift₂ f j := by rfl
    _ = ∑ j : Fin (Fintype.card (V × V)),
          ((if ((Fintype.equivFin (V × V)).symm j).1 = N.source then 1 else 0) -
             (if ((Fintype.equivFin (V × V)).symm j).2 = N.source then 1 else 0)) *
            FinEncoding.lift₂ f j := by
          simp only [A_demand]
    _ = (∑ j : Fin (Fintype.card (V × V)),
          (if ((Fintype.equivFin (V × V)).symm j).1 = N.source then 1 else 0) * FinEncoding.lift₂ f j) -
          (∑ j : Fin (Fintype.card (V × V)),
          (if ((Fintype.equivFin (V × V)).symm j).2 = N.source then 1 else 0) * FinEncoding.lift₂ f j) := by
          simp only [sub_mul, Finset.sum_sub_distrib]
    _ = (∑ b : V, f N.source b) - (∑ b : V, f b N.source) := by
          rw [FinEncoding.sum_indicator_fst, FinEncoding.sum_indicator_snd]
    _ = FlowNetwork.netOutflow f N.source := rfl

A capacity row reads out the gross flow on its directed pair.

lemma mulVec_cap (N : CostedFlowNetwork V) (demand : ℝ) (e : Fin (Fintype.card (V × V))) (f : V → V → ℝ) :
    ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) (capIndex N e) = FinEncoding.lift₂ f e := by
  calc
    ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) (capIndex N e)
        = ∑ j : Fin (Fintype.card (V × V)), (toGeneralLP N demand).A (capIndex N e) j * FinEncoding.lift₂ f j := by rfl
    _ = ∑ j : Fin (Fintype.card (V × V)), (if j = e then 1 else 0) * FinEncoding.lift₂ f j := by
          simp only [A_cap]
    _ = FinEncoding.lift₂ f e := FinEncoding.sum_indicator_fin e (FinEncoding.lift₂ f)

A conservation row reads out the net outflow at its vertex.


lemma mulVec_cons (N : CostedFlowNetwork V) (demand : ℝ) (u : Fin (Fintype.card (Internal N))) (f : V → V → ℝ) :
    ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) (consIndex N u) =
      FlowNetwork.outflow f ((Fintype.equivFin (Internal N)).symm u).1 -
        FlowNetwork.inflow f ((Fintype.equivFin (Internal N)).symm u).1 := by
  calc
    ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) (consIndex N u)
        = ∑ j : Fin (Fintype.card (V × V)), (toGeneralLP N demand).A (consIndex N u) j * FinEncoding.lift₂ f j := by rfl
    _ = ∑ j : Fin (Fintype.card (V × V)),
          ((if ((Fintype.equivFin (V × V)).symm j).1 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) -
             (if ((Fintype.equivFin (V × V)).symm j).2 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0)) *
            FinEncoding.lift₂ f j := by
          simp only [A_cons]
    _ = (∑ j : Fin (Fintype.card (V × V)),
          (if ((Fintype.equivFin (V × V)).symm j).1 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) * FinEncoding.lift₂ f j) -
          (∑ j : Fin (Fintype.card (V × V)),
          (if ((Fintype.equivFin (V × V)).symm j).2 = ((Fintype.equivFin (Internal N)).symm u).1 then 1 else 0) * FinEncoding.lift₂ f j) := by
          simp only [sub_mul, Finset.sum_sub_distrib]
    _ = (∑ b : V, f ((Fintype.equivFin (Internal N)).symm u).1 b) -
          (∑ b : V, f b ((Fintype.equivFin (Internal N)).symm u).1) := by
          rw [FinEncoding.sum_indicator_fst, FinEncoding.sum_indicator_snd]
    _ = FlowNetwork.outflow f ((Fintype.equivFin (Internal N)).symm u).1 -
          FlowNetwork.inflow f ((Fintype.equivFin (Internal N)).symm u).1 := rfl

Semantic feasibility is exactly encoded general-form feasibility.


theorem feasible_iff_generalLP (N : CostedFlowNetwork V) (demand : ℝ) (f : V → V → ℝ) :
    IsFeasible N demand f ↔ (toGeneralLP N demand).IsFeasible (FinEncoding.lift₂ f) := by
  unfold IsFeasible GeneralLP.IsFeasible FlowNetwork.IsFlow FlowNetwork.IsCapacityFeasible
  constructor
  · intro hd
    refine ⟨?_, ?_⟩
    · intro j hfree
      simpa [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry] using
        (hd.1.1.1 ((Fintype.equivFin (V × V)).symm j).1 ((Fintype.equivFin (V × V)).symm j).2)
    · intro i
      exact Fin.cases (motive := fun i => match (toGeneralLP N demand).rel i with
          | ConstraintRel.le => ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) i ≤ (toGeneralLP N demand).b i
          | ConstraintRel.eq => ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) i = (toGeneralLP N demand).b i
          | ConstraintRel.ge => (toGeneralLP N demand).b i ≤ ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) i)
        (by
          rw [rel_demand, mulVec_demand, b_demand]
          exact hd.2)
        (fun i => by
          exact Fin.addCases (motive := fun i => match (toGeneralLP N demand).rel i.succ with
              | ConstraintRel.le => ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) i.succ ≤ (toGeneralLP N demand).b i.succ
              | ConstraintRel.eq => ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) i.succ = (toGeneralLP N demand).b i.succ
              | ConstraintRel.ge => (toGeneralLP N demand).b i.succ ≤ ((toGeneralLP N demand).A *ᵥ FinEncoding.lift₂ f) i.succ)
            (fun e => by
              rw [rel_cap, mulVec_cap, b_cap]
              simpa [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry] using
                (hd.1.1.2 ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2))
            (fun u => by
              rw [rel_cons, mulVec_cons, b_cons]
              have hc := hd.1.2 ((Fintype.equivFin (Internal N)).symm u).1
                ((Fintype.equivFin (Internal N)).symm u).2.1
                ((Fintype.equivFin (Internal N)).symm u).2.2
              unfold FlowNetwork.ConservesAt at hc
              linarith)
            i)
        i
  · intro h
    refine ⟨⟨⟨?_, ?_⟩, ?_⟩, ?_⟩
    · intro u v
      have hn := h.1 (Fintype.equivFin (V × V) (u, v))
      simpa [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry] using (hn (by simp [toGeneralLP]))
    · intro u v
      have hc := h.2 (capIndex N (Fintype.equivFin (V × V) (u, v)))
      rw [rel_cap] at hc
      rw [mulVec_cap, b_cap] at hc
      simpa [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry] using hc
    · intro u hu hw
      let e : Internal N := ⟨u, ⟨hu, hw⟩⟩
      have hcons := h.2 (consIndex N (Fintype.equivFin (Internal N) e))
      rw [rel_cons] at hcons
      rw [mulVec_cons, b_cons] at hcons
      have hcons' : FlowNetwork.outflow f u - FlowNetwork.inflow f u = 0 := by
        simpa [e] using hcons
      unfold FlowNetwork.ConservesAt
      linarith
    · have hdemand := h.2 (demandIndex N)
      rw [rel_demand] at hdemand
      rw [mulVec_demand, b_demand] at hdemand
      exact hdemand

The general-form objective is the total cost (minimized).


lemma objective_generalLP (N : CostedFlowNetwork V) (demand : ℝ) (f : V → V → ℝ) :
    (toGeneralLP N demand).objective (FinEncoding.lift₂ f) = objective N f := by
  dsimp [GeneralLP.objective, toGeneralLP, objective]
  simp only [dotProduct]
  rw [FinEncoding.sum_reindex]
  simp [FinEncoding.lift₂, FinEncoding.lift, Function.uncurry]
  rw [Fintype.sum_prod_type]

The finite standard-form program obtained by normalizing the minimum-cost general program.

noncomputable def toStandardLP (N : CostedFlowNetwork V) (demand : ℝ) :=
  (toGeneralLP N demand).toStandardLP

The expansion of a gross-flow vector to the normalized standard-form variable vector.

noncomputable def fullLift (N : CostedFlowNetwork V) (demand : ℝ) (f : V → V → ℝ) :
    Fin (Fintype.card (V × V) + Fintype.card (V × V)) → ℝ :=
  (toGeneralLP N demand).lift (FinEncoding.lift₂ f)

The normalized standard-form objective equals the signed total cost.


theorem objective_toStandardLP (N : CostedFlowNetwork V) (demand : ℝ) (f : V → V → ℝ) :
    (toStandardLP N demand).objective (fullLift N demand f) = -objective N f := by
  unfold toStandardLP fullLift
  rw [GeneralLP.objective_lift]
  rw [objective_generalLP]
  simp [toGeneralLP, GeneralLP.objectiveSign]

Feasibility is exactly preserved under the finite standard-form encoding.


theorem feasible_iff_toStandardLP (N : CostedFlowNetwork V) (demand : ℝ) (f : V → V → ℝ) :
    IsFeasible N demand f ↔ (toStandardLP N demand).IsFeasible (fullLift N demand f) := by
  unfold toStandardLP fullLift
  rw [← GeneralLP.feasible_iff_lift]
  exact feasible_iff_generalLP N demand f

              end Encodingend MinimumCostFlowLPend Chapter29end CLRS

CLRSLean.FourthEdition.Chapter_29.Section_29_2_Formulating_Problems_As_Linear_Programs.MulticommodityFlow

29.2: Multicommodity flow as a linear program

Each commodity has its own source, sink, demand, and nonnegative gross flow. All commodities share the edge capacities. The optional cost objective also records Exercise 29.2-7's minimum-cost multicommodity formulation.

This module also records the finite standard-form encoding: one nonnegative variable per commodity/ordered-pair, a shared capacity inequality per ordered pair, a conservation equality per internal commodity/vertex, and a demand equality per commodity, reindexed into a concrete StandardLP.

              namespace CLRSnamespace Chapter29open Finsetopen Matrixopen scoped BigOperators

Source, sink, and nonnegative demand of one commodity.

structure Commodity (V : Type*) where
  source : V
  sink : V
  source_ne_sink : source ≠ sink
  demand : ℝ
  demand_nonnegative : 0 ≤ demand

namespace MulticommodityFlowLPvariable {V K : Type*} [Fintype V] [Fintype K]

Total flow of all commodities on one directed pair.

def aggregate (f : K → V → V → ℝ) (u v : V) : ℝ := ∑ i, f i u v

The CLRS multicommodity feasibility constraints.

def IsFeasible (N : FlowNetwork V) (commodity : K → Commodity V)
    (f : K → V → V → ℝ) : Prop :=
  (∀ i u v, 0 ≤ f i u v) ∧
  (∀ u v, aggregate f u v ≤ N.capacity u v) ∧
  (∀ i u, u ≠ (commodity i).source → u ≠ (commodity i).sink →
    FlowNetwork.ConservesAt (f i) u) ∧
  ∀ i, FlowNetwork.netOutflow (f i) (commodity i).source = (commodity i).demand

An expanded statement of the displayed multicommodity LP.

theorem isFeasible_iff (N : FlowNetwork V) (commodity : K → Commodity V)
    (f : K → V → V → ℝ) :
    IsFeasible N commodity f ↔
      (∀ i u v, 0 ≤ f i u v) ∧
      (∀ u v, (∑ i, f i u v) ≤ N.capacity u v) ∧
      (∀ i u, u ≠ (commodity i).source → u ≠ (commodity i).sink →
        FlowNetwork.inflow (f i) u = FlowNetwork.outflow (f i) u) ∧
      ∀ i, FlowNetwork.outflow (f i) (commodity i).source -
          FlowNetwork.inflow (f i) (commodity i).source = (commodity i).demand := by
  rfl

Total cost of the aggregate multicommodity flow.

def cost (unitCost : V → V → ℝ) (f : K → V → V → ℝ) : ℝ :=
  ∑ u, ∑ v, unitCost u v * aggregate f u v

Minimum-cost feasible multicommodity routing.

def IsMinimumCost (N : FlowNetwork V) (commodity : K → Commodity V)
    (unitCost : V → V → ℝ) (f : K → V → V → ℝ) : Prop :=
  IsFeasible N commodity f ∧
    ∀ g, IsFeasible N commodity g → cost unitCost f ≤ cost unitCost g

Expanded optimality statement for minimum-cost multicommodity flow.

theorem isMinimumCost_iff (N : FlowNetwork V) (commodity : K → Commodity V)
    (unitCost : V → V → ℝ) (f : K → V → V → ℝ) :
    IsMinimumCost N commodity unitCost f ↔
      IsFeasible N commodity f ∧
      ∀ g, IsFeasible N commodity g →
        (∑ u, ∑ v, unitCost u v * (∑ i, f i u v)) ≤
          ∑ u, ∑ v, unitCost u v * (∑ i, g i u v) := by
  rfl

Finite standard-form encoding

section Encodingvariable [DecidableEq V] [DecidableEq K]

Lift a commodity-indexed flow to the Fin-indexed vector over K × (V × V).

noncomputable def lift₃ (f : K → V → V → ℝ) : Fin (Fintype.card (K × (V × V))) → ℝ :=
  FinEncoding.lift (fun p : K × (V × V) => f p.1 p.2.1 p.2.2)

The internal commodity/vertex pairs at which flow is conserved.

abbrev Internal (Variable name `N` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`N : FlowNetwork V) (commodity : K → Commodity V) :=
  {p : K × V // p.2 ≠ (commodity p.1).source ∧ p.2 ≠ (commodity p.1).sink}

Sum of an indicator on the commodity and the source coordinate (outflow).


lemma sum_indicator_fst_fst (i : K) (u : V) (f : K → V → V → ℝ) :
    (∑ j : Fin (Fintype.card (K × (V × V))),
      (if ((Fintype.equivFin (K × (V × V))).symm j).1 = i ∧
           ((Fintype.equivFin (K × (V × V))).symm j).2.1 = u then 1 else 0) * lift₃ f j) =
      ∑ b : V, f i u b := by
  rw [FinEncoding.sum_reindex]
  simp [lift₃, FinEncoding.lift]
  rw [Fintype.sum_prod_type]
  rw [Finset.sum_eq_single i]
  · rw [Fintype.sum_prod_type]
    rw [Finset.sum_eq_single u]
    · simp
    · intro a _ ha; simp [ha]
    · intro h; exact False.elim (h (Finset.mem_univ u))
  · intro k _ hk; simp [hk]
  · intro h; exact False.elim (h (Finset.mem_univ i))

Sum of an indicator on the commodity and the target coordinate (inflow).


lemma sum_indicator_fst_snd (i : K) (u : V) (f : K → V → V → ℝ) :
    (∑ j : Fin (Fintype.card (K × (V × V))),
      (if ((Fintype.equivFin (K × (V × V))).symm j).1 = i ∧
           ((Fintype.equivFin (K × (V × V))).symm j).2.2 = u then 1 else 0) * lift₃ f j) =
      ∑ a : V, f i a u := by
  rw [FinEncoding.sum_reindex]
  simp [lift₃, FinEncoding.lift]
  rw [Fintype.sum_prod_type]
  rw [Finset.sum_eq_single i]
  · rw [Fintype.sum_prod_type]
    rw [Finset.sum_comm]
    rw [Finset.sum_eq_single u]
    · simp
    · intro a _ ha; simp [ha]
    · intro h; exact False.elim (h (Finset.mem_univ u))
  · intro k _ hk; simp [hk]
  · intro h; exact False.elim (h (Finset.mem_univ i))

Sum of an indicator on the directed pair (shared capacity).

automatically included section variable(s) unused in theorem `CLRS.Chapter29.MulticommodityFlowLP.sum_indicator_pair`:
  [DecidableEq K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter29.MulticommodityFlowLP.sum_indicator_pair`:
  [DecidableEq K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter29.MulticommodityFlowLP.sum_indicator_pair`:
  [DecidableEq K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter29.MulticommodityFlowLP.sum_indicator_pair`:
  [DecidableEq K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter29.MulticommodityFlowLP.sum_indicator_pair`:
  [DecidableEq K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter29.MulticommodityFlowLP.sum_indicator_pair`:
  [DecidableEq K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.Chapter29.MulticommodityFlowLP.sum_indicator_pair`:
  [DecidableEq K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
automatically included section variable(s) unused in theorem `CLRS.Chapter29.MulticommodityFlowLP.sum_indicator_pair`:
  [DecidableEq K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma sum_indicator_pair (u v : V) (f : K → V → V → ℝ) :
    (∑ j : Fin (Fintype.card (K × (V × V))),
      (if ((Fintype.equivFin (K × (V × V))).symm j).2 = (u, v) then 1 else 0) * lift₃ f j) =
      ∑ i : K, f i u v := by
  rw [FinEncoding.sum_reindex]
  simp [lift₃, FinEncoding.lift]
  rw [Fintype.sum_prod_type]
  simp [Finset.sum_ite_eq']

The general-form program for the multicommodity-flow LP.

noncomputable def toGeneralLP (N : FlowNetwork V) (commodity : K → Commodity V)
    (unitCost : V → V → ℝ) : GeneralLP where
  n := Fintype.card (K × (V × V))
  m := Fintype.card (V × V) + Fintype.card (Internal N commodity) + Fintype.card K
  maximize := false
  c := fun j => unitCost ((Fintype.equivFin (K × (V × V))).symm j).2.1 ((Fintype.equivFin (K × (V × V))).symm j).2.2
  rel := fun i =>
    Fin.addCases (motive := fun _ => ConstraintRel)
      (fun ij => Fin.addCases (motive := fun _ => ConstraintRel)
        (fun _ => ConstraintRel.le)
        (fun _ => ConstraintRel.eq)
        ij)
      (fun _ => ConstraintRel.eq)
      i
  A := fun i =>
    Fin.addCases (motive := fun _ => Fin (Fintype.card (K × (V × V))) → ℝ)
      (fun ij => Fin.addCases (motive := fun _ => Fin (Fintype.card (K × (V × V))) → ℝ)
        (fun e j => if ((Fintype.equivFin (K × (V × V))).symm j).2 = (Fintype.equivFin (V × V)).symm e then 1 else 0)
        (fun p j =>
          let iu := (Fintype.equivFin (Internal N commodity)).symm p
          (if ((Fintype.equivFin (K × (V × V))).symm j).1 = iu.1.1 ∧
               ((Fintype.equivFin (K × (V × V))).symm j).2.1 = iu.1.2 then 1 else 0) -
            (if ((Fintype.equivFin (K × (V × V))).symm j).1 = iu.1.1 ∧
                 ((Fintype.equivFin (K × (V × V))).symm j).2.2 = iu.1.2 then 1 else 0))
        ij)
      (fun i j =>
        let ci := (Fintype.equivFin K).symm i
        (if ((Fintype.equivFin (K × (V × V))).symm j).1 = ci ∧
             ((Fintype.equivFin (K × (V × V))).symm j).2.1 = (commodity ci).source then 1 else 0) -
          (if ((Fintype.equivFin (K × (V × V))).symm j).1 = ci ∧
               ((Fintype.equivFin (K × (V × V))).symm j).2.2 = (commodity ci).source then 1 else 0))
      i
  b := fun i =>
    Fin.addCases (motive := fun _ => ℝ)
      (fun ij => Fin.addCases (motive := fun _ => ℝ)
        (fun e => N.capacity ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2)
        (fun _ => 0)
        ij)
      (fun i => (commodity ((Fintype.equivFin K).symm i)).demand)
      i
  free := fun _ => false

The index of the shared-capacity constraint for a directed pair.

abbrev capIndex (N : FlowNetwork V) (commodity : K → Commodity V) (e : Fin (Fintype.card (V × V))) :
    Fin (Fintype.card (V × V) + Fintype.card (Internal N commodity) + Fintype.card K) :=
  Fin.castAdd (Fintype.card K) (Fin.castAdd (Fintype.card (Internal N commodity)) e)

The index of the conservation constraint for an internal commodity/vertex.

abbrev consIndex (N : FlowNetwork V) (commodity : K → Commodity V) (p : Fin (Fintype.card (Internal N commodity))) :
    Fin (Fintype.card (V × V) + Fintype.card (Internal N commodity) + Fintype.card K) :=
  Fin.castAdd (Fintype.card K) (Fin.natAdd (Fintype.card (V × V)) p)

The index of the demand constraint for a commodity.

abbrev demandIndex (N : FlowNetwork V) (commodity : K → Commodity V) (i : Fin (Fintype.card K)) :
    Fin (Fintype.card (V × V) + Fintype.card (Internal N commodity) + Fintype.card K) :=
  Fin.natAdd (Fintype.card (V × V) + Fintype.card (Internal N commodity)) i

              

lemma rel_cap (N : FlowNetwork V) (commodity : K → Commodity V) (e : Fin (Fintype.card (V × V))) :
    (toGeneralLP N commodity (fun _ _ => 0)).rel (capIndex N commodity e) = ConstraintRel.le := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]
  rw [FinEncoding.addCases_castAdd]

lemma b_cap (N : FlowNetwork V) (commodity : K → Commodity V) (e : Fin (Fintype.card (V × V))) :
    (toGeneralLP N commodity (fun _ _ => 0)).b (capIndex N commodity e) =
      N.capacity ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2 := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]
  rw [FinEncoding.addCases_castAdd]

lemma A_cap (N : FlowNetwork V) (commodity : K → Commodity V) (e : Fin (Fintype.card (V × V)))
    (j : Fin (Fintype.card (K × (V × V)))) :
    (toGeneralLP N commodity (fun _ _ => 0)).A (capIndex N commodity e) j =
      if ((Fintype.equivFin (K × (V × V))).symm j).2 = (Fintype.equivFin (V × V)).symm e then 1 else 0 := by
  dsimp [toGeneralLP, capIndex]
  rw [FinEncoding.addCases_castAdd]
  rw [FinEncoding.addCases_castAdd]

lemma rel_cons (N : FlowNetwork V) (commodity : K → Commodity V) (p : Fin (Fintype.card (Internal N commodity))) :
    (toGeneralLP N commodity (fun _ _ => 0)).rel (consIndex N commodity p) = ConstraintRel.eq := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_castAdd]
  rw [FinEncoding.addCases_natAdd]

lemma b_cons (N : FlowNetwork V) (commodity : K → Commodity V) (p : Fin (Fintype.card (Internal N commodity))) :
    (toGeneralLP N commodity (fun _ _ => 0)).b (consIndex N commodity p) = 0 := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_castAdd]
  rw [FinEncoding.addCases_natAdd]

lemma A_cons (N : FlowNetwork V) (commodity : K → Commodity V) (p : Fin (Fintype.card (Internal N commodity)))
    (j : Fin (Fintype.card (K × (V × V)))) :
    (toGeneralLP N commodity (fun _ _ => 0)).A (consIndex N commodity p) j =
      (if ((Fintype.equivFin (K × (V × V))).symm j).1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.1 ∧
           ((Fintype.equivFin (K × (V × V))).symm j).2.1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.2 then 1 else 0) -
        (if ((Fintype.equivFin (K × (V × V))).symm j).1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.1 ∧
             ((Fintype.equivFin (K × (V × V))).symm j).2.2 = ((Fintype.equivFin (Internal N commodity)).symm p).1.2 then 1 else 0) := by
  dsimp [toGeneralLP, consIndex]
  rw [FinEncoding.addCases_castAdd]
  rw [FinEncoding.addCases_natAdd]

lemma rel_demand (N : FlowNetwork V) (commodity : K → Commodity V) (i : Fin (Fintype.card K)) :
    (toGeneralLP N commodity (fun _ _ => 0)).rel (demandIndex N commodity i) = ConstraintRel.eq := by
  dsimp [toGeneralLP, demandIndex]
  rw [FinEncoding.addCases_natAdd]

lemma b_demand (N : FlowNetwork V) (commodity : K → Commodity V) (i : Fin (Fintype.card K)) :
    (toGeneralLP N commodity (fun _ _ => 0)).b (demandIndex N commodity i) =
      (commodity ((Fintype.equivFin K).symm i)).demand := by
  dsimp [toGeneralLP, demandIndex]
  rw [FinEncoding.addCases_natAdd]

lemma A_demand (N : FlowNetwork V) (commodity : K → Commodity V) (i : Fin (Fintype.card K))
    (j : Fin (Fintype.card (K × (V × V)))) :
    (toGeneralLP N commodity (fun _ _ => 0)).A (demandIndex N commodity i) j =
      (if ((Fintype.equivFin (K × (V × V))).symm j).1 = (Fintype.equivFin K).symm i ∧
           ((Fintype.equivFin (K × (V × V))).symm j).2.1 = (commodity ((Fintype.equivFin K).symm i)).source then 1 else 0) -
        (if ((Fintype.equivFin (K × (V × V))).symm j).1 = (Fintype.equivFin K).symm i ∧
             ((Fintype.equivFin (K × (V × V))).symm j).2.2 = (commodity ((Fintype.equivFin K).symm i)).source then 1 else 0) := by
  dsimp [toGeneralLP, demandIndex]
  rw [FinEncoding.addCases_natAdd]

A capacity row reads out the aggregate flow on its directed pair.

lemma mulVec_cap (N : FlowNetwork V) (commodity : K → Commodity V) (e : Fin (Fintype.card (V × V)))
    (f : K → V → V → ℝ) :
    ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (capIndex N commodity e) =
      aggregate f ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2 := by
  calc
    ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (capIndex N commodity e)
        = ∑ j : Fin (Fintype.card (K × (V × V))), (toGeneralLP N commodity (fun _ _ => 0)).A (capIndex N commodity e) j * lift₃ f j := by rfl
    _ = ∑ j : Fin (Fintype.card (K × (V × V))),
          (if ((Fintype.equivFin (K × (V × V))).symm j).2 = (Fintype.equivFin (V × V)).symm e then 1 else 0) * lift₃ f j := by
          simp only [A_cap]
    _ = ∑ i : K, f i ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2 := by
          simpa using (sum_indicator_pair ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2 f)
    _ = aggregate f ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2 := rfl

A conservation row reads out the net outflow of one commodity at its internal vertex.


lemma mulVec_cons (N : FlowNetwork V) (commodity : K → Commodity V) (p : Fin (Fintype.card (Internal N commodity)))
    (f : K → V → V → ℝ) :
    ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (consIndex N commodity p) =
      FlowNetwork.outflow (f ((Fintype.equivFin (Internal N commodity)).symm p).1.1) ((Fintype.equivFin (Internal N commodity)).symm p).1.2 -
        FlowNetwork.inflow (f ((Fintype.equivFin (Internal N commodity)).symm p).1.1) ((Fintype.equivFin (Internal N commodity)).symm p).1.2 := by
  calc
    ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (consIndex N commodity p)
        = ∑ j : Fin (Fintype.card (K × (V × V))), (toGeneralLP N commodity (fun _ _ => 0)).A (consIndex N commodity p) j * lift₃ f j := by rfl
    _ = ∑ j : Fin (Fintype.card (K × (V × V))),
          ((if ((Fintype.equivFin (K × (V × V))).symm j).1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.1 ∧
                ((Fintype.equivFin (K × (V × V))).symm j).2.1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.2 then 1 else 0) -
             (if ((Fintype.equivFin (K × (V × V))).symm j).1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.1 ∧
                  ((Fintype.equivFin (K × (V × V))).symm j).2.2 = ((Fintype.equivFin (Internal N commodity)).symm p).1.2 then 1 else 0)) *
            lift₃ f j := by
          simp only [A_cons]
    _ = (∑ j : Fin (Fintype.card (K × (V × V))),
          (if ((Fintype.equivFin (K × (V × V))).symm j).1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.1 ∧
               ((Fintype.equivFin (K × (V × V))).symm j).2.1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.2 then 1 else 0) * lift₃ f j) -
          (∑ j : Fin (Fintype.card (K × (V × V))),
          (if ((Fintype.equivFin (K × (V × V))).symm j).1 = ((Fintype.equivFin (Internal N commodity)).symm p).1.1 ∧
               ((Fintype.equivFin (K × (V × V))).symm j).2.2 = ((Fintype.equivFin (Internal N commodity)).symm p).1.2 then 1 else 0) * lift₃ f j) := by
          simp only [sub_mul, Finset.sum_sub_distrib]
    _ = (∑ b : V, f ((Fintype.equivFin (Internal N commodity)).symm p).1.1 ((Fintype.equivFin (Internal N commodity)).symm p).1.2 b) -
          (∑ a : V, f ((Fintype.equivFin (Internal N commodity)).symm p).1.1 a ((Fintype.equivFin (Internal N commodity)).symm p).1.2) := by
          rw [sum_indicator_fst_fst, sum_indicator_fst_snd]
    _ = FlowNetwork.outflow (f ((Fintype.equivFin (Internal N commodity)).symm p).1.1) ((Fintype.equivFin (Internal N commodity)).symm p).1.2 -
          FlowNetwork.inflow (f ((Fintype.equivFin (Internal N commodity)).symm p).1.1) ((Fintype.equivFin (Internal N commodity)).symm p).1.2 := rfl

A demand row reads out the net outflow of one commodity at its source.


lemma mulVec_demand (N : FlowNetwork V) (commodity : K → Commodity V) (i : Fin (Fintype.card K))
    (f : K → V → V → ℝ) :
    ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (demandIndex N commodity i) =
      FlowNetwork.netOutflow (f ((Fintype.equivFin K).symm i)) (commodity ((Fintype.equivFin K).symm i)).source := by
  calc
    ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (demandIndex N commodity i)
        = ∑ j : Fin (Fintype.card (K × (V × V))), (toGeneralLP N commodity (fun _ _ => 0)).A (demandIndex N commodity i) j * lift₃ f j := by rfl
    _ = ∑ j : Fin (Fintype.card (K × (V × V))),
          ((if ((Fintype.equivFin (K × (V × V))).symm j).1 = (Fintype.equivFin K).symm i ∧
                ((Fintype.equivFin (K × (V × V))).symm j).2.1 = (commodity ((Fintype.equivFin K).symm i)).source then 1 else 0) -
             (if ((Fintype.equivFin (K × (V × V))).symm j).1 = (Fintype.equivFin K).symm i ∧
                  ((Fintype.equivFin (K × (V × V))).symm j).2.2 = (commodity ((Fintype.equivFin K).symm i)).source then 1 else 0)) *
            lift₃ f j := by
          simp only [A_demand]
    _ = (∑ j : Fin (Fintype.card (K × (V × V))),
          (if ((Fintype.equivFin (K × (V × V))).symm j).1 = (Fintype.equivFin K).symm i ∧
               ((Fintype.equivFin (K × (V × V))).symm j).2.1 = (commodity ((Fintype.equivFin K).symm i)).source then 1 else 0) * lift₃ f j) -
          (∑ j : Fin (Fintype.card (K × (V × V))),
          (if ((Fintype.equivFin (K × (V × V))).symm j).1 = (Fintype.equivFin K).symm i ∧
               ((Fintype.equivFin (K × (V × V))).symm j).2.2 = (commodity ((Fintype.equivFin K).symm i)).source then 1 else 0) * lift₃ f j) := by
          simp only [sub_mul, Finset.sum_sub_distrib]
    _ = (∑ b : V, f ((Fintype.equivFin K).symm i) (commodity ((Fintype.equivFin K).symm i)).source b) -
          (∑ a : V, f ((Fintype.equivFin K).symm i) a (commodity ((Fintype.equivFin K).symm i)).source) := by
          rw [sum_indicator_fst_fst, sum_indicator_fst_snd]
    _ = FlowNetwork.netOutflow (f ((Fintype.equivFin K).symm i)) (commodity ((Fintype.equivFin K).symm i)).source := rfl

Semantic feasibility is exactly encoded general-form feasibility.


theorem feasible_iff_generalLP (N : FlowNetwork V) (commodity : K → Commodity V)
    (f : K → V → V → ℝ) :
    IsFeasible N commodity f ↔ (toGeneralLP N commodity (fun _ _ => 0)).IsFeasible (lift₃ f) := by
  unfold IsFeasible GeneralLP.IsFeasible
  constructor
  · intro hd
    refine ⟨?_, ?_⟩
    · intro j hfree
      simpa [lift₃, FinEncoding.lift] using
        (hd.1 ((Fintype.equivFin (K × (V × V))).symm j).1
          ((Fintype.equivFin (K × (V × V))).symm j).2.1
          ((Fintype.equivFin (K × (V × V))).symm j).2.2)
    · intro i
      exact Fin.addCases (motive := fun i => match (toGeneralLP N commodity (fun _ _ => 0)).rel i with
          | ConstraintRel.le => ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) i ≤ (toGeneralLP N commodity (fun _ _ => 0)).b i
          | ConstraintRel.eq => ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) i = (toGeneralLP N commodity (fun _ _ => 0)).b i
          | ConstraintRel.ge => (toGeneralLP N commodity (fun _ _ => 0)).b i ≤ ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) i)
        (fun ij =>
          Fin.addCases (motive := fun ij => match (toGeneralLP N commodity (fun _ _ => 0)).rel (Fin.castAdd (Fintype.card K) ij) with
              | ConstraintRel.le => ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (Fin.castAdd (Fintype.card K) ij) ≤ (toGeneralLP N commodity (fun _ _ => 0)).b (Fin.castAdd (Fintype.card K) ij)
              | ConstraintRel.eq => ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (Fin.castAdd (Fintype.card K) ij) = (toGeneralLP N commodity (fun _ _ => 0)).b (Fin.castAdd (Fintype.card K) ij)
              | ConstraintRel.ge => (toGeneralLP N commodity (fun _ _ => 0)).b (Fin.castAdd (Fintype.card K) ij) ≤ ((toGeneralLP N commodity (fun _ _ => 0)).A *ᵥ lift₃ f) (Fin.castAdd (Fintype.card K) ij))
            (fun e => by
              rw [rel_cap, mulVec_cap, b_cap]
              simpa [aggregate] using
                (hd.2.1 ((Fintype.equivFin (V × V)).symm e).1 ((Fintype.equivFin (V × V)).symm e).2))
            (fun p => by
              rw [rel_cons, mulVec_cons, b_cons]
              have hc := hd.2.2.1 ((Fintype.equivFin (Internal N commodity)).symm p).1.1
                ((Fintype.equivFin (Internal N commodity)).symm p).1.2
                ((Fintype.equivFin (Internal N commodity)).symm p).2.1
                ((Fintype.equivFin (Internal N commodity)).symm p).2.2
              unfold FlowNetwork.ConservesAt at hc
              linarith)
            ij)
        (fun i => by
          rw [rel_demand, mulVec_demand, b_demand]
          exact hd.2.2.2 ((Fintype.equivFin K).symm i))
        i
  · intro h
    refine ⟨?_, ?_, ?_, ?_⟩
    · intro i u v
      have hn := h.1 (Fintype.equivFin (K × (V × V)) (i, (u, v)))
      simpa [lift₃, FinEncoding.lift] using (hn (by simp [toGeneralLP]))
    · intro u v
      have hc := h.2 (capIndex N commodity (Fintype.equivFin (V × V) (u, v)))
      rw [rel_cap] at hc
      rw [mulVec_cap, b_cap] at hc
      simpa [aggregate] using hc
    · intro i u hu hw
      let e : Internal N commodity := ⟨(i, u), ⟨hu, hw⟩⟩
      have hcons := h.2 (consIndex N commodity (Fintype.equivFin (Internal N commodity) e))
      rw [rel_cons] at hcons
      rw [mulVec_cons, b_cons] at hcons
      have hcons' : FlowNetwork.outflow (f i) u - FlowNetwork.inflow (f i) u = 0 := by
        simpa [e] using hcons
      unfold FlowNetwork.ConservesAt
      linarith
    · intro i
      have hdemand := h.2 (demandIndex N commodity (Fintype.equivFin K i))
      rw [rel_demand] at hdemand
      rw [mulVec_demand, b_demand] at hdemand
      simpa using hdemand

The general-form objective is the aggregate minimum cost.


lemma objective_generalLP (N : FlowNetwork V) (commodity : K → Commodity V)
    (unitCost : V → V → ℝ) (f : K → V → V → ℝ) :
    (toGeneralLP N commodity unitCost).objective (lift₃ f) = cost unitCost f := by
  dsimp [GeneralLP.objective, toGeneralLP, cost, aggregate]
  simp only [dotProduct]
  rw [FinEncoding.sum_reindex]
  simp [lift₃, FinEncoding.lift]
  rw [Fintype.sum_prod_type]
  rw [Finset.sum_comm]
  rw [Fintype.sum_prod_type]
  simp [Finset.mul_sum]

The finite standard-form program obtained by normalizing the multicommodity general program.

noncomputable def toStandardLP (N : FlowNetwork V) (commodity : K → Commodity V)
    (unitCost : V → V → ℝ) :=
  (toGeneralLP N commodity unitCost).toStandardLP

The expansion of a commodity flow to the normalized standard-form variable vector.

noncomputable def fullLift (N : FlowNetwork V) (commodity : K → Commodity V)
    (unitCost : V → V → ℝ) (f : K → V → V → ℝ) :
    Fin (Fintype.card (K × (V × V)) + Fintype.card (K × (V × V))) → ℝ :=
  (toGeneralLP N commodity unitCost).lift (lift₃ f)

The normalized standard-form objective equals the signed aggregate cost.


theorem objective_toStandardLP (N : FlowNetwork V) (commodity : K → Commodity V)
    (unitCost : V → V → ℝ) (f : K → V → V → ℝ) :
    (toStandardLP N commodity unitCost).objective (fullLift N commodity unitCost f) = -cost unitCost f := by
  unfold toStandardLP fullLift
  rw [GeneralLP.objective_lift]
  rw [objective_generalLP]
  simp [toGeneralLP, GeneralLP.objectiveSign]

Feasibility is exactly preserved under the finite standard-form encoding.


theorem feasible_iff_toStandardLP (N : FlowNetwork V) (commodity : K → Commodity V)
    (f : K → V → V → ℝ) :
    IsFeasible N commodity f ↔ (toStandardLP N commodity (fun _ _ => 0)).IsFeasible (fullLift N commodity (fun _ _ => 0) f) := by
  unfold toStandardLP fullLift
  rw [← GeneralLP.feasible_iff_lift]
  exact feasible_iff_generalLP N commodity f

              end Encodingend MulticommodityFlowLPend Chapter29end CLRS