Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Bipartite capacity networks

Lax342547.BipartiteFlows · concepts/Lax342547/BipartiteFlows.lean · lax-342547

proven

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

    Lemma

    Real flows encode probability laws with two marginal caps and a pointwise pair cap; infeasibility yields a cut of capacity less than one.

    Concept map
    4 concepts; 10 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.

    1 capacity_nonneg proven

    2 forward_flow_nonneg proven

    3 infeasible_cut proven

    4 left_conservation proven

    5 normalized_flow_law proven

    6 right_conservation proven

    7 source_flow_total proven

    8 zero_capacity_flow proven

    Lean source view on GitHub

    1import Lax342547.FlowCuts
    2import Mathlib.Algebra.BigOperators.Field
    3
    4/-!
    5---
    6title: Bipartite capacity networks
    7type: lemma
    8---
    9Real flows encode probability laws with two marginal caps and a pointwise pair cap; infeasibility yields a cut of capacity less than one.
    10-/
    11
    12namespace Lax342547.BipartiteFlows
    13
    14open Lax342547.RealFlows
    15open scoped BigOperators
    16
    17abbrev Vertex (A B : Type) := Bool ⊕ (A ⊕ B)
    18
    19def source {A B : Type} : Vertex A B := .inl false
    20def sink {A B : Type} : Vertex A B := .inl true
    21def left {A B : Type} (a : A) : Vertex A B := .inr (.inl a)
    22def right {A B : Type} (b : B) : Vertex A B := .inr (.inr b)
    23
    24noncomputable def capacity {A B : Type} (a : A → ℝ) (b : B → ℝ) (p : A → B → ℝ) :
    25 Vertex A B → Vertex A B → ℝ
    26 | .inl false, .inr (.inl x) => a x
    27 | .inr (.inl x), .inr (.inr y) => p x y
    28 | .inr (.inr y), .inl true => b y
    29 | _, _ => 0
    30
    31axiom capacity_nonneg {A B : Type} (a : A → ℝ) (b : B → ℝ) (p : A → B → ℝ)
    32 (ha : ∀ x, 0 ≤ a x) (hb : ∀ y, 0 ≤ b y) (hp : ∀ x y, 0 ≤ p x y) :
    33 ∀ u v, 0 ≤ capacity a b p u v
    34
    35axiom zero_capacity_flow {V : Type} [Fintype V] (c f : V → V → ℝ) (s t u v : V)
    36 (hf : Feasible c f s t) (huv : c u v = 0) (hvu : c v u = 0) : f u v = 0
    37
    38axiom forward_flow_nonneg {A B : Type} [Fintype A] [Fintype B]
    39 (a : A → ℝ) (b : B → ℝ) (p : A → B → ℝ) (f : Vertex A B → Vertex A B → ℝ)
    40 (hf : Feasible (capacity a b p) f source sink) (x : A) (y : B) : 0 ≤ f (left x) (right y)
    41
    42axiom left_conservation {A B : Type} [Fintype A] [Fintype B]
    43 (a : A → ℝ) (b : B → ℝ) (p : A → B → ℝ) (f : Vertex A B → Vertex A B → ℝ)
    44 (hf : Feasible (capacity a b p) f source sink) (x : A) :
    45 (∑ y, f (left x) (right y)) = f source (left x)
    46
    47axiom right_conservation {A B : Type} [Fintype A] [Fintype B]
    48 (a : A → ℝ) (b : B → ℝ) (p : A → B → ℝ) (f : Vertex A B → Vertex A B → ℝ)
    49 (hf : Feasible (capacity a b p) f source sink) (y : B) :
    50 (∑ x, f (left x) (right y)) = f (right y) sink
    51
    52axiom source_flow_total {A B : Type} [Fintype A] [Fintype B]
    53 (a : A → ℝ) (b : B → ℝ) (p : A → B → ℝ) (f : Vertex A B → Vertex A B → ℝ)
    54 (hf : Feasible (capacity a b p) f source sink) :
    55 divergence f source = ∑ x, ∑ y, f (left x) (right y)
    56
    57def Law {A B : Type} [Fintype A] [Fintype B]
    58 (a : A → ℝ) (b : B → ℝ) (p ρ : A → B → ℝ) : Prop :=
    59 (∀ x y, 0 ≤ ρ x y) ∧ (∑ x, ∑ y, ρ x y) = 1 ∧
    60 (∀ x, (∑ y, ρ x y) ≤ a x) ∧ (∀ y, (∑ x, ρ x y) ≤ b y) ∧ (∀ x y, ρ x y ≤ p x y)
    61
    62axiom normalized_flow_law {A B : Type} [Fintype A] [Fintype B]
    63 (a : A → ℝ) (b : B → ℝ) (p : A → B → ℝ) (f : Vertex A B → Vertex A B → ℝ)
    64 (hf : Feasible (capacity a b p) f source sink)
    65 (ha : ∀ x, 0 ≤ a x) (hb : ∀ y, 0 ≤ b y) (hp : ∀ x y, 0 ≤ p x y)
    66 (hv : 1 ≤ divergence f source) : ∃ ρ, Law a b p ρ
    67
    68axiom infeasible_cut {A B : Type} [Fintype A] [Fintype B]
    69 (a : A → ℝ) (b : B → ℝ) (p : A → B → ℝ)
    70 (ha : ∀ x, 0 ≤ a x) (hb : ∀ y, 0 ≤ b y) (hp : ∀ x y, 0 ≤ p x y)
    71 (hn : ¬ ∃ ρ, Law a b p ρ) :
    72 ∃ Z : Finset (Vertex A B), source ∈ Z ∧ sink ∉ Z ∧
    73 Lax342547.FlowCuts.cutCapacity (capacity a b p) Z < 1
    74
    75end Lax342547.BipartiteFlows
    76
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    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…