is_dominant_strategy_incentive_compatible

def

For a direct mechanism (M : DirectMechanism Player Theta Outcome) with {Player : Type*} [DecidableEq Player], {Theta : Player → Type*}, {Outcome : Type*}, and valuation profile (v : (i : Player) → Theta i → Outcome → ℝ), is_dominant_strategy_incentive_compatible M v is defined with body := ∀ (i : Player) (θ : ∀ j, Theta j) (θ_i' : Theta i), v i (θ i) (M.allocation (Function.update θ i θ_i')) - M.payment i (Function.update θ i θ_i') ≤ v i (θ i) (M.allocation θ) - M.payment i θ.

Statement

def is_dominant_strategy_incentive_compatible
    {Player : Type*} [DecidableEq Player] {Theta : Player → Type*} {Outcome : Type*}
    (M : DirectMechanism Player Theta Outcome)
    (v : (i : Player) → Theta i → Outcome → ℝ) : Prop

Source

Borgers, Definition 2.1

Verified

07 Sep 2026

Axioms

none listed

Built on 1

DirectMechanismA direct mechanism with player type Player, type spaces Theta i for each player i : Player, and outcome type Outcome, consists of an…

Read back from the Lean

Given a type Player with decidable equality, a type family Theta : Player → Type* of types for each player, an outcome type Outcome, a direct mechanism M (consisting of an allocation function M.allocation : (∀ j, Theta j) → Outcome and a payment function M.payment : Player → (∀ j, Theta j) → ℝ), and a valuation function v : (i : Player) → Theta i → Outcome → ℝ, is_dominant_strategy_incentive_compatible M v is the proposition that: For every player i : Player, every type profile θ : ∀ j, Theta j, and every alternative type θ_i' : Theta i for player i: The valuation v i (θ i) of the outcome allocated when player i reports θ_i' (and all other players report according to θ), minus the payment charged to player i under that updated profile, is less than or equal to the valuation v i (θ i) of the outcome allocated when all players report according to θ, minus the payment charged to player i under θ.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- Dominant-strategy incentive compatibility (strategy-proofness) for a direct mechanism. -/
def is_dominant_strategy_incentive_compatible
    {Player : Type*} [DecidableEq Player] {Theta : Player → Type*} {Outcome : Type*}
    (M : DirectMechanism Player Theta Outcome)
    (v : (i : Player) → Theta i → Outcome → ℝ) : Prop := ∀ (i : Player) (θ : ∀ j, Theta j) (θ_i' : Theta i),
    v i (θ i) (M.allocation (Function.update θ i θ_i')) - M.payment i (Function.update θ i θ_i') ≤
    v i (θ i) (M.allocation θ) - M.payment i θ

Discuss this result Challenge it