Keyword: mechanism-design

Definition Basic Auction Formats formalized

Definition Bayesian Mechanisms formalized

Definition Bayesian Selling Problem (IPV) staged

Definition DSIC Predicate formalized

Definition Direct Mechanism Interface formalized

Definition Ex-Ante Equilibrium Predicates formalized

Definition Ex-Ante Expected Utility (Bayesian Mechanisms) formalized

Theorem Ex-Ante Revelation Principle Interface proved

Definition Ex-Post Individual Rationality Predicate formalized

Definition Induced Strategic Game formalized

Definition Mechanisms With Transfers formalized

Definition Multiple-Parameter Transfer Layer formalized

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 Single-Parameter Transfer Layer formalized

Definition Strategy-Proof Social Choice Function formalized

Theorem Strategy-Proofness of Gale-Shapley for the Proposing Side (Roth 1982) staged

Theorem Truthfulness From DSIC proved

Theorem VCG Payment Identity proved

Definition VCG Social Welfare formalized

Theorem VCG Truthfulness And Individual Rationality proved

Definition VCG Welfare And Payments formalized

Definition VCG Welfare Without Agent i formalized

Definition Virtual Values and Regularity formalized

Definition Virtual-Surplus-Maximizing Allocation formalized