• Bayesian Mechanisms
• Ex-Ante Expected Utility (Bayesian Mechanisms)

• def BayesianMechanismWithTransfers.IntegrableExAnteUtility EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

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

  def IntegrableExAnteUtility
      (B : BayesianMechanismWithTransfers I T M A P)
      (u : A → (I → P) → (∀ i, T i) → I → ℝ)
      (σ : StrategyProfile T M) (i : I) : Prop :=
    Integrable (fun t => u (B.inducedAllocation σ t) (B.inducedPayments σ t) t i) B.prior

• def BayesianMechanismWithTransfers.IsExAnteBayesianNashEquilibrium EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

  def IsExAnteBayesianNashEquilibrium
      [DecidableEq I]
      [∀ i, MeasurableSpace (M i)]
      (B : BayesianMechanismWithTransfers I T M A P)
      (u : A → (I → P) → (∀ i, T i) → I → ℝ)
      (σ : StrategyProfile T M) : Prop

• abbrev DirectBayesianMechanismWithTransfers EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

  A direct-revelation Bayesian transfer mechanism.

  abbrev DirectBayesianMechanismWithTransfers
      (I : Type*) (T : I → Type*) [∀ i, MeasurableSpace (T i)] (A : Type*) (P : Type*) :=
    BayesianMechanismWithTransfers I T T A P

• def DirectBayesianMechanismWithTransfers.truthfulStrategy EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

  Truthful reporting in a direct Bayesian mechanism with transfers.

  def truthfulStrategy :
      BayesianMechanismWithTransfers.StrategyProfile T T :=
    fun _ => id

Modules: EconCSLib.MechanismDesign.Auction.MechBayesian