Lean declarations

def BayesianSingleItemAuction.virtualValue EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem
Myerson virtual value `v - (1 - F_i(v)) / f_i(v)` for bidder `i`.
```
noncomputable def virtualValue (A : BayesianSingleItemAuction I) (i : I) (v : ℝ) : ℝ :=
  v - (1 - (A.typeData.cdf i).cdf v) / A.typeDensity i v
```
def BayesianSingleItemAuction.IsRegular EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem
Regularity: every bidder's virtual value is monotone.
```
def IsRegular (A : BayesianSingleItemAuction I) : Prop :=
  ∀ i : I, Monotone (A.virtualValue i)
```

def BayesianSingleItemAuction.IsReserveThreshold EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem

A reserve threshold separating nonpositive and nonnegative virtual values.

def IsReserveThreshold (A : BayesianSingleItemAuction I) (i : I) (reserve : ℝ) : Prop :=
  (∀ v, v < reserve → A.virtualValue i v ≤ 0) ∧
    ∀ v, reserve ≤ v → 0 ≤ A.virtualValue i v

theorem BayesianSingleItemAuction.measurable_virtualValue_of_isRegular EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem

theorem measurable_virtualValue_of_isRegular
    (A : BayesianSingleItemAuction I) (hA : A.IsRegular) (i : I) :
    Measurable (A.virtualValue i)

theorem BayesianSingleItemAuction.isReserveThreshold_of_isRegular_of_virtualValue_eq_zero EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem

A zero of a regular virtual value is a reserve threshold.

theorem isReserveThreshold_of_isRegular_of_virtualValue_eq_zero
    (A : BayesianSingleItemAuction I) (hA : A.IsRegular) {i : I} {reserve : ℝ}
    (hzero : A.virtualValue i reserve = 0) :
    A.IsReserveThreshold i reserve

Modules: EconCSLib.MechanismDesign.Auction.OptimalSingleItem

Virtual Values and Regularity

For a Bayesian single-item auction ([[mechanism_design.auction.bayesian.single_item_framework]]), the Myerson virtual value of bidder \(i\) at type \(v\) is \[ \psi_i(v) = v - \frac{1 - F_i(v)}{f_i(v)}. \]

In Lean this is virtualValue A i v, using the CDF stored in A.typeData and the density A.typeDensity i.

Regularity

IsRegular A states that each function \(v \mapsto \psi_i(v)\) is monotone. Regularity is the condition that makes the virtual-surplus-maximizing allocation rule monotone in each bidder's own report, which is the bridge to DSIC via the Myerson monotonicity characterization ([[mechanism_design.myerson.monotonicity_characterization]]).

Reserve thresholds

IsReserveThreshold A i rho records that rho separates nonpositive and nonnegative virtual values for bidder \(i\). If the virtual value is regular and \(\psi_i(\rho)=0\), then rho is a reserve threshold. These threshold lemmas are used to interpret the optimal allocation rule as selling only above reserve values, and support the reserve-price node [[mechanism_design.myerson.reserve_price]].

References

[MSZ, Chapter 12, Section 12.10] Maschler, Solan, and Zamir, Game Theory.
[Myerson 1981] Roger Myerson, "Optimal Auction Design", Mathematics of Operations Research 6(1):58-73.
[Krishna, Chapter 5] Vijay Krishna, Auction Theory, 2nd ed..

Virtual Values and Regularity

Regularity

Reserve thresholds

References

Used by

Also in