• Single-Parameter Transfer Layer

• def SingleParameterMechanism.myersonPayment EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Myerson

  noncomputable def myersonPayment
      [DecidableEq I]
      (x : (I → ℝ) → I → ℝ) (b : I → ℝ) (i : I) : ℝ :=
    b i * x b i - ∫ z in 0..b i, x (Function.update b i z) i

• def SingleParameterMechanism.ZeroNormalized EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Myerson

  def ZeroNormalized [DecidableEq I] (p : (I → ℝ) → I → ℝ) : Prop :=
    ∀ (i : I) (b : I → ℝ), p (Function.update b i 0) i = 0

• theorem SingleParameterMechanism.myersonPayment_zeroNormalized EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.Myerson

  The canonical Myerson payment rule is zero-normalized.

  theorem myersonPayment_zeroNormalized [DecidableEq I] (x : (I → ℝ) → I → ℝ) :
      ZeroNormalized (myersonPayment x)

Modules: EconCSLib.MechanismDesign.Auction.Myerson