Lax Lean Archive

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

Individual cost in the network creation game

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

    For an edge price α>0\alpha>0, player ii has cost ci(s)=α∣si∣+∑jdG[s](i,j)c_i(s)=\alpha|s_i|+\sum_j d_{G[s]}(i,j). The distance is the length of a shortest path, and is infinite if there is no path. A player pays for every edge it purchases, including an edge also purchased by its other endpoint.

    Concept map
    2 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax899194.NetworkCreationGame
    2import Mathlib.Combinatorics.SimpleGraph.Metric
    3import Mathlib.Data.Real.ENatENNReal
    4import Mathlib.Algebra.BigOperators.Group.Finset.Defs
    5
    6/-!
    7---
    8title: Individual cost in the network creation game
    9type: definition
    10---
    11For an edge price α>0\alpha>0, player ii has cost
    12ci(s)=α∣si∣+∑jdG[s](i,j)c_i(s)=\alpha|s_i|+\sum_j d_{G[s]}(i,j).
    13The distance is the length of a shortest path, and is infinite if there is no
    14path. A player pays for every edge it purchases, including an edge also
    15purchased by its other endpoint.
    16
    17# Formalization notes
    18
    19Costs take values in the extended nonnegative reals so that disconnected
    20networks retain the infinite penalty. `SimpleGraph.edist` supplies the graph
    21distance, and `ENat.toENNReal` preserves both finite distances and infinity.
    22The edge price is a finite nonnegative real; the theorem assumes it is positive.
    23-/
    24
    25namespace Lax899194.PlayerCost
    26
    27open Lax899194.NetworkCreationGame
    28open scoped BigOperators NNReal ENNReal
    29
    30/-- Edge expenditure plus the sum of distances from player `i` to all players. -/
    31noncomputable def playerCost {n : ℕ} (α : ℝ≥0) (s : Profile n)
    32 (i : Fin n) : ℝ≥0∞ :=
    33 (α : ℝ≥0∞) * (s i).val.ncard +
    34 ∑ j : Fin n, ((graph s).edist i j).toENNReal
    35
    36end Lax899194.PlayerCost
    37
    Formalization notes

    Costs take values in the extended nonnegative reals so that disconnected networks retain the infinite penalty. SimpleGraph.edistSimpleGraph.edist supplies the graph distance, and ENat.toENNRealENat.toENNReal preserves both finite distances and infinity. The edge price is a finite nonnegative real; the theorem assumes it is positive.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…