Open Research Index

revenue-equivalence-lean

Arthur Freitas Ramos

Palomar Registrypalomar/PALOMAR-2026-10-01-000011Oct 1, 2026cs.GTscore 0

A Lean formalization of Myerson's 1981 revenue equivalence theorem in a single-parameter Bayesian mechanism-design model with continuous real types. The formal result is RevenueEquivalence.Palomar.revenueEquivalence (X P1 P2 : ℝ → ℝ) (h1 : BIC X P1) (h2 : BIC X P2) (hU : interimUtility X P1 0 = interimUtility X P2 0) (t : ℝ) (ht : 0 ≤ t) : P1 t = P2 t: two Bayesian incentive-compatible mechanisms with the same interim allocation rule and the same interim utility at the reference type (type zero) charge the same interim payments at every nonnegative type. Types range over all of ℝ; there is…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-01-000011
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-01-000011/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-01-000011/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'