Theorem 1 — BWE are exactly the minimizers of the weighted potential; the equilibrium edge load is unique

Proved

BayesRouting.Adoption.bwe_iff_optimal

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-optimizationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1potential-gamerouting-game

Let $\Gamma(\lambda)$ be the Bayesian routing game (standing assumptions as in the game definition, including positive probability of every type profile), and let $\lambda$ satisfy $\lambda^i\ge0$ , $\sum_i\lambda^i=1$ .

A strategy profile $q$ is a Bayesian Wardrop equilibrium of $\Gamma(\lambda)$ if and only if it is an optimal solution of $\min\ \Phi(q)\quad\text{s.t.}\quad q\in\mathcal Q(\lambda).\tag{OPT-$\mathcal Q$}$
Any two Bayesian Wardrop equilibria of $\Gamma(\lambda)$ induce the same edge load $w^*(\lambda)=(w_e(t))_{e,t}$ .

This characterization is the basis of the whole analysis: it turns equilibrium questions into questions about a convex program and its optimal value $\Psi(\lambda)$ , and the uniqueness of the load makes the equilibrium population costs independent of the equilibrium chosen.

Formalization Note The uniqueness claim uses the added assumption that every type profile has positive probability.

Preamble

import Mathlib
import Definitions.Def_BayesRouting_Adoption_Game
import Definitions.Def_BayesRouting_Adoption_Potential

open Finset

Formal statement

namespace BayesRouting.Adoption

/-- Theorem 1 (p. 154). For `λ` in the simplex, a strategy profile is a BWE of `Γ(λ)` if and only
if it minimizes the weighted potential `Φ` over the feasible set `𝒬(λ)` (problem (OPT-𝒬)); and
any two BWE of `Γ(λ)` induce the same edge load `w*(λ)`. -/
theorem bwe_iff_optimal {I : Type} [Fintype I] [DecidableEq I] {T : I → Type} [∀ i, Fintype (T i)]
    [∀ i, DecidableEq (T i)] [∀ i, Nonempty (T i)] {S E R : Type} [Fintype S] [Fintype E]
    [DecidableEq E] [Fintype R] [Nonempty R]
    (G : Game I T S E R) (lam : I → ℝ) (hlam : lam ∈ stdSimplex ℝ I) :
    (∀ q, IsBWE G lam q ↔
      (q ∈ feasibleStrategies G lam ∧
        ∀ q' ∈ feasibleStrategies G lam, potential G q ≤ potential G q')) ∧
    (∀ q q', IsBWE G lam q → IsBWE G lam q' → edgeLoad G q = edgeLoad G q') := by sorry

end BayesRouting.Adoption

Source

Wu, Amin, Ozdaglar, Value of Information in Bayesian Routing Games, Oper. Res. 69(1) 2021, p. 154, Theorem 1

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph