Definition Bayesian Single-Item Auction Framework

✓ definition formalized

Lean declarations

structure TypeCDF EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

A scalar type distribution on the interval `[0, ω]`, recorded by its CDF.

structure TypeCDF (ω : ℝ) where
  /-- Upper bound of the support interval is nonnegative. -/
  omega_nonneg : 0 ≤ ω
  /-- Cumulative distribution function. -/
  cdf : ℝ → ℝ
  /-- Monotonicity of the CDF on the support interval. -/
  monotoneOn_cdf : MonotoneOn cdf (Set.Icc 0 ω)
  /-- Normalization at the lower endpoint. -/
  cdf_zero : cdf 0 = 0
  /-- Normalization at the upper endpoint. -/
  cdf_upper : cdf ω = 1
  /-- Smoothness assumption used in continuous-type auction theory. -/
  differentiableOn_cdf : DifferentiableOn ℝ cdf (Set.Ioo 0 ω)

structure ContinuousTypeProfile EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

Agent-specific continuous private-value data.

structure ContinuousTypeProfile (I : Type*) where
  /-- Agent-specific upper bounds `ωᵢ` for the type support. -/
  omega : I → ℝ
  /-- Agent-specific CDFs `Fᵢ` on `[0, ωᵢ]`. -/
  cdf : ∀ i, TypeCDF (omega i)

abbrev OpponentProfile EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem
Opponent profiles for agent `i`, with constant coordinate type `X`.
```
abbrev OpponentProfile (I : Type*) (X : Type*) (i : I) := ∀ _ : {j // j ≠ i}, X
```
abbrev OpponentTypeProfile EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem
Opponent type profiles for real-valued auction types.
```
abbrev OpponentTypeProfile (I : Type*) (i : I) := OpponentProfile I ℝ i
```

structure BayesianSingleItemAuction EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

structure BayesianSingleItemAuction (I : Type*)
    extends SingleParameterMechanism I ℝ where
  /-- Common prior probability measure over true type profiles. -/
  prior : MeasureTheory.Measure (∀ _ : I, ℝ)
  /-- The prior is a probability measure. -/
  prob_prior : MeasureTheory.IsProbabilityMeasure prior
  /-- Opponent-type prior `μᵢ` used for interim expectations conditional on a
  fixed report by agent `i`. -/
  opponentPrior : (i : I) → MeasureTheory.Measure (OpponentTypeProfile I i)
  /-- Each opponent-type prior is a probability measure. -/
  prob_opponentPrior :
    ∀ i : I, MeasureTheory.IsProbabilityMeasure (opponentPrior i)
  /-- Continuous private-value support and CDF data for each agent. -/
  typeData : ContinuousTypeProfile I

def BayesianSingleItemAuction.profileInsert EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

Insert one coordinate into an opponent profile.

noncomputable def profileInsert (i : I) (x : X) (t : OpponentProfile I X i) :
    ∀ _ : I, X := by
  classical
  exact fun j => if h : j = i then x else t ⟨j, h⟩

def BayesianSingleItemAuction.toDirectBayesianMechanismWithTransfers EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

def toDirectBayesianMechanismWithTransfers (A : BayesianSingleItemAuction I) :
    DirectBayesianMechanismWithTransfers I (fun _ => ℝ) (I → ℝ) ℝ where
  prior := A.prior
  prob_prior := A.prob_prior
  allocationRule := A.allocationRule
  paymentRule := A.paymentRule

def BayesianSingleItemAuction.RespectsSingleItemCapacity EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem
The allocation rule respects the single-item probability budget.
```
def RespectsSingleItemCapacity [Fintype I] (A : BayesianSingleItemAuction I) : Prop :=
  ∀ t : ∀ _ : I, ℝ, (∑ i, A.allocationRule t i) ≤ 1
```

def BayesianSingleItemAuction.IsFeasible EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

def IsFeasible [Fintype I] (A : BayesianSingleItemAuction I) : Prop :=
  A.IsAllocFeasible ∧ A.RespectsSingleItemCapacity

def BayesianSingleItemAuction.typeDensity EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

noncomputable def typeDensity (A : BayesianSingleItemAuction I) (i : I) : ℝ → ℝ :=
  deriv (A.typeData.cdf i).cdf

def BayesianSingleItemAuction.typeMeasure EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

Type measure generated by `fᵢ` on `[0, ωᵢ]`.

noncomputable def typeMeasure (A : BayesianSingleItemAuction I) (i : I) : Measure ℝ :=
  (volume.restrict (Set.Ioc 0 (A.typeData.omega i))).withDensity
    fun v => ENNReal.ofReal (A.typeDensity i v)

def BayesianSingleItemAuction.jointDensity EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

noncomputable def jointDensity [Fintype I] (A : BayesianSingleItemAuction I)
    (t : ∀ _ : I, ℝ) : ℝ :=
  Finset.univ.prod fun i => A.typeDensity i (t i)

def BayesianSingleItemAuction.productPrior EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

Product type prior.

noncomputable def productPrior [Fintype I] (A : BayesianSingleItemAuction I) :
    Measure (∀ _ : I, ℝ) :=
  Measure.pi fun i => A.typeMeasure i

def BayesianSingleItemAuction.opponentProductPrior EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

Product prior over `i`'s opponents.

noncomputable def opponentProductPrior [Fintype I] [DecidableEq I]
    (A : BayesianSingleItemAuction I) (i : I) : Measure (OpponentTypeProfile I i) :=
  Measure.pi fun j : {j // j ≠ i} => A.typeMeasure j

def BayesianSingleItemAuction.HasIndependentTypePriors EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.BayesianSingleItem

Stored priors are the product priors.

def HasIndependentTypePriors [Fintype I] [DecidableEq I]
    (A : BayesianSingleItemAuction I) : Prop :=
  A.prior = A.productPrior ∧
    ∀ i : I, A.opponentPrior i = A.opponentProductPrior i

Modules: EconCSLib.MechanismDesign.Auction.BayesianSingleItem

Bayesian Single-Item Auction Framework

This node bundles the data definitions used to model a sealed-bid single-item auction in an incomplete-information environment as a direct Bayesian mechanism with transfers ([[mechanism_design.bayesian.bayesian_mechanisms]]).

Continuous private-value data

TypeCDF (ω : ℝ) records a one-dimensional scalar type distribution on the support interval [0, ω]: a CDF F : ℝ → ℝ that is monotone on the support and continuously differentiable on the open interval (0, ω), with normalisation F(0) = 0 and F(ω) = 1.
ContinuousTypeProfile I records a per-agent upper bound ωᵢ and CDF Fᵢ : TypeCDF (ωᵢ). This is the data structure used to attach Myerson-style regularity assumptions to a Bayesian auction without forcing them into the abstract mechanism layer.

Opponent profiles

OpponentTypeProfile I i is the function space {j // j ≠ i} → ℝ of type reports for everyone except agent i.
profileInsert i z_i glues an opponent profile t₋ᵢ together with agent i's report z_i to recover a full report profile (∀ _ : I, ℝ).

These objects support the interim viewpoint: fixing agent i's report and integrating over opponents' types.

Auction structure

A BayesianSingleItemAuction I extends SingleParameterMechanism I ℝ ([[mechanism_design.transfer.single_parameter_transfer_layer]]) with Bayesian environment data:

prior : Measure (∀ _ : I, ℝ) — the common-knowledge prior on full type profiles, registered as a probability measure.
opponentPrior : (i : I) → Measure (OpponentTypeProfile I i) — explicit per-agent opponent marginals, used to define interim expectations without committing to an independence assumption at the level of measures.
typeData : ContinuousTypeProfile I — the per-agent CDFs and supports for Myerson-style analysis.

The reuse pattern is:

allocationRule t i : ℝ — agent i's winning probability at report profile t, inherited from the single-parameter mechanism.
paymentRule t i : ℝ — agent i's payment at report profile t.
toDirectBayesianMechanismWithTransfers exposes the auction as a DirectBayesianMechanismWithTransfers I (fun _ => ℝ) (I → ℝ) ℝ, so Bayesian ex-ante / interim machinery from ([[mechanism_design.bayesian.bayesian_mechanisms]]) applies.

Feasibility

For probabilistic single-item allocation, two constraints matter:

IsAllocFeasible (inherited): every allocationRule t i lies in [0, 1].
RespectsSingleItemCapacity: for every report profile, $\sum_i x_i(t) \le 1$ — at most one item is allocated in expectation.
IsFeasible is the conjunction.

Density layer (assuming independence)

When the prior is independent across agents, typeDensity i returns the derivative of Fᵢ, and jointDensity t = ∏ᵢ fᵢ(tᵢ) is the product density. These are convenience helpers for density-based analysis; the core mechanism layer does not require independence.

Product priors

productPrior and opponentProductPrior build the full type prior and opponent priors from the one-dimensional density-induced measures. The predicate HasIndependentTypePriors records when the auction's stored priors are exactly these product priors.

Position in the library

The single-parameter Myerson payment identity ([[mechanism_design.myerson.payment_formula]]) and the ex-ante revelation principle ([[mechanism_design.bayesian.ex_ante_revelation_principle]]) both apply to instances of this framework. Concrete IPV models such as the symmetric first-price equilibrium and Myerson's optimal auction are tracked separately ([[mechanism_design.auction.bayesian.symmetric_first_price_equilibrium]], [[mechanism_design.myerson.optimal_auction]]).

References

[MFoGT, Chapter 12, Section 12.1] Maschler, Solan, and Zamir, Game Theory. IPV setting for single-object auctions.
[Krishna, Chapters 2–3] Vijay Krishna, Auction Theory, 2nd ed.. Continuous-type private-value model with CDFs and densities.
[AGT, Chapter 9, Section 9.5] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. Single-parameter Bayesian mechanism design.