Lax Lean Archive

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

Network creation game

Lax899194.NetworkCreationGame · concepts/Lax899194/NetworkCreationGame.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

    There are nn players, indexed by {0,…,n−1}\{0,\ldots,n-1\}. A strategy of player ii is a set sis_i of other players: player ii purchases an edge to each member of sis_i. A strategy profile specifies one strategy for every player.

    The resulting network G[s]G[s] is undirected. Distinct players ii and jj are adjacent when j∈sij\in s_i or i∈sji\in s_j. Either endpoint may purchase an edge, and both endpoints may purchase the same edge.

    Concept map
    1 concept; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2import Mathlib.Data.Set.Card
    3
    4/-!
    5---
    6title: Network creation game
    7type: definition
    8---
    9There are nn players, indexed by {0,…,n−1}\{0,\ldots,n-1\}. A strategy of player
    10ii is a set sis_i of other players: player ii purchases an edge to each member
    11of sis_i. A strategy profile specifies one strategy for every player.
    12
    13The resulting network G[s]G[s] is undirected. Distinct players ii and jj are
    14adjacent when j∈sij\in s_i or i∈sji\in s_j. Either endpoint may purchase an edge,
    15and both endpoints may purchase the same edge.
    16
    17# Formalization notes
    18
    19Strategies are subsets of `Fin n`, with self-purchases excluded by their type.
    20Every such subset is finite. Edge ownership remains part of the profile even
    21though the resulting graph is a simple graph.
    22-/
    23
    24namespace Lax899194.NetworkCreationGame
    25
    26/-- The other players to which player `i` purchases edges. -/
    27def Strategy (n : ℕ) (i : Fin n) := { S : Set (Fin n) // i ∉ S }
    28
    29/-- A choice of strategy for every player. -/
    30abbrev Profile (n : ℕ) := (i : Fin n) → Strategy n i
    31
    32/-- The undirected network formed by all purchased edges. -/
    33def graph {n : ℕ} (s : Profile n) : SimpleGraph (Fin n) where
    34 Adj i j := j ∈ (s i).val ∨ i ∈ (s j).val
    35 symm := ⟨fun _ _ h => h.elim Or.inr Or.inl⟩
    36 loopless := ⟨fun i h => h.elim (s i).property (s i).property⟩
    37
    38end Lax899194.NetworkCreationGame
    39
    Formalization notes

    Strategies are subsets of FinnFin n, with self-purchases excluded by their type. Every such subset is finite. Edge ownership remains part of the profile even though the resulting graph is a simple graph.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…