Theorem 1, proof — summing over players:
ProvedCongestionPoA.AsymSum.sum_cost_boundcongestion-gamenash-equilibriump2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1price-of-anarchy
Let be a congestion game with linear latencies , , let be a pure Nash equilibrium of , and let be any pure strategy profile. Then
The inequality sums the deviation inequality over all players; the equality regroups the double sum by facilities, each facility appearing once for each of the players that use it in . Lemma 1 then bounds the right-hand side, completing the proof of Theorem 1.
Formalization Note The paper writes this chain for the identity latency , as , and states that its proofs extend to general linear latencies; the statement here is that general case.
Preamble
import Mathlib import Definitions.Def_CongestionPoA_AsymSum_Model
Formal statement
namespace CongestionPoA.AsymSum
/-- Christodoulou and Koutsoupias, *The Price of Anarchy of Finite Congestion Games*, STOC 2005,
PDF p. 3, unnumbered step of the proof of Theorem 1 (summing over the players): at a pure Nash
equilibrium `A` of a linear congestion game, for any pure strategy profile `P`,
`SUM(A) = Σ_{i∈N} cᵢ(A) ≤ Σ_{i∈N} Σ_{e∈Pᵢ} f_e(n_e(A) + 1) = Σ_{e∈E} n_e(P) f_e(n_e(A) + 1)`.
**Formalization Note.** The paper prints this chain for the identity latency `f_e(k) = k`, as
`SUM(A) ≤ Σ_{i∈N} Σ_{e∈Pᵢ} (n_e(A) + 1) = Σ_{e∈E} n_e(P)(n_e(A) + 1)`, and says (Sect. 2, §1.1) that its
proofs extend to the general linear case `f_e(k) = a_e k + b_e`, `a_e, b_e ≥ 0`; the statement here is
that general case. -/
theorem sum_cost_bound {ι E : Type*} [Fintype ι] [DecidableEq ι] [Fintype E] [DecidableEq E]
(G : CongestionGame ι E) (A P : ι → Finset E)
(hlin : IsLinear G) (hA : IsPureNash G A) (hP : IsProfile G P) :
sumCost G A ≤ ∑ i, ∑ e ∈ P i, G.latency e (load A e + 1) ∧
∑ i, ∑ e ∈ P i, G.latency e (load A e + 1) =
∑ e, (load P e : ℝ) * G.latency e (load A e + 1) := by sorry
end CongestionPoA.AsymSum
Source
Christodoulou and Koutsoupias, The Price of Anarchy of Finite Congestion Games, STOC 2005, DOI 10.1145/1060590.1060600, PDF p. 3, Theorem 1, proof (sum over all players)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.