Lax Lean Archive

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

Uniform endpoint normalization of finite path flows

Lax263307.RoutingNormalization · concepts/Lax263307/RoutingNormalization.lean · lax-263307

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

    Theorem

    Normalize each of the n2n^2 ordered endpoint commodities to mass 1/n21/n^2. If every commodity has routed mass at least 1/γ1/\gamma, normalization increases any nonnegative load by at most γ/n2\gamma/n^2. Each flow record belongs to at most one endpoint pair, so records are counted only once. The statement includes diagonal commodities and applies to vertex loads that count both route endpoints.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 normalization_correct proven

    2 normalized_load_bound proven

    Lean source view on GitHub

    1import Lax263307.PathSampling
    2
    3/-!
    4---
    5title: Uniform endpoint normalization of finite path flows
    6type: theorem
    7---
    8Normalize each of the n2n^2 ordered endpoint commodities to mass 1/n21/n^2.
    9If every commodity has routed mass at least 1/γ1/\gamma, normalization
    10increases any nonnegative load by at most γ/n2\gamma/n^2. Each flow record
    11belongs to at most one endpoint pair, so records are counted only once.
    12The statement includes diagonal commodities and applies to vertex loads
    13that count both route endpoints.
    14
    15# Attribution
    16
    17Bonnet–Chang, normalization and vertex-load accounting in Lemma 7.
    18-/
    19
    20namespace Lax263307.RoutingNormalization
    21
    22def IsUniquePair {n q : ℕ} (E : Fin n → Fin n → Fin q → Prop) : Prop :=
    23 ∀ i u v u' v', E u v i → E u' v' i → u = u' ∧ v = v'
    24
    25noncomputable def routed {n q : ℕ} (w : Fin q → ℝ)
    26 (E : Fin n → Fin n → Fin q → Prop) (u v : Fin n) : ℝ := by
    27 classical
    28 exact ∑ i, if E u v i then w i else 0
    29
    30noncomputable def probability {n q : ℕ} (w : Fin q → ℝ)
    31 (E : Fin n → Fin n → Fin q → Prop) (u v : Fin n) (i : Fin q) : ℝ := by
    32 classical
    33 exact if E u v i then w i / (routed w E u v * (n : ℝ) ^ 2) else 0
    34
    35/-- Nonnegative normalized probabilities with uniform ordered endpoints. -/
    36axiom normalization_correct {n q : ℕ} (w : Fin q → ℝ)
    37 (E : Fin n → Fin n → Fin q → Prop) (hn : 0 < n)
    38 (nonnegative : ∀ i, 0 ≤ w i) (positive : ∀ u v, 0 < routed w E u v) :
    39 (∀ u v i, 0 ≤ probability w E u v i) ∧
    40 (∀ u v, (∑ i, probability w E u v i) = 1 / (n : ℝ) ^ 2) ∧
    41 (∑ u, ∑ v, ∑ i, probability w E u v i) = 1
    42
    43/-- Uniform commodity normalization preserves the scaled load bound. -/
    44axiom normalized_load_bound {n q : ℕ} (w : Fin q → ℝ)
    45 (E : Fin n → Fin n → Fin q → Prop) (hn : 0 < n)
    46 (nonnegative : ∀ i, 0 ≤ w i) (unique : IsUniquePair E)
    47 (γ : ℝ) (γ_positive : 0 < γ) (lower_bound : ∀ u v, 1 / γ ≤ routed w E u v)
    48 (cost : Fin q → ℝ) (cost_nonnegative : ∀ i, 0 ≤ cost i) :
    49 (∑ u, ∑ v, ∑ i, probability w E u v i * cost i) ≤
    50 γ / (n : ℝ) ^ 2 * (∑ i, w i * cost i)
    51
    52end Lax263307.RoutingNormalization
    53
    Show ProofShow Proof

    Attribution

    Bonnet–Chang, normalization and vertex-load accounting in Lemma 7.

    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…