Lean declarations

def BayesianSingleItemAuction.virtualSurplus EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem
Virtual surplus of an allocation rule at a reported type profile.
```
noncomputable def virtualSurplus [Fintype I]
    (A : BayesianSingleItemAuction I) (x : (I → ℝ) → I → ℝ) (b : I → ℝ) : ℝ :=
  ∑ i, x b i * A.virtualValue i (b i)
```
def BayesianSingleItemAuction.expectedVirtualSurplus EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem
Ex-ante expected virtual surplus under the auction prior.
```
noncomputable def expectedVirtualSurplus [Fintype I]
    (A : BayesianSingleItemAuction I) (x : (I → ℝ) → I → ℝ) : ℝ :=
  ∫ t, A.virtualSurplus x t ∂A.prior
```
def BayesianSingleItemAuction.IntegrableVirtualSurplus EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem
Integrability condition for ex-ante virtual surplus under the auction prior.
```
def IntegrableVirtualSurplus [Fintype I]
    (A : BayesianSingleItemAuction I) (x : (I → ℝ) → I → ℝ) : Prop :=
  Integrable (fun t => A.virtualSurplus x t) A.prior
```
def BayesianSingleItemAuction.IsSingleItemAllocationRule EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem
A nonnegative fractional allocation rule with total mass at most `1`.
```
def IsSingleItemAllocationRule [Fintype I]
    (x : (I → ℝ) → I → ℝ) : Prop :=
  (∀ b i, 0 ≤ x b i) ∧ ∀ b, (∑ i, x b i) ≤ 1
```

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

Feasible allocation rules that pointwise maximize virtual surplus.

def IsVirtualSurplusOptimalAllocationRule [Fintype I]
    (A : BayesianSingleItemAuction I) (x : (I → ℝ) → I → ℝ) : Prop :=
  IsSingleItemAllocationRule x ∧
    ∀ y, IsSingleItemAllocationRule y →
      ∀ b, A.virtualSurplus y b ≤ A.virtualSurplus x b

def BayesianSingleItemAuction.virtualScore EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem
Lexicographic score used to break ties among virtual values.
```
noncomputable def virtualScore [LinearOrder I]
    (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : ℝ ×ₗ I :=
  toLex (A.virtualValue i (b i), i)
```

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

The virtual-value winner with deterministic tie-breaking.

noncomputable def virtualSurplusMaximizingWinner
    [Fintype I] [Nontrivial I] [LinearOrder I]
    (A : BayesianSingleItemAuction I) (b : I → ℝ) : I :=
  Auction.argmaxBid (A.virtualScore b)

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

The virtual value attained by the selected virtual-value winner.

noncomputable def winningVirtualValue
    [Fintype I] [Nontrivial I] [LinearOrder I]
    (A : BayesianSingleItemAuction I) (b : I → ℝ) : ℝ :=
  A.virtualValue (A.virtualSurplusMaximizingWinner b)
    (b (A.virtualSurplusMaximizingWinner b))

def BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.OptimalSingleItem
Allocates to the highest positive virtual value, otherwise withholds the item.
```
noncomputable def virtualSurplusMaximizingAllocationRule
    [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I]
    (A : BayesianSingleItemAuction I) : (I → ℝ) → I → ℝ
```

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

The virtual-surplus-maximizing allocation rule is feasible.

theorem virtualSurplusMaximizingAllocationRule_isSingleItemAllocationRule
    [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I]
    (A : BayesianSingleItemAuction I) :
    IsSingleItemAllocationRule A.virtualSurplusMaximizingAllocationRule

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

theorem virtualSurplusMaximizingAllocationRule_isVirtualSurplusOptimalAllocationRule
    [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I]
    (A : BayesianSingleItemAuction I) :
    A.IsVirtualSurplusOptimalAllocationRule A.virtualSurplusMaximizingAllocationRule

Modules: EconCSLib.MechanismDesign.Auction.OptimalSingleItem

Virtual-Surplus-Maximizing Allocation

The virtual-surplus objective for a single-item allocation rule \(x\) is \[ \sum_i x_i(t)\,\psi_i(t_i), \] where \(\psi_i\) is bidder \(i\)'s virtual value ([[mechanism_design.myerson.virtual_value_regularity]]).

Allocation rule

virtualSurplusMaximizingAllocationRule A chooses a bidder with maximal virtual value when the winning virtual value is positive. If every virtual value is nonpositive, the allocation rule assigns probability zero to every bidder, so the item is withheld.

Tie-breaking is deterministic: virtualScore pairs each virtual value with the bidder index in lexicographic order, and virtualSurplusMaximizingWinner uses the existing finite argmax utilities from the auction layer.

Formal properties

The formalization proves that this rule is a feasible single-item allocation: allocation probabilities are nonnegative and the total allocation probability is at most one. It also proves pointwise virtual-surplus optimality among all feasible single-item allocation rules.

These pointwise facts lift to ex-ante expected virtual-surplus comparisons under the corresponding integrability assumptions, and become the allocation part of the regular Myerson optimal auction theorem [[mechanism_design.myerson.optimal_auction]].

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.
[AGT, Chapter 13] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory.

Used by

Regular Myerson Optimal Single-Item Auction

Virtual-Surplus-Maximizing Allocation

Allocation rule

Formal properties

References

Used by

Also in