EconCSLib.MechanismDesign.Auction.Transfer

Mechanisms with monetary transfers.

Design

This file separates the roles that were previously collapsed into one scalar type:

• T i — report/type space for agent i
• A — allocation space
• P — payment space
• V — valuation type
• U — utility type

The transfer mechanism itself stores only an allocation rule and a payment rule. Utility construction is external: quasi-linearity is one important specialization, but it is not baked into the most general structure.

Structure hierarchy

Mechanism I T O                                  -- outcome-only direct mechanism
  └─ MechanismWithTransfers I T A P              -- allocation + payment rules
       └─ SingleParameterMechanism I R           -- T i = R, A = I → R, P = R

MechanismWithTransfers I (fun _ => A → V) A P    -- valuation reports over A
  └─ MultipleParameterMechanism I A V P          -- named multiple-parameter layer

Main definitions

• MechanismWithTransfers — allocation rule + payment rule
• MechanismWithTransfers.quasiLinearUtility — utility induced by a value extractor and payment embedding
• SingleParameterMechanism — scalar reports, scalar-vector allocations, scalar payments
• MultipleParameterMechanism — valuation-function reports over an allocation space
• MechanismWithTransfers.toMechanism — forget the decomposition
• MechanismWithTransfers.toStrategicGame — induced strategic game under external utility
• MechanismWithTransfers.isDSIC — DSIC specialized to the induced game
• MechanismWithTransfers.isExPostIR — ex-post IR specialized to the induced game

References

• [Nisan et al., Algorithmic Game Theory, Ch. 9]
• [Maschler, Solan, Zamir, Game Theory, Ch. 11–12]

structure MechanismWithTransfers (I : Type u_1) (T : I → Type u_2) (A : Type u_3) (P : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A mechanism with monetary transfers.

• I — agents
• T — report/type space of each agent
• A — allocation space
• P — payment space

The mechanism stores only how reports determine allocations and payments. Utility is imposed later, for example by quasi-linear utility or some richer domain-specific construction.

• allocationRule : ((i : I) → T i) → A

  The allocation rule: given reports, choose an allocation.

• paymentRule : ((i : I) → T i) → I → P

  The payment rule: given reports, determine each agent's payment.

def MechanismWithTransfers.quasiLinearUtility {I : Type u_1} {T : I → Type u_2} {A : Type u_3} {P : Type u_4} {V : Type u_5} {U : Type u_6} (M : MechanismWithTransfers I T A P) [Sub U] (val : A → ((i : I) → T i) → I → V) (valueToUtility : V → U) (paymentToUtility : P → U) (r trueTypes : (i : I) → T i) (i : I) : U

Quasi-linear utility induced by:

• a valuation function on allocations
• an embedding of payments into utility space
• subtraction in the utility space

This permits, for example:

• V = U with identity payment embedding
• valuation codomains and payment codomains that differ but both map into U.

Equations

• M.quasiLinearUtility val valueToUtility paymentToUtility r trueTypes i = valueToUtility (val (M.allocationRule r) trueTypes i) - paymentToUtility (M.paymentRule r i)

def MechanismWithTransfers.toMechanism {I : Type u_1} {T : I → Type u_2} {A : Type u_3} {P : Type u_4} (M : MechanismWithTransfers I T A P) : Mechanism I T (A × (I → P))

Viewing MechanismWithTransfers as a general Mechanism.

The outcome type is A × (I → P) (allocation, payment vector).

Equations

• M.toMechanism = { outcome := fun (r : (i : I) → T i) => (M.allocationRule r, M.paymentRule r) }

def MechanismWithTransfers.toStrategicGame {I : Type u_1} {T : I → Type u_2} {A : Type u_3} {P : Type u_4} {U : Type u_6} (M : MechanismWithTransfers I T A P) (u : A → (I → P) → ((i : I) → T i) → I → U) (trueTypes : (i : I) → T i) : StrategicGame I U

The strategic game induced by a transfer mechanism and an external utility rule.

Utility is supplied as a function of:

• allocation
• payment vector
• true type profile
• agent index

Equations

• M.toStrategicGame u trueTypes = { strategy := T, payoff := fun (r : (i : I) → T i) (i : I) => u (M.allocationRule r) (M.paymentRule r) trueTypes i }

def MechanismWithTransfers.isDSIC {I : Type u_1} [DecidableEq I] {T : I → Type u_2} {A : Type u_3} {P : Type u_4} {U : Type u_6} (M : MechanismWithTransfers I T A P) [Preorder U] (u : A → (I → P) → ((i : I) → T i) → I → U) : Prop

DSIC for a mechanism with transfers, relative to an externally supplied utility rule.

Equations

• M.isDSIC u = ∀ (trueTypes : (i : I) → T i) (i : I), IsWeaklyDominant (M.toStrategicGame u trueTypes) i (trueTypes i)

def MechanismWithTransfers.isExPostIR {I : Type u_1} [DecidableEq I] {T : I → Type u_2} {A : Type u_3} {P : Type u_4} {U : Type u_6} (M : MechanismWithTransfers I T A P) [Preorder U] [Zero U] (u : A → (I → P) → ((i : I) → T i) → I → U) : Prop

Ex-post individual rationality for a mechanism with transfers, relative to an externally supplied utility rule.

Equations

• One or more equations did not get rendered due to their size.

def MechanismWithTransfers.toQuasiLinearGame {I : Type u_1} {T : I → Type u_2} {A : Type u_3} {P : Type u_4} {V : Type u_5} {U : Type u_6} (M : MechanismWithTransfers I T A P) [Sub U] (val : A → ((i : I) → T i) → I → V) (valueToUtility : V → U) (paymentToUtility : P → U) (trueTypes : (i : I) → T i) : StrategicGame I U

The standard quasi-linear specialization of toStrategicGame.

Equations

• One or more equations did not get rendered due to their size.

def MechanismWithTransfers.isQuasiLinearDSIC {I : Type u_1} [DecidableEq I] {T : I → Type u_2} {A : Type u_3} {P : Type u_4} {V : Type u_5} {U : Type u_6} (M : MechanismWithTransfers I T A P) [Sub U] [Preorder U] (val : A → ((i : I) → T i) → I → V) (valueToUtility : V → U) (paymentToUtility : P → U) : Prop

DSIC for quasi-linear utility, as a specialization of isDSIC.

Equations

• M.isQuasiLinearDSIC val valueToUtility paymentToUtility = M.isDSIC fun (a : A) (pay : I → P) (types : (i : I) → T i) (i : I) => valueToUtility (val a types i) - paymentToUtility (pay i)

def MechanismWithTransfers.isQuasiLinearExPostIR {I : Type u_1} [DecidableEq I] {T : I → Type u_2} {A : Type u_3} {P : Type u_4} {V : Type u_5} {U : Type u_6} (M : MechanismWithTransfers I T A P) [Sub U] [Preorder U] [Zero U] (val : A → ((i : I) → T i) → I → V) (valueToUtility : V → U) (paymentToUtility : P → U) : Prop

Ex-post IR for quasi-linear utility, as a specialization of isExPostIR.

Equations

• M.isQuasiLinearExPostIR val valueToUtility paymentToUtility = M.isExPostIR fun (a : A) (pay : I → P) (types : (i : I) → T i) (i : I) => valueToUtility (val a types i) - paymentToUtility (pay i)

Standard transfer-mechanism specializations

structure SingleParameterMechanism (I : Type u_1) (R : Type u_2) extends MechanismWithTransfers I (fun (x : I) => R) (I → R) R : Type (max u_1 u_2)

A single-parameter mechanism.

Each agent i has a single private type θ_i : R (their "value per unit"). The allocation gives each agent a scalar x_i : R (typically in [0, 1], interpreted as probability of winning or fractional quantity received). Payments are of the same scalar type R; utility is quasi-linear: θ_i · x_i - p_i.

In practice R = ℝ. The structure is kept polymorphic for generality.

This is the canonical setting for Myerson's revenue-optimal auction theorem and for characterizing implementable (DSIC) allocation rules via monotonicity.

• allocationRule : (I → R) → I → R
• paymentRule : (I → R) → I → R

def SingleParameterMechanism.IsAllocFeasible {I : Type u_1} {R : Type u_2} (M : SingleParameterMechanism I R) [Zero R] [One R] [LE R] : Prop

Allocation feasibility: each agent's allocation lies in [0, 1].

Requires Zero R, One R, and LE R (e.g., any linearly ordered field).

Equations

• M.IsAllocFeasible = ∀ (b : I → R) (i : I), 0 ≤ M.allocationRule b i ∧ M.allocationRule b i ≤ 1

def SingleParameterMechanism.IsMonotone {I : Type u_1} [DecidableEq I] {R : Type u_2} (M : SingleParameterMechanism I R) [Preorder R] : Prop

Monotonicity of the allocation rule.

Agent i's allocation is non-decreasing in i's reported type, holding all other reports fixed.

This is Myerson's necessary and sufficient condition for DSIC in the single-parameter setting (with quasi-linear utility and the appropriate payment formula). [Myerson 1981; AGT Thm 9.36]

Equations

• M.IsMonotone = ∀ (i : I) (θ θ' : R), θ ≤ θ' → ∀ (b : I → R), M.allocationRule (Function.update b i θ) i ≤ M.allocationRule (Function.update b i θ') i

@[reducible, inline]

abbrev SingleParameterMechanism.payment {I : Type u_1} {R : Type u_2} (M : SingleParameterMechanism I R) (b : I → R) : I → R

The payment vector induced by a bid profile in a single-parameter mechanism.

This is just the inherited MechanismWithTransfers.paymentRule, restated with single-parameter terminology.

Equations

• M.payment b = M.paymentRule b

def SingleParameterMechanism.quasiLinearValue {I : Type u_1} {R : Type u_2} [Mul R] (x θ : I → R) (i : I) : R

Quasi-linear value in the single-parameter setting: agent i with true type θᵢ gets allocation xᵢ, worth θᵢ * xᵢ.

Equations

• SingleParameterMechanism.quasiLinearValue x θ i = θ i * x i

def SingleParameterMechanism.quasiLinearUtility {I : Type u_1} {R : Type u_2} (M : SingleParameterMechanism I R) [Mul R] [Sub R] (b θ : I → R) (i : I) : R

Quasi-linear utility in the single-parameter setting: uᵢ(θ, b) = θᵢ * xᵢ(b) - pᵢ(b).

Equations

• M.quasiLinearUtility b θ i = SingleParameterMechanism.quasiLinearValue (M.allocationRule b) θ i - M.payment b i

theorem SingleParameterMechanism.quasiLinearUtility_eq_transferQuasiLinearUtility {I : Type u_1} {R : Type u_2} (M : SingleParameterMechanism I R) [Mul R] [Sub R] (b θ : I → R) (i : I) : M.quasiLinearUtility b θ i = M.quasiLinearUtility (fun (a : I → R) (types : (i : I) → (fun (x : I) => R) i) (j : I) => types j * a j) id id b θ i

The single-parameter quasi-linear utility is the specialization of the generic transfer-mechanism quasi-linear utility to val a θ i = θᵢ * aᵢ and identity payment embedding.

def SingleParameterMechanism.IsDSIC {I : Type u_1} [DecidableEq I] {R : Type u_2} (M : SingleParameterMechanism I R) [Mul R] [Sub R] [Preorder R] : Prop

Dominant-strategy incentive compatibility in the single-parameter, quasi-linear setting.

Truthful reporting θᵢ is weakly dominant for every agent under utility θᵢ * xᵢ(b) - pᵢ(b).

Equations

• M.IsDSIC = M.isDSIC fun (a pay types : I → R) (i : I) => types i * a i - pay i

def SingleParameterMechanism.IsImplementable {I : Type u_1} [DecidableEq I] {R : Type u_2} [Mul R] [Sub R] [Preorder R] (x : (I → R) → I → R) : Prop

An allocation rule is implementable if there exists some payment rule such that the resulting single-parameter mechanism is DSIC.

Equations

• SingleParameterMechanism.IsImplementable x = ∃ (p : (I → R) → I → R), { allocationRule := x, paymentRule := p }.IsDSIC

structure MultipleParameterMechanism (I : Type u_1) (A : Type u_2) (V : Type u_3) (P : Type u_4) extends MechanismWithTransfers I (fun (x : I) => A → V) A P : Type (max (max (max u_1 u_2) u_3) u_4)

A multiple-parameter mechanism with transfers.

Here A is the type of feasible allocations and V is the codomain of valuations. Agent i's type/report space is A → V: a valuation function assigning a value to every possible allocation. The mechanism then maps a profile of reported valuations to an allocation and a payment for each agent.

• allocationRule : (I → A → V) → A
• paymentRule : (I → A → V) → I → P

@[reducible, inline]

abbrev MultipleParameterMechanism.Valuation (A : Type u_4) (V : Type u_5) : Type (max u_4 u_5)

The valuation/type space of an agent in a multiple-parameter mechanism.

Equations

• MultipleParameterMechanism.Valuation A V = (A → V)

def MultipleParameterMechanism.valueOfAllocation {I : Type u_1} {A : Type u_2} {V : Type u_3} (a : A) (types : I → Valuation A V) (i : I) : V

The value extractor used by the generic quasi-linear transfer definitions: agent i evaluates allocation a by applying their valuation function to a.

Equations

• MultipleParameterMechanism.valueOfAllocation a types i = types i a