Lax Lean Archive

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

Inefficiency relative to the social optimum

Lax899194.InefficiencyRatio · concepts/Lax899194/InefficiencyRatio.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 fixed nn and edge price α\alpha, the social optimum is the minimum social cost over all strategy profiles. The inefficiency of a profile is ρ(s)=C(s)/OPT⁡(n,α)\rho(s)=C(s)/\operatorname{OPT}(n,\alpha).

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

    Lean source view on GitHub

    1import Lax899194.SocialCost
    2
    3/-!
    4---
    5title: Inefficiency relative to the social optimum
    6type: definition
    7---
    8For fixed nn and edge price α\alpha, the social optimum is the minimum
    9social cost over all strategy profiles. The inefficiency of a profile is
    10ρ(s)=C(s)/OPT⁡(n,α)\rho(s)=C(s)/\operatorname{OPT}(n,\alpha).
    11
    12# Formalization notes
    13
    14The optimum is encoded as an infimum. There are finitely many profiles and
    15the set of profiles is nonempty. For n≥2n\ge2, a connected profile exists and
    16every profile has social cost at least n(n−1)>0n(n-1)>0. Thus the infimum is an
    17attained finite minimum with a positive denominator in the theorem's domain.
    18
    19The optimum ranges over all profiles, including networks with cycles. This
    20uses the actual social optimum for every edge price rather than prescribing
    21a star. The paper uses ρ(G)\rho(G) for the ratio of an individual equilibrium;
    22the worst ratio over all equilibria is the price of anarchy.
    23-/
    24
    25namespace Lax899194.InefficiencyRatio
    26
    27open Lax899194.NetworkCreationGame Lax899194.SocialCost
    28open scoped NNReal ENNReal
    29
    30/-- The least social cost among all strategy profiles with `n` players. -/
    31noncomputable def optimalCost (n : ℕ) (α : ℝ≥0) : ℝ≥0∞ :=
    32 ⨅ s : Profile n, socialCost α s
    33
    34/-- The social cost of a profile divided by the social optimum for the same game. -/
    35noncomputable def inefficiencyRatio {n : ℕ} (α : ℝ≥0) (s : Profile n) : ℝ≥0∞ :=
    36 socialCost α s / optimalCost n α
    37
    38end Lax899194.InefficiencyRatio
    39
    Formalization notes

    The optimum is encoded as an infimum. There are finitely many profiles and the set of profiles is nonempty. For n≥2n\ge2, a connected profile exists and every profile has social cost at least n(n−1)>0n(n-1)>0. Thus the infimum is an attained finite minimum with a positive denominator in the theorem's domain.

    The optimum ranges over all profiles, including networks with cycles. This uses the actual social optimum for every edge price rather than prescribing a star. The paper uses ρ(G)\rho(G) for the ratio of an individual equilibrium; the worst ratio over all equilibria is the price of anarchy.

    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…