DirectMechanism
structure
A direct mechanism with player type Player, type spaces Theta i for each player i : Player, and outcome type Outcome, consists of an allocation rule allocation : (∀ i : Player, Theta i) → Outcome and a payment rule payment : Player → (∀ i : Player, Theta i) → ℝ.
Statement
structure DirectMechanism (Player : Type*) (Theta : Player → Type*) (Outcome : Type*)
- Source
- Borgers, An Introduction to the Theory of Mechanism Design, Section 2.1
- Verified
- 07 Sep 2026
- Axioms
- none listed
- Used by 1
- is_dominant_strategy_incentive_compatibleFor a direct mechanism (M : DirectMechanism Player Theta Outcome) with {Player : Type*} [DecidableEq Player], {Theta : Player → Type*},…
Read back from the Lean
A structure DirectMechanism parameterized by types Player : Type*, Theta : Player → Type*, and Outcome : Type*. It consists of two fields:
1. allocation: a function from type profiles (∀ i : Player, Theta i) to Outcome.
2. payment: a function that takes a player i : Player and a type profile (∀ i : Player, Theta i) and returns a real number in ℝ.
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
/-- A direct mechanism consists of an allocation rule and a profile of payment rules for each player. -/ structure DirectMechanism (Player : Type*) (Theta : Player → Type*) (Outcome : Type*) where allocation : (∀ i, Theta i) → Outcome payment : Player → (∀ i, Theta i) → ℝ