• Myerson Payment Formula
• Myerson Payment Envelope Lemmas
• Myerson Payment Construction (withMyersonPayment)

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

  theorem isMonotone_of_isDSIC [DecidableEq I] {M : SingleParameterMechanism I ℝ}
      (hdsic : M.IsDSIC) :
      M.IsMonotone

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

  theorem withMyersonPayment_isDSIC_of_isMonotone [DecidableEq I]
      {x : (I → ℝ) → I → ℝ}
      (hx : IsMonotone ({ allocationRule := x, paymentRule := myersonPayment x } :
        SingleParameterMechanism I ℝ)) :
      (withMyersonPayment x).IsDSIC

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

  theorem isImplementable_of_isMonotone [DecidableEq I]
      {x : (I → ℝ) → I → ℝ}
      (hx : IsMonotone ({ allocationRule := x, paymentRule := myersonPayment x } :
        SingleParameterMechanism I ℝ)) :
      IsImplementable x

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

  theorem isImplementable_iff_isMonotone [DecidableEq I]
      (x : (I → ℝ) → I → ℝ) :
      IsImplementable x ↔
        IsMonotone ({ allocationRule := x, paymentRule := myersonPayment x } :
          SingleParameterMechanism I ℝ)

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

  theorem payment_formula_of_isDSIC_of_zeroNormalized [DecidableEq I]
      {x p : (I → ℝ) → I → ℝ}
      (hdsic : ({ allocationRule := x, paymentRule := p } :
        SingleParameterMechanism I ℝ).IsDSIC)
      (h0 : ZeroNormalized p)
      (b : I → ℝ) (i : I) :
      p b i = b i * x b i - ∫ z in 0..b i, x (Function.update b i z) i

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

  theorem payment_eq_myersonPayment_of_isDSIC_of_zeroNormalized [DecidableEq I]
      {x p : (I → ℝ) → I → ℝ}
      (hdsic : ({ allocationRule := x, paymentRule := p } :
        SingleParameterMechanism I ℝ).IsDSIC)
      (h0 : ZeroNormalized p) :
      p = myersonPayment x

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

  theorem existsUnique_zeroNormalized_payment_of_isMonotone [DecidableEq I]
      {x : (I → ℝ) → I → ℝ}
      (hx : IsMonotone ({ allocationRule := x, paymentRule := myersonPayment x } :
        SingleParameterMechanism I ℝ)) :
      ∃! p : (I → ℝ) → I → ℝ,
        ZeroNormalized p ∧
          ({ allocationRule := x, paymentRule := p } : SingleParameterMechanism I ℝ).IsDSIC

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

  theorem payment_formula_of_zeroNormalized_and_isDSIC [DecidableEq I]
      {x p : (I → ℝ) → I → ℝ}
      (hp : ZeroNormalized p ∧
        ({ allocationRule := x, paymentRule := p } : SingleParameterMechanism I ℝ).IsDSIC)
      (b : I → ℝ) (i : I) :
      p b i = b i * x b i - ∫ z in 0..b i, x (Function.update b i z) i

Modules: EconCSLib.MechanismDesign.Auction.Myerson