Lax Lean Archive

Concurrent flow on short paths

Lax455465.ShortPathFlow · concepts/Lax455465/ShortPathFlow.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

    The length of a path is its number of edges. A fractional flow has path length at most LL if every path carrying positive flow has at most LL edges. For an undirected network, Cmax⁡C_{\max} is the largest total capacity incident to a single vertex.

    Concept map
    3 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax455465.ConcurrentFlow
    2
    3/-!
    4---
    5title: Concurrent flow on short paths
    6type: definition
    7---
    8The length of a path is its number of edges. A fractional flow has path
    9length at most LL if every path carrying positive flow has at most LL
    10edges. For an undirected network, Cmax⁡C_{\max} is the largest total capacity
    11incident to a single vertex.
    12
    13# Formalization notes
    14
    15Path lengths are integers, compared with a real bound. Only the support
    16of the fractional flow matters. Incident capacity sums the capacity matrix
    17along one row, counting each edge incident to the vertex once.
    18-/
    19
    20open scoped BigOperators NNReal
    21
    22namespace Lax455465.ShortPathFlow
    23
    24open Lax455465.ProductNetwork Lax455465.ConcurrentFlow
    25
    26/-- Every path carrying flow has at most `L` edges. -/
    27def HasPathLengthAtMost {n : ℕ} (F : PathFlow n) (L : ℝ) : Prop :=
    28 ∀ P ∈ F.support, ((P.length - 1 : ℕ) : ℝ) ≤ L
    29
    30/-- The largest total capacity incident to one vertex. -/
    31noncomputable def maxIncidentCapacity {n : ℕ} (N : Network n) : ℝ≥0 :=
    32 sSup {r | ∃ v : Fin n, (∑ u : Fin n, N.capacity v u) = r}
    33
    34end Lax455465.ShortPathFlow
    35
    Formalization notes

    Path lengths are integers, compared with a real bound. Only the support of the fractional flow matters. Incident capacity sums the capacity matrix along one row, counting each edge incident to the vertex once.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…