• Mechanisms With Transfers

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

  structure SingleParameterMechanism (I : Type*) (R : Type*)
      extends MechanismWithTransfers I (fun _ => R) (I → R) R
  
  namespace SingleParameterMechanism
  
  variable {I : Type*} [DecidableEq I] {R : Type*}
  variable (M : SingleParameterMechanism I R)
  
  /-- Allocation feasibility: each agent's allocation lies in `[0, 1]`.
  
    Requires `Zero R`, `One R`, and `LE R` (e.g., any linearly ordered field). -/

• def SingleParameterMechanism.IsAllocFeasible EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def IsAllocFeasible [Zero R] [One R] [LE R] : Prop :=
    ∀ (b : I → R) (i : I), 0 ≤ M.allocationRule b i ∧ M.allocationRule b i ≤ 1

• def SingleParameterMechanism.IsMonotone EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def IsMonotone [Preorder R] : Prop

• abbrev SingleParameterMechanism.payment EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  abbrev payment (b : I → R) : I → R :=
    M.paymentRule b

• def SingleParameterMechanism.quasiLinearValue EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def quasiLinearValue [Mul R]
      (x θ : I → R) (i : I) : R :=
    θ i * x i

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

  def quasiLinearUtility [Mul R] [Sub R]
      (b θ : I → R) (i : I) : R :=
    quasiLinearValue (M.allocationRule b) θ i - M.payment b i

• lemma SingleParameterMechanism.quasiLinearUtility_eq_transferQuasiLinearUtility EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  lemma quasiLinearUtility_eq_transferQuasiLinearUtility [Mul R] [Sub R]
      (b θ : I → R) (i : I) :
      M.quasiLinearUtility b θ i =
        MechanismWithTransfers.quasiLinearUtility
          (I := I) (T := fun _ => R) (A := I → R) (P := R) (V := R) (U := R)
          ({ allocationRule := M.allocationRule
             paymentRule

• def SingleParameterMechanism.IsDSIC EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def IsDSIC [Mul R] [Sub R] [Preorder R] : Prop

• def SingleParameterMechanism.IsImplementable EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Transfer

  def IsImplementable [Mul R] [Sub R] [Preorder R]
      (x : (I → R) → I → R) : Prop :=
    ∃ p : (I → R) → I → R,
      ( { allocationRule := x
          paymentRule := p } : SingleParameterMechanism I R).IsDSIC

Modules: EconCSLib.MechanismDesign.Auction.Transfer