EconCSLib.MechanismDesign.Auction.MechBayesian

Mechanism-design primitives for incomplete-information settings.

This file adds a lightweight Bayesian layer on top of the existing Mechanism / MechanismWithTransfers hierarchy:

• agents have true types drawn from a common prior probability measure
• agents choose messages as functions of their types
• the mechanism maps message profiles to outcomes, or to allocations and payments

The goal here is only to model the objects cleanly. Equilibrium notions, interim / ex-ante utilities, and Bayesian incentive properties can be added on top of this interface in later files.

Structure hierarchy

BayesianMechanism I T M O                        -- prior + message-to-outcome rule
  └─ BayesianMechanismWithTransfers I T M A P    -- allocation + payment rules
       └─ DirectBayesianMechanismWithTransfers I T A P
                                                   -- direct revelation: M = T

MechanismWithTransfers I M A P                   -- complete-information projection
  ↑
BayesianMechanismWithTransfers.toMechanismWithTransfers

Main results

• BayesianMechanismWithTransfers.exAnte_revelation_principle — ex-ante revelation principle

References

• Vijay Krishna, Auction Theory, 2nd ed., 2010, Chapter 5
• Roger Myerson, Incentive Compatibility and the Bargaining Problem, 1979

structure BayesianMechanism (I : Type u_1) (T : I → Type u_2) [(i : I) → MeasurableSpace (T i)] (M : I → Type u_3) (O : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A mechanism in an incomplete-information environment.

T i is agent i's true type space, M i is agent i's message space, and prior is the common prior over type profiles.

This keeps the Harsanyi-style uncertainty separate from the mechanism map itself: the mechanism acts on reported messages, while the prior lives as extra Bayesian structure.

• prior : MeasureTheory.Measure ((i : I) → T i)

  Common prior probability measure over true type profiles.

• prob_prior : MeasureTheory.IsProbabilityMeasure self.prior

  The prior is a probability measure.

• outcome : ((i : I) → M i) → O

  Outcome rule as a function of reported messages.

@[reducible, inline]

abbrev BayesianMechanism.Strategy (Tᵢ : Type u_5) (Mᵢ : Type u_6) : Type (max u_5 u_6)

A pure reporting strategy in an incomplete-information mechanism: an agent maps each possible true type to a report/message.

Equations

• BayesianMechanism.Strategy Tᵢ Mᵢ = (Tᵢ → Mᵢ)

@[reducible, inline]

abbrev BayesianMechanism.StrategyProfile {I : Type u_1} (T : I → Type u_5) (M : I → Type u_6) : Type (max (max u_1 u_6) u_5)

A strategy profile for all agents in an incomplete-information mechanism.

Equations

• BayesianMechanism.StrategyProfile T M = ((i : I) → BayesianMechanism.Strategy (T i) (M i))

def BayesianMechanism.IsMeasurableStrategyProfile {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} [(i : I) → MeasurableSpace (M i)] (σ : StrategyProfile T M) : Prop

A measurable strategy profile for all agents in an incomplete-information mechanism.

Equations

• BayesianMechanism.IsMeasurableStrategyProfile σ = ∀ (i : I), Measurable (σ i)

def BayesianMechanism.inducedMessages {I : Type u_1} {T : I → Type u_2} {M : I → Type u_3} (σ : StrategyProfile T M) (t : (i : I) → T i) (i : I) : M i

The message profile induced by a true type profile and a strategy profile.

Equations

• BayesianMechanism.inducedMessages σ t i = σ i (t i)

def BayesianMechanism.toMechanism {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {O : Type u_4} (B : BayesianMechanism I T M O) : Mechanism I M O

Forget the prior and view a Bayesian mechanism simply as a mechanism on reported messages.

Equations

• B.toMechanism = { outcome := B.outcome }

@[reducible, inline]

abbrev DirectBayesianMechanism (I : Type u_1) (T : I → Type u_2) [(i : I) → MeasurableSpace (T i)] (O : Type u_3) : Type (max (max u_1 u_2) u_3)

A direct-revelation Bayesian mechanism: agents report in their own type spaces.

Equations

• DirectBayesianMechanism I T O = BayesianMechanism I T T O

def DirectBayesianMechanism.truthfulStrategy {I : Type u_1} {T : I → Type u_2} : BayesianMechanism.StrategyProfile T T

Truthful reporting in a direct Bayesian mechanism.

This is kept as a namespace-local definition, rather than always reusing the transfer-mechanism version, so the direct non-transfer interface remains self-contained.

Equations

• DirectBayesianMechanism.truthfulStrategy x✝ = id

structure BayesianMechanismWithTransfers (I : Type u_1) (T : I → Type u_2) [(i : I) → MeasurableSpace (T i)] (M : I → Type u_3) (A : Type u_4) (P : Type u_5) : Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

A transfer mechanism in an incomplete-information environment.

As in MechanismWithTransfers, the allocation and payment rules are stored separately, while the common prior records the incomplete-information structure. Utility is intentionally left external.

• prior : MeasureTheory.Measure ((i : I) → T i)

  Common prior probability measure over true type profiles.

• prob_prior : MeasureTheory.IsProbabilityMeasure self.prior

  The prior is a probability measure.

• allocationRule : ((i : I) → M i) → A

  Allocation rule from reported messages.

• paymentRule : ((i : I) → M i) → I → P

  Payment rule from reported messages.

@[reducible, inline]

abbrev BayesianMechanismWithTransfers.StrategyProfile {I : Type u_1} (T : I → Type u_6) (M : I → Type u_7) : Type (max (max u_1 u_7) u_6)

A pure reporting strategy profile for a Bayesian transfer mechanism.

Equations

• BayesianMechanismWithTransfers.StrategyProfile T M = BayesianMechanism.StrategyProfile T M

def BayesianMechanismWithTransfers.inducedAllocation {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) (σ : StrategyProfile T M) (t : (i : I) → T i) : A

The allocation induced by a strategy profile and a realized type profile.

Equations

• B.inducedAllocation σ t = B.allocationRule (BayesianMechanism.inducedMessages σ t)

def BayesianMechanismWithTransfers.inducedPayments {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) (σ : StrategyProfile T M) (t : (i : I) → T i) : I → P

The payment vector induced by a strategy profile and a realized type profile.

Equations

• B.inducedPayments σ t = B.paymentRule (BayesianMechanism.inducedMessages σ t)

def BayesianMechanismWithTransfers.deviate {I : Type u_1} {T : I → Type u_2} {M : I → Type u_3} [DecidableEq I] (σ : StrategyProfile T M) (i : I) (τ : T i → M i) : StrategyProfile T M

Deviating from a strategy profile at one agent.

Equations

• BayesianMechanismWithTransfers.deviate σ i τ = Function.update σ i τ

def BayesianMechanismWithTransfers.toMechanismWithTransfers {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) : MechanismWithTransfers I M A P

Forget the Bayesian prior and recover the underlying transfer mechanism on reported messages.

Equations

• B.toMechanismWithTransfers = { allocationRule := B.allocationRule, paymentRule := B.paymentRule }

def BayesianMechanismWithTransfers.toBayesianMechanism {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) : BayesianMechanism I T M (A × (I → P))

Forget the transfer decomposition and recover the corresponding Bayesian mechanism with outcome space A × (I → P).

Equations

• B.toBayesianMechanism = { prior := B.prior, prob_prior := ⋯, outcome := fun (r : (i : I) → M i) => (B.allocationRule r, B.paymentRule r) }

noncomputable def BayesianMechanismWithTransfers.exAnteExpectedUtility {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) (u : A → (I → P) → ((i : I) → T i) → I → ℝ) (σ : StrategyProfile T M) (i : I) : ℝ

Ex-ante expected utility of agent i under a strategy profile.

The utility rule is supplied externally, as in MechanismWithTransfers: it depends on the induced allocation, the induced payments, the realized true type profile, and the agent index.

Equations

• B.exAnteExpectedUtility u σ i = ∫ (t : (i : I) → T i), u (B.inducedAllocation σ t) (B.inducedPayments σ t) t i ∂B.prior

def BayesianMechanismWithTransfers.IntegrableExAnteUtility {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) (u : A → (I → P) → ((i : I) → T i) → I → ℝ) (σ : StrategyProfile T M) (i : I) : Prop

Integrability of ex-ante utilities for agent i under a strategy profile.

Equations

• B.IntegrableExAnteUtility u σ i = MeasureTheory.Integrable (fun (t : (i : I) → T i) => u (B.inducedAllocation σ t) (B.inducedPayments σ t) t i) B.prior

def BayesianMechanismWithTransfers.IsExAnteBayesianNashEquilibrium {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} [DecidableEq I] [(i : I) → MeasurableSpace (M i)] (B : BayesianMechanismWithTransfers I T M A P) (u : A → (I → P) → ((i : I) → T i) → I → ℝ) (σ : StrategyProfile T M) : Prop

An ex-ante Bayesian Nash equilibrium of a transfer mechanism.

No agent can improve their ex-ante expected utility by replacing their reporting rule with any other measurable pure type-contingent reporting rule.

This is the ex-ante notion: expectations are taken under the full prior, not conditional on agent i's realized type. The standard interim BNE notion from mechanism design is a natural future extension.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev DirectBayesianMechanismWithTransfers (I : Type u_1) (T : I → Type u_2) [(i : I) → MeasurableSpace (T i)] (A : Type u_3) (P : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A direct-revelation Bayesian transfer mechanism.

Equations

• DirectBayesianMechanismWithTransfers I T A P = BayesianMechanismWithTransfers I T T A P

def DirectBayesianMechanismWithTransfers.truthfulStrategy {I : Type u_1} {T : I → Type u_2} : BayesianMechanismWithTransfers.StrategyProfile T T

Truthful reporting in a direct Bayesian mechanism with transfers.

Equations

• DirectBayesianMechanismWithTransfers.truthfulStrategy x✝ = id

def BayesianMechanismWithTransfers.directRevelation {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) (σ : StrategyProfile T M) : DirectBayesianMechanismWithTransfers I T A P

The direct-revelation mechanism induced by an indirect mechanism and a strategy profile.

An agent reports their type directly; the mechanism then feeds these reports through the original equilibrium reporting strategies and applies the original allocation and payment rules. This is the standard object behind the revelation principle.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BayesianMechanismWithTransfers.directRevelation_allocation_truthful {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) (σ : StrategyProfile T M) (t : (i : I) → T i) : (B.directRevelation σ).allocationRule t = B.inducedAllocation σ t

Under truthful reporting in the induced direct mechanism, the realized allocation agrees definitionally with the original mechanism played under σ.

@[simp]

theorem BayesianMechanismWithTransfers.directRevelation_payments_truthful {I : Type u_1} {T : I → Type u_2} [(i : I) → MeasurableSpace (T i)] {M : I → Type u_3} {A : Type u_4} {P : Type u_5} (B : BayesianMechanismWithTransfers I T M A P) (σ : StrategyProfile T M) (t : (i : I) → T i) : (B.directRevelation σ).paymentRule t = B.inducedPayments σ t

Under truthful reporting in the induced direct mechanism, the realized payment vector agrees definitionally with the original mechanism played under σ.

def BayesianMechanismWithTransfers.ExAnteRevelationPrincipleConclusion {I : Type u_1} {T : I → Type u_2} {M : I → Type u_3} {A : Type u_4} {P : Type u_5} [DecidableEq I] [(i : I) → MeasurableSpace (T i)] [(i : I) → MeasurableSpace (M i)] (B : BayesianMechanismWithTransfers I T M A P) (u : A → (I → P) → ((i : I) → T i) → I → ℝ) (σ : StrategyProfile T M) : Prop

The revelation-principle target property attached to a strategy profile.

This packages the statement we will eventually want to prove: if σ is an equilibrium of the indirect mechanism, then truthful reporting is a Bayesian equilibrium of the induced direct mechanism.

Equations

• B.ExAnteRevelationPrincipleConclusion u σ = BayesianMechanismWithTransfers.IsExAnteBayesianNashEquilibrium (B.directRevelation σ) u DirectBayesianMechanismWithTransfers.truthfulStrategy

theorem BayesianMechanismWithTransfers.exAnte_revelation_principle {I : Type u_1} {T : I → Type u_2} {M : I → Type u_3} {A : Type u_4} {P : Type u_5} [DecidableEq I] [(i : I) → MeasurableSpace (T i)] [(i : I) → MeasurableSpace (M i)] (B : BayesianMechanismWithTransfers I T M A P) (u : A → (I → P) → ((i : I) → T i) → I → ℝ) (σ : StrategyProfile T M) (hσ : B.IsExAnteBayesianNashEquilibrium u σ) : B.ExAnteRevelationPrincipleConclusion u σ

Revelation principle, ex-ante form: if σ is a Bayesian Nash equilibrium of the indirect mechanism, then truthful reporting is a Bayesian Nash equilibrium of the induced direct mechanism.

This is the ex-ante version because IsExAnteBayesianNashEquilibrium above is defined via ex-ante expected utility rather than interim conditional utility.

References:

• [Myerson 1979, "Incentive Compatibility and the Bargaining Problem"]
• [Krishna 2010, Ch. 5]