Lax Lean Archive

Concurrent fractional flow

Lax455465.ConcurrentFlow · concepts/Lax455465/ConcurrentFlow.lean · lax-455465

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A fractional flow can be represented by nonnegative commodity/arc amounts or by nonnegative amounts on finitely many simple paths. It is feasible when the total load on every edge is at most its capacity. Undirected edges carry the sum of the loads in both directions; directed arcs carry only forward load. A concurrent flow of value ff meets ff times every commodity's demand simultaneously. The maximum concurrent flow is the supremum of feasible values.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax455465.ProductNetwork
    2import Mathlib.Data.Finsupp.Defs
    3import Mathlib.Data.List.Count
    4
    5/-!
    6---
    7title: Concurrent fractional flow
    8type: definition
    9---
    10A fractional flow can be represented by nonnegative commodity/arc amounts
    11or by nonnegative amounts on finitely many simple paths.
    12It is feasible when the total load on every edge is at most its capacity.
    13Undirected edges carry the sum of the loads in both directions; directed arcs
    14carry only forward load. A concurrent flow of value ff meets ff times
    15every commodity's demand simultaneously. The maximum concurrent flow is the
    16supremum of feasible values.
    17
    18# Formalization notes
    19
    20The ordinary algorithm uses arc amounts with exact supply and conservation,
    21so its certificate has polynomially many coordinates. The short-path
    22algorithm uses explicit path records to certify the lengths.
    23
    24A path is its ordered vertex list. Positive flow is supported only on lists
    25with at least two vertices and no repeated vertex. Its commodity is determined
    26by its endpoints, rather than stored separately. Requiring at least the stated
    27demand allows excess flow; deleting excess gives the usual equality formulation.
    28Cycles are unnecessary for fractional routing and can be deleted.
    29
    30For undirected product demand, each ordered pair receives fπ(u)π(v)/2f\pi(u)\pi(v)/2;
    31for directed product demand it receives fπ(u)π(v)f\pi(u)\pi(v). Only distinct
    32endpoints impose demands. An absent edge has zero capacity, so feasibility
    33prevents a positive-flow path from using it. There are finitely many simple
    34paths on `Fin n`; with at least two positive-weight vertices, feasible values
    35form a nonempty bounded set and the supremum is attained.
    36-/
    37
    38open scoped BigOperators NNReal
    39
    40namespace Lax455465.ConcurrentFlow
    41
    42open Lax455465.ProductNetwork
    43
    44/-- A finite assignment of nonnegative flow amounts to vertex lists. -/
    45abbrev PathFlow (n : ℕ) := List (Fin n) →₀ ℝ≥0
    46
    47/-- Every path carrying positive flow is simple and has distinct endpoints. -/
    48def IsPathFlow {n : ℕ} (F : PathFlow n) : Prop :=
    49 ∀ P ∈ F.support, 2 ≤ P.length ∧ P.Nodup
    50
    51/-- The forward load on an arc, counting its occurrences on each path. -/
    52noncomputable def arcLoad {n : ℕ} (F : PathFlow n) (u v : Fin n) : ℝ≥0 :=
    53 ∑ P ∈ F.support, F P * ((P.zip P.tail).count (u, v) : ℝ≥0)
    54
    55/-- The capacity consumed by a path flow in the chosen edge model. -/
    56noncomputable def edgeLoad {n : ℕ} (kind : EdgeKind) (F : PathFlow n)
    57 (u v : Fin n) : ℝ≥0 :=
    58 match kind with
    59 | .undirected => arcLoad F u v + arcLoad F v u
    60 | .directed => arcLoad F u v
    61
    62/-- The amount routed from one endpoint to another. -/
    63noncomputable def routed {n : ℕ} (F : PathFlow n) (s t : Fin n) : ℝ≥0 :=
    64 ∑ P ∈ F.support,
    65 if P.head? = some s ∧ P.getLast? = some t then F P else 0
    66
    67/-- The demand assigned to an ordered pair of distinct endpoints. -/
    68noncomputable def pairDemand {n : ℕ} (kind : EdgeKind) (π : VertexWeight n)
    69 (s t : Fin n) : ℝ≥0 :=
    70 match kind with
    71 | .undirected => π s * π t / 2
    72 | .directed => π s * π t
    73
    74/-- A simple-path flow respects capacities and meets the specified common
    75fraction of every demand. -/
    76def IsConcurrentFlow {n : ℕ} (kind : EdgeKind) (N : Network n)
    77 (π : VertexWeight n) (f : ℝ≥0) (F : PathFlow n) : Prop :=
    78 IsPathFlow F ∧
    79 (∀ u v, edgeLoad kind F u v ≤ N.capacity u v) ∧
    80 ∀ s t, s ≠ t → f * pairDemand kind π s t ≤ routed F s t
    81
    82/-- The largest feasible concurrent-flow value, expressed as a supremum. -/
    83noncomputable def maxFlow {n : ℕ} (kind : EdgeKind) (N : Network n)
    84 (π : VertexWeight n) : ℝ≥0 :=
    85 sSup {f | ∃ F : PathFlow n, IsConcurrentFlow kind N π f F}
    86
    87/-- An arc flow records a nonnegative amount for each commodity and arc. -/
    88abbrev ArcFlow (n : ℕ) := Fin n → Fin n → Fin n → Fin n → ℝ≥0
    89
    90/-- Aggregate forward capacity consumption in the edge formulation. -/
    91def totalArcLoad {n : ℕ} (F : ArcFlow n) (u v : Fin n) : ℝ≥0 :=
    92 ∑ s, ∑ t, F s t u v
    93
    94/-- Shared or separate capacities in the edge formulation. -/
    95def totalEdgeLoad {n : ℕ} (kind : EdgeKind) (F : ArcFlow n) (u v : Fin n) : ℝ≥0 :=
    96 match kind with
    97 | .undirected => totalArcLoad F u v + totalArcLoad F v u
    98 | .directed => totalArcLoad F u v
    99
    100/-- Net required supply at a vertex for one commodity; diagonal commodities
    101have zero supply at every vertex. -/
    102noncomputable def requiredSupply {n : ℕ} (kind : EdgeKind) (π : VertexWeight n)
    103 (f : ℝ≥0) (s t u : Fin n) : ℝ :=
    104 if s = t then 0 else
    105 (if u = s then (f * pairDemand kind π s t : ℝ≥0) else 0) -
    106 (if u = t then (f * pairDemand kind π s t : ℝ≥0) else 0)
    107
    108/-- Capacity and exact commodity conservation in the polynomial-size arc formulation. -/
    109def IsArcConcurrentFlow {n : ℕ} (kind : EdgeKind) (N : Network n)
    110 (π : VertexWeight n) (f : ℝ≥0) (F : ArcFlow n) : Prop :=
    111 (∀ u v, totalEdgeLoad kind F u v ≤ N.capacity u v) ∧
    112 ∀ s t u, (∑ v, (F s t u v : ℝ)) - (∑ v, (F s t v u : ℝ)) =
    113 requiredSupply kind π f s t u
    114
    115end Lax455465.ConcurrentFlow
    116
    Formalization notes

    The ordinary algorithm uses arc amounts with exact supply and conservation, so its certificate has polynomially many coordinates. The short-path algorithm uses explicit path records to certify the lengths.

    A path is its ordered vertex list. Positive flow is supported only on lists with at least two vertices and no repeated vertex. Its commodity is determined by its endpoints, rather than stored separately. Requiring at least the stated demand allows excess flow; deleting excess gives the usual equality formulation. Cycles are unnecessary for fractional routing and can be deleted.

    For undirected product demand, each ordered pair receives fπ(u)π(v)/2f\pi(u)\pi(v)/2; for directed product demand it receives fπ(u)π(v)f\pi(u)\pi(v). Only distinct endpoints impose demands. An absent edge has zero capacity, so feasibility prevents a positive-flow path from using it. There are finitely many simple paths on FinnFin n; with at least two positive-weight vertices, feasible values form a nonempty bounded set and the supremum is attained.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…