EconCSLib.MechanismDesign.Auction.Myerson

Myerson-specific theory for single-parameter mechanisms over ℝ.

This file extends the single-parameter transfer mechanism layer with:

• the canonical payment rule myersonPayment
• the induced mechanism withMyersonPayment
• zero normalization
• the monotonicity, implementability, and uniqueness statements usually grouped under Myerson's Lemma

It is the mechanism-design layer that depends on interval integration.

Structure hierarchy

MechanismWithTransfers I (fun _ => ℝ) (I → ℝ) ℝ   -- scalar reports, scalar allocations
  └─ SingleParameterMechanism I ℝ                 -- single-parameter layer
       └─ withMyersonPayment x                    -- allocation rule + Myerson payment

SingleParameterMechanism.IsMonotone               -- implementability condition
  └─ SingleParameterMechanism.IsDSIC              -- via Myerson payment formula

noncomputable def SingleParameterMechanism.myersonPayment {I : Type u_1} [DecidableEq I] (x : (I → ℝ) → I → ℝ) (b : I → ℝ) (i : I) : ℝ

The canonical Myerson payment formula associated with an allocation rule x. Holding all other bids fixed, agent i pays

bᵢ xᵢ(b) - ∫₀^{bᵢ} xᵢ(z, b₋ᵢ) dz.

Equations

• SingleParameterMechanism.myersonPayment x b i = b i * x b i - ∫ (z : ℝ) in 0..b i, x (Function.update b i z) i

noncomputable def SingleParameterMechanism.withMyersonPayment {I : Type u_1} [DecidableEq I] (x : (I → ℝ) → I → ℝ) : SingleParameterMechanism I ℝ

The single-parameter mechanism obtained by equipping an allocation rule with its canonical Myerson payment rule.

Equations

• SingleParameterMechanism.withMyersonPayment x = { allocationRule := x, paymentRule := SingleParameterMechanism.myersonPayment x }

theorem SingleParameterMechanism.withMyersonPayment_quasiLinearUtility_eq {I : Type u_1} [DecidableEq I] (x : (I → ℝ) → I → ℝ) (v b : I → ℝ) (i : I) : (withMyersonPayment x).quasiLinearUtility b v i = (v i - b i) * x b i + ∫ (z : ℝ) in 0..b i, x (Function.update b i z) i

Utility under the canonical Myerson payment rule can be written in the standard envelope-friendly form.

def SingleParameterMechanism.ZeroNormalized {I : Type u_1} [DecidableEq I] (p : (I → ℝ) → I → ℝ) : Prop

Zero normalization for payment rules: reporting 0 yields payment 0, holding the other reports fixed.

Equations

• SingleParameterMechanism.ZeroNormalized p = ∀ (i : I) (b : I → ℝ), p (Function.update b i 0) i = 0

theorem SingleParameterMechanism.myersonPayment_zeroNormalized {I : Type u_1} [DecidableEq I] (x : (I → ℝ) → I → ℝ) : ZeroNormalized (myersonPayment x)

The canonical Myerson payment rule is zero-normalized.

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

Myerson Lemma, Property 1: every DSIC single-parameter mechanism has a monotone allocation rule.

theorem SingleParameterMechanism.payment_sandwich {I : Type u_1} [DecidableEq I] {x p : (I → ℝ) → I → ℝ} (hdsic : { allocationRule := x, paymentRule := p }.IsDSIC) (b : I → ℝ) (i : I) (y z : ℝ) : z * (x (Function.update b i y) i - x (Function.update b i z) i) ≤ p (Function.update b i y) i - p (Function.update b i z) i ∧ p (Function.update b i y) i - p (Function.update b i z) i ≤ y * (x (Function.update b i y) i - x (Function.update b i z) i)

For a DSIC single-parameter mechanism, fixing all other bids yields the standard two-sided bound on payment differences.

theorem SingleParameterMechanism.payment_difference_bound {I : Type u_1} [DecidableEq I] {x p q : (I → ℝ) → I → ℝ} (hpdsic : { allocationRule := x, paymentRule := p }.IsDSIC) (hqdsic : { allocationRule := x, paymentRule := q }.IsDSIC) (b : I → ℝ) (i : I) (y z : ℝ) : |p (Function.update b i y) i - q (Function.update b i y) i - (p (Function.update b i z) i - q (Function.update b i z) i)| ≤ (y - z) * (x (Function.update b i y) i - x (Function.update b i z) i)

If two payment rules implement the same allocation rule in DSIC form, then their difference along a one-dimensional deviation is controlled by the change in the allocation rule. This is the comparison estimate used in the proof of the Myerson payment identity.

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

Myerson Lemma, Property 2: a monotone allocation rule is DSIC when paired with the canonical Myerson payment rule.

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

Myerson Lemma, Property 2, reformulated: an allocation rule is implementable if it is monotone.

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

Myerson Lemma (a): an allocation rule is implementable if and only if it is monotone.

theorem SingleParameterMechanism.payment_formula_of_isDSIC_of_zeroNormalized {I : Type u_1} [DecidableEq I] {x p : (I → ℝ) → I → ℝ} (hdsic : { allocationRule := x, paymentRule := p }.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

Explicit payment identity used in Myerson's Lemma: for a DSIC single-parameter mechanism with zero-normalized payments, the payment rule is given pointwise by the Myerson payment identity.

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

Uniqueness of zero-normalized DSIC payment rules: among zero-normalized payment rules, the canonical Myerson payment rule is the unique one that implements a monotone allocation rule.

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

Myerson Lemma (b): if x is monotone, then there is a unique zero-normalized payment rule making (x, p) DSIC.

theorem SingleParameterMechanism.payment_formula_of_zeroNormalized_and_isDSIC {I : Type u_1} [DecidableEq I] {x p : (I → ℝ) → I → ℝ} (hp : ZeroNormalized p ∧ { allocationRule := x, paymentRule := p }.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

Myerson Lemma (c): the unique zero-normalized DSIC payment rule from (b) is given by the explicit formula bᵢ xᵢ(b) - ∫₀^{bᵢ} xᵢ(z, b₋ᵢ) dz.