Lax Lean Archive

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

Pure Nash equilibrium

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

definition

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

    Definition

    A strategy profile is a pure Nash equilibrium when no player can reduce its individual cost by changing its own strategy while all other players keep their strategies. A deviation may replace the entire set of purchased edges.

    Concept map
    3 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax899194.PlayerCost
    2
    3/-!
    4---
    5title: Pure Nash equilibrium
    6type: definition
    7---
    8A strategy profile is a pure Nash equilibrium when no player can reduce its
    9individual cost by changing its own strategy while all other players keep
    10their strategies. A deviation may replace the entire set of purchased edges.
    11
    12# Formalization notes
    13
    14The comparison is between costs in the two resulting networks, including
    15deviations that disconnect the network. Equality is allowed, so weak and
    16transient equilibria are included.
    17
    18The displayed equilibrium inequality on p. 348 of the paper has its direction
    19reversed. We use cost minimization, as specified by the surrounding discussion
    20and explicitly by footnote 4 on p. 350: the current cost is at most the cost
    21after any unilateral deviation.
    22-/
    23
    24namespace Lax899194.NashEquilibrium
    25
    26open Lax899194.NetworkCreationGame Lax899194.PlayerCost
    27open scoped NNReal
    28
    29/-- No unilateral replacement of a player's strategy lowers that player's cost. -/
    30def IsNashEquilibrium {n : ℕ} (α : ℝ≥0) (s : Profile n) : Prop :=
    31 ∀ (i : Fin n) (t : Profile n),
    32 (∀ j : Fin n, j ≠ i → t j = s j) →
    33 playerCost α s i ≤ playerCost α t i
    34
    35end Lax899194.NashEquilibrium
    36
    Formalization notes

    The comparison is between costs in the two resulting networks, including deviations that disconnect the network. Equality is allowed, so weak and transient equilibria are included.

    The displayed equilibrium inequality on p. 348 of the paper has its direction reversed. We use cost minimization, as specified by the surrounding discussion and explicitly by footnote 4 on p. 350: the current cost is at most the cost after any unilateral deviation.

    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…