Lean declarations

structure BayesianMechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

structure BayesianMechanism
    (I : Type*) (T : I → Type*) [∀ i, MeasurableSpace (T i)]
    (M : I → Type*) (O : Type*) where
  /-- Common prior probability measure over true type profiles. -/
  prior : MeasureTheory.Measure (∀ i, T i)
  /-- The prior is a probability measure. -/
  prob_prior : MeasureTheory.IsProbabilityMeasure prior
  /-- Outcome rule as a function of reported messages. -/
  outcome : (∀ i, M i) → O

abbrev BayesianMechanism.Strategy EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
```
abbrev Strategy (Tᵢ : Type*) (Mᵢ : Type*) := Tᵢ → Mᵢ
```
abbrev BayesianMechanism.StrategyProfile EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
A strategy profile for all agents in an incomplete-information mechanism.
```
abbrev StrategyProfile (T : I → Type*) (M : I → Type*) := ∀ i, Strategy (T i) (M i)
```
def BayesianMechanism.IsMeasurableStrategyProfile EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
A measurable strategy profile for all agents in an incomplete-information mechanism.
```
def IsMeasurableStrategyProfile
    [∀ i, MeasurableSpace (M i)]
    (σ : StrategyProfile T M) : Prop :=
  ∀ i, Measurable (σ i)
```
def BayesianMechanism.inducedMessages EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
The message profile induced by a true type profile and a strategy profile.
```
def inducedMessages (σ : StrategyProfile T M) (t : ∀ i, T i) : ∀ i, M i :=
  fun i => σ i (t i)
```
def BayesianMechanism.toMechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
```
def toMechanism (B : BayesianMechanism I T M O) : Mechanism I M O where
  outcome := B.outcome
```
abbrev DirectBayesianMechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
A direct-revelation Bayesian mechanism: agents report in their own type spaces.
```
abbrev DirectBayesianMechanism
    (I : Type*) (T : I → Type*) [∀ i, MeasurableSpace (T i)] (O : Type*) :=
  BayesianMechanism I T T O
```
def DirectBayesianMechanism.truthfulStrategy EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
```
def truthfulStrategy : BayesianMechanism.StrategyProfile T T :=
  fun _ => id
```

structure BayesianMechanismWithTransfers EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

structure BayesianMechanismWithTransfers
    (I : Type*) (T : I → Type*) [∀ i, MeasurableSpace (T i)]
    (M : I → Type*) (A : Type*) (P : Type*) where
  /-- Common prior probability measure over true type profiles. -/
  prior : MeasureTheory.Measure (∀ i, T i)
  /-- The prior is a probability measure. -/
  prob_prior : MeasureTheory.IsProbabilityMeasure prior
  /-- Allocation rule from reported messages. -/
  allocationRule : (∀ i, M i) → A
  /-- Payment rule from reported messages. -/
  paymentRule : (∀ i, M i) → I → P

abbrev BayesianMechanismWithTransfers.StrategyProfile EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
A pure reporting strategy profile for a Bayesian transfer mechanism.
```
abbrev StrategyProfile (T : I → Type*) (M : I → Type*) :=
  BayesianMechanism.StrategyProfile T M
```
def BayesianMechanismWithTransfers.inducedAllocation EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
The allocation induced by a strategy profile and a realized type profile.
```
def inducedAllocation
    (B : BayesianMechanismWithTransfers I T M A P)
    (σ : StrategyProfile T M) (t : ∀ i, T i) : A :=
  B.allocationRule (BayesianMechanism.inducedMessages σ t)
```
def BayesianMechanismWithTransfers.inducedPayments EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
The payment vector induced by a strategy profile and a realized type profile.
```
def inducedPayments
    (B : BayesianMechanismWithTransfers I T M A P)
    (σ : StrategyProfile T M) (t : ∀ i, T i) : I → P :=
  B.paymentRule (BayesianMechanism.inducedMessages σ t)
```
def BayesianMechanismWithTransfers.deviate EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian
Deviating from a strategy profile at one agent.
```
def deviate
    [DecidableEq I]
    (σ : StrategyProfile T M) (i : I) (τ : T i → M i) :
    StrategyProfile T M :=
  Function.update σ i τ
```

def BayesianMechanismWithTransfers.toMechanismWithTransfers EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

def toMechanismWithTransfers
    (B : BayesianMechanismWithTransfers I T M A P) :
    MechanismWithTransfers I M A P where
  allocationRule := B.allocationRule
  paymentRule := B.paymentRule

def BayesianMechanismWithTransfers.toBayesianMechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

def toBayesianMechanism
    (B : BayesianMechanismWithTransfers I T M A P) :
    BayesianMechanism I T M (A × (I → P)) where
  prior := B.prior
  prob_prior := B.prob_prior
  outcome r := (B.allocationRule r, B.paymentRule r)

Modules: EconCSLib.MechanismDesign.Auction.MechBayesian

Bayesian Mechanisms

Bayesian mechanisms record type spaces, message spaces, a common prior, and type-contingent strategies. They induce messages from strategy profiles and can be converted to direct or transfer mechanisms.

For mechanisms with transfers, the interface also records induced allocations, induced payments, deviations, and the associated Bayesian mechanism obtained by forgetting the allocation/payment decomposition.

References

[AGT, Chapter 9, Section 9.6, Def. 9.41] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Bayesian mechanisms, type spaces, strategies, and expected utilities.
[MFoGT, Chapter 7, Section 7.4] Maschler, Solan, and Zamir, Game Theory. Bayesian games and Bayesian equilibrium background.

Used by auctions

[[mechanism_design.auction.bayesian.single_item_framework]] (single-item Bayesian auction framework).

Provenance

Migrated from EconCSLib pull request 27, old blueprint label def:md_bayesian_interface in blueprint/src/content.tex.

Bayesian Mechanisms

References

Used by auctions

Provenance

Used by

Also in