Lax Lean Archive

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

Tree Nash equilibria have inefficiency below five

Lax899194.TreeNashEfficiency · concepts/Lax899194/TreeNashEfficiency.lean · lax-899194

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

    For every positive edge price α\alpha and every tree Nash equilibrium TT, ρ(T)<5\rho(T)<5: its social cost is strictly less than five times the social optimum.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax899194.NashEquilibrium
    2import Lax899194.InefficiencyRatio
    3import Mathlib.Combinatorics.SimpleGraph.Acyclic
    4
    5/-!
    6---
    7title: Tree Nash equilibria have inefficiency below five
    8type: theorem
    9---
    10For every positive edge price α\alpha and every tree Nash equilibrium TT,
    11ρ(T)<5\rho(T)<5: its social cost is strictly less than five times the social
    12optimum.
    13
    14# Formalization notes
    15
    16There are at least two players, making the cost ratio well-defined with a
    17positive denominator. `SimpleGraph.IsTree` means connected and acyclic.
    18The equilibrium is a strategy profile whose resulting undirected network is
    19a tree; the profile retains edge ownership and the costs of deviations.
    20No non-transience assumption or lower bound such as α≥2\alpha\ge2 is imposed.
    21
    22# Reference
    23
    24Theorem 3, p. 350, in Fabrikant, Luthra, Maneva, Papadimitriou, and Shenker,
    25[*On a Network Creation Game*](https://people.eecs.berkeley.edu/~kubitron/courses/cs294-4-F03/papers/p347-fabrikant.pdf),
    26PODC 2003, pp. 347-351, DOI: 10.1145/872035.872088.
    27-/
    28
    29namespace Lax899194.TreeNashEfficiency
    30
    31open Lax899194.NetworkCreationGame Lax899194.NashEquilibrium
    32open Lax899194.InefficiencyRatio
    33open scoped NNReal
    34
    35/-- Theorem 3: every tree Nash equilibrium has inefficiency strictly below five. -/
    36axiom statement (n : ℕ) (hn : 2 ≤ n) (α : ℝ≥0) (hα : 0 < α)
    37 (s : Profile n) (hNash : IsNashEquilibrium α s) (hTree : (graph s).IsTree) :
    38 inefficiencyRatio α s < 5
    39
    40end Lax899194.TreeNashEfficiency
    41
    Show Proof
    Formalization notes

    There are at least two players, making the cost ratio well-defined with a positive denominator. SimpleGraph.IsTreeSimpleGraph.IsTree means connected and acyclic. The equilibrium is a strategy profile whose resulting undirected network is a tree; the profile retains edge ownership and the costs of deviations. No non-transience assumption or lower bound such as α≥2\alpha\ge2 is imposed.

    Reference

    Theorem 3, p. 350, in Fabrikant, Luthra, Maneva, Papadimitriou, and Shenker, On a Network Creation Game, PODC 2003, pp. 347-351, DOI: 10.1145/872035.872088.

    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…