• Ex-Ante Equilibrium Predicates

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

  def directRevelation
      (B : BayesianMechanismWithTransfers I T M A P)
      (σ : StrategyProfile T M) :
      DirectBayesianMechanismWithTransfers I T A P where
    prior := B.prior
    prob_prior := B.prob_prior
    allocationRule t := B.inducedAllocation σ t
    paymentRule t := B.inducedPayments σ t

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

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

• theorem BayesianMechanismWithTransfers.exAnte_revelation_principle EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.MechBayesian

  theorem exAnte_revelation_principle
      [DecidableEq I]
      [∀ i, MeasurableSpace (T i)]
      [∀ i, MeasurableSpace (M i)]
      (B : BayesianMechanismWithTransfers I T M A P)
      (u : A → (I → P) → (∀ i, T i) → I → ℝ)
      (σ : StrategyProfile T M)
      (hσ : B.IsExAnteBayesianNashEquilibrium u σ) :
      B.ExAnteRevelationPrincipleConclusion u σ

Modules: EconCSLib.MechanismDesign.Auction.MechBayesian