• Direct Mechanism Interface
• DSIC Predicate
• Ex-Post Individual Rationality Predicate

• structure MechanismWithTransfers EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  structure MechanismWithTransfers
      (I : Type*) (T : I → Type*) (A : Type*) (P : Type*) where
    /-- The allocation rule: given reports, choose an allocation. -/
    allocationRule : (∀ i, T i) → A
    /-- The payment rule: given reports, determine each agent's payment. -/
    paymentRule : (∀ i, T i) → I → P

• def MechanismWithTransfers.quasiLinearUtility EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def quasiLinearUtility [Sub U]
      (val : A → (∀ i, T i) → I → V)
      (valueToUtility : V → U) (paymentToUtility : P → U)
      (r : ∀ i, T i) (trueTypes : ∀ i, T i) (i : I) : U :=
    valueToUtility (val (M.allocationRule r) trueTypes i) -
      paymentToUtility (M.paymentRule r i)

• def MechanismWithTransfers.toMechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def toMechanism :
      Mechanism I T (A × (I → P)) where
    outcome r := (M.allocationRule r, M.paymentRule r)

• def MechanismWithTransfers.toStrategicGame EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def toStrategicGame
      (u : A → (I → P) → (∀ i, T i) → I → U)
      (trueTypes : ∀ i, T i) : StrategicGame I U where
    strategy := T
    payoff r i := u (M.allocationRule r) (M.paymentRule r) trueTypes i

• def MechanismWithTransfers.isDSIC EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

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

  def isDSIC [Preorder U]
      (u : A → (I → P) → (∀ i, T i) → I → U) : Prop :=
    ∀ trueTypes : (∀ i, T i), ∀ i : I,
      IsWeaklyDominant (M.toStrategicGame u trueTypes) i (trueTypes i)

• def MechanismWithTransfers.isExPostIR EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def isExPostIR [Preorder U] [Zero U]
      (u : A → (I → P) → (∀ i, T i) → I → U) : Prop :=
    ∀ trueTypes : (∀ i, T i), ∀ i : I, ∀ r : (∀ i, T i),
      0 ≤ u (M.allocationRule (Function.update r i (trueTypes i)))
        (M.paymentRule (Function.update r i (trueTypes i))) trueTypes i

• def MechanismWithTransfers.toQuasiLinearGame EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  The standard quasi-linear specialization of `toStrategicGame`.

  def toQuasiLinearGame [Sub U]
      (val : A → (∀ i, T i) → I → V)
      (valueToUtility : V → U) (paymentToUtility : P → U)
      (trueTypes : ∀ i, T i) : StrategicGame I U :=
    M.toStrategicGame
      (fun a pay types i => valueToUtility (val a types i) - paymentToUtility (pay i))
      trueTypes

• def MechanismWithTransfers.isQuasiLinearDSIC EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

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

  def isQuasiLinearDSIC [Sub U] [Preorder U]
      (val : A → (∀ i, T i) → I → V)
      (valueToUtility : V → U) (paymentToUtility : P → U) : Prop :=
    M.isDSIC (fun a pay types i => valueToUtility (val a types i) - paymentToUtility (pay i))

• def MechanismWithTransfers.isQuasiLinearExPostIR EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

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

  def isQuasiLinearExPostIR [Sub U] [Preorder U] [Zero U]
      (val : A → (∀ i, T i) → I → V)
      (valueToUtility : V → U) (paymentToUtility : P → U) : Prop :=
    M.isExPostIR (fun a pay types i => valueToUtility (val a types i) - paymentToUtility (pay i))

Modules: EconCSLib.MechanismDesign.Auction.Transfer