Lax Lean Archive

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

Social cost

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

    The social cost of a strategy profile is the sum of all players' individual costs: C(s)=∑ici(s)C(s)=\sum_i c_i(s). Distances are counted over ordered pairs of players. An edge purchased by both endpoints is charged twice.

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

    Lean source view on GitHub

    1import Lax899194.PlayerCost
    2
    3/-!
    4---
    5title: Social cost
    6type: definition
    7---
    8The social cost of a strategy profile is the sum of all players' individual
    9costs: C(s)=∑ici(s)C(s)=\sum_i c_i(s). Distances are counted over ordered pairs of
    10players. An edge purchased by both endpoints is charged twice.
    11
    12# Formalization notes
    13
    14Social cost is defined on profiles so that it accounts for who purchases each
    15edge. The graph alone does not determine the expenditure when both endpoints
    16purchase an edge. No absence of double purchases is assumed in this definition.
    17-/
    18
    19namespace Lax899194.SocialCost
    20
    21open Lax899194.NetworkCreationGame Lax899194.PlayerCost
    22open scoped BigOperators NNReal ENNReal
    23
    24/-- The sum of all players' individual costs, with distances counted in both directions. -/
    25noncomputable def socialCost {n : ℕ} (α : ℝ≥0) (s : Profile n) : ℝ≥0∞ :=
    26 ∑ i : Fin n, playerCost α s i
    27
    28end Lax899194.SocialCost
    29
    Formalization notes

    Social cost is defined on profiles so that it accounts for who purchases each edge. The graph alone does not determine the expenditure when both endpoints purchase an edge. No absence of double purchases is assumed in this definition.

    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…