Mechanism Design.Myerson

Theorem Myerson Monotonicity Characterization proved

Proof plan Myerson Optimal Auction Legacy Plan staged

Definition Myerson Payment Construction (withMyersonPayment) formalized

Lemma Myerson Payment Envelope Lemmas proved

Definition Myerson Payment Formula formalized

Theorem Myerson Reserve-Price Characterisation staged

Theorem Regular Myerson Optimal Single-Item Auction proved

Theorem Revenue Equivalence Theorem staged

Definition Virtual Values and Regularity formalized

Definition Virtual-Surplus-Maximizing Allocation formalized