EconCSLib.MechanismDesign.Auction.AuctionBasic

Basic auction and mechanism definitions used across the library.

This is the base layer for EconCSLib/MechanismDesign/Auction. It provides:

• abstract auction formats: SingleItemAuction, CombinatorialAuction, and the transfer-layer SingleParameterMechanism
• generic predicates such as feasibility, monotonicity, DSIC, and implementability
• ordered-bid helper constructions such as Auction.maxBid and Auction.argmaxBid

Myerson-specific payment formulas and proofs are in EconCSLib/MechanismDesign/Auction/Myerson.lean.

Auction format hierarchy

Different auction formats arise by specializing the report/type space, allocation space, and payment space:

MechanismWithTransfers I T A P                     -- general transfer mechanism
  ├─ SingleItemAuction I V P                        -- T i = V, A = Option I
  └─ SingleParameterMechanism I R                   -- T i = R, A = I → R, P = R

MultipleParameterMechanism I A V P                  -- T i = A → V
  └─ CombinatorialAuction I k V P                   -- A = CombinatorialAllocation I k

Main definitions

Auction formats

• SingleItemAuction — one indivisible item; allocation is Option I (winner or no sale)
• CombinatorialAuction — k distinct items; allocation assigns item bundles per agent
• SingleParameterMechanism — Myerson's single-parameter setting, defined in MechanismDesign.Auction.Transfer

Predicates on auction formats

• CombinatorialAuction.IsFeasible — no item allocated to two agents
• SingleParameterMechanism.IsAllocFeasible — allocations lie in [0, 1]
• SingleParameterMechanism.IsMonotone — allocation is non-decreasing in each agent's reported type (Myerson's necessary condition for DSIC)

Bid-profile support predicates (Auction.BidProfile)

• Auction.BidProfile.Nonnegative — every bid is nonnegative
• Auction.BidProfile.InSet — each bid lies in a per-agent admissible set
• Auction.BidProfile.InBox — each bid lies in a per-agent closed interval
• Auction.BidProfile.StrategyMapsBoxToBox — a strategy maps one bid box into another
• Auction.BidProfile.inBox_iff_inSet_Icc — InBox ↔ InSet with Set.Icc

Ordered-bid utilities

The following are mathematical tools for auction rules that rank bids. They do not define any specific auction's winner — each concrete auction specifies its own allocation rule, which may or may not select the highest bidder.

• Auction.maxBid — the highest bid in a profile
• Auction.argmaxBid — the bidder with the highest bid
• Auction.maxBidExcluding — the highest bid excluding a given bidder

References

• [Nisan et al., Algorithmic Game Theory, Ch. 9, 11]
• [Maschler, Solan, Zamir, Game Theory, Ch. 11–12]

Abstract auction formats

structure SingleItemAuction (I : Type u_1) (V : Type u_2) (P : Type u_3) extends MechanismWithTransfers I (fun (x : I) => V) (Option I) P : Type (max (max u_1 u_2) u_3)

A single-item auction.

One indivisible item is for sale. Each agent reports a scalar bid of type V. The allocation is Option I:

• some i — bidder i receives the item
• none — the item is withheld (reserve price not met, etc.)

Which bidder wins, or whether anyone wins, is determined by the allocation rule of the specific mechanism. This structure imposes no winner-selection policy.

• allocationRule : (I → V) → Option I
• paymentRule : (I → V) → I → P

def MultiItemBundle (k : ℕ) : Type

A multi-item auction with k distinct items.

An agent bundle is a finite subset of the k items, represented as Finset (Fin k). A full allocation assigns one bundle to each agent. Agents report valuation functions over full allocation profiles, so this is the specialization of MultipleParameterMechanism to bundle allocations.

Feasibility (no item sold twice) is a separate predicate; see IsFeasible.

Equations

• MultiItemBundle k = Finset (Fin k)

def MultiItemBundle.toFinset {k : ℕ} (bundle : MultiItemBundle k) : Finset (Fin k)

View a named multi-item bundle as the underlying finite set of item indices.

Equations

• bundle.toFinset = bundle

def CombinatorialAllocation (I : Type u_1) (k : ℕ) : Type u_1

A multi-item allocation assigns each agent a bundle of items.

Equations

• CombinatorialAllocation I k = (I → MultiItemBundle k)

structure CombinatorialAuction (I : Type u_1) (k : ℕ) (V : Type u_2) (P : Type u_3) extends MultipleParameterMechanism I (CombinatorialAllocation I k) V P : Type (max (max u_1 u_2) u_3)

A combinatorial auction with k distinct items.

This is a multiple-parameter mechanism whose allocation space is the type of bundle-allocation profiles I → Finset (Fin k). Each agent reports a valuation over those allocation profiles.

• allocationRule : (I → CombinatorialAllocation I k → V) → CombinatorialAllocation I k
• paymentRule : (I → CombinatorialAllocation I k → V) → I → P

def CombinatorialAuction.IsFeasible {I : Type u_1} {k : ℕ} {V : Type u_2} {P : Type u_3} (M : CombinatorialAuction I k V P) : Prop

Feasibility: each item is allocated to at most one agent.

Equations

• One or more equations did not get rendered due to their size.

Bid-profile support predicates

Side conditions on bid profiles that constrain the admissible bid space without modifying the underlying auction format. Useful for bounded-support equilibrium arguments and strategy-set restrictions in Bayesian auction theory.

[Krishna, Ch. 2-3]; [AGT, Ch. 9, §9.3-9.5]

def Auction.BidProfile.Nonnegative {I : Type u_1} {V : Type u_2} [Zero V] [LE V] (b : I → V) : Prop

Every bid is nonnegative.

$\forall i.\; b_i \ge 0$. Captures the standard private-value convention that bids represent willingness-to-pay.

Equations

• Auction.BidProfile.Nonnegative b = ∀ (i : I), 0 ≤ b i

def Auction.BidProfile.InSet {I : Type u_1} {V : Type u_2} (b : I → V) (S : I → Set V) : Prop

Each bid lies in the per-agent admissible set.

For a family of strategy sets $S_i \subseteq V$, asserts $\forall i.\; b_i \in S_i$. Captures heterogeneous strategy spaces.

Equations

• Auction.BidProfile.InSet b S = ∀ (i : I), b i ∈ S i

def Auction.BidProfile.InBox {I : Type u_1} {V : Type u_2} [LE V] (b ℓ u : I → V) : Prop

Each bid lies in the per-agent box $[\ell_i, u_i]$.

$\forall i.\; \ell_i \le b_i \le u_i$.

Equations

• Auction.BidProfile.InBox b ℓ u = ∀ (i : I), ℓ i ≤ b i ∧ b i ≤ u i

def Auction.BidProfile.StrategyMapsBoxToBox {V : Type u_2} [LE V] (σ : V → V) (ℓ u ℓ' u' : V) : Prop

A scalar strategy maps the input bid interval $[\ell, u]$ into $[\ell', u']$.

Captures Lipschitz/contraction conditions for best-response dynamics in bounded auctions.

Equations

• Auction.BidProfile.StrategyMapsBoxToBox σ ℓ u ℓ' u' = ∀ (v : V), ℓ ≤ v ∧ v ≤ u → ℓ' ≤ σ v ∧ σ v ≤ u'

theorem Auction.BidProfile.inBox_iff_inSet_Icc {I : Type u_1} {V : Type u_2} [Preorder V] (b ℓ u : I → V) : InBox b ℓ u ↔ InSet b fun (i : I) => Set.Icc (ℓ i) (u i)

InBox b ℓ u is equivalent to InSet b (fun i => Set.Icc (ℓ i) (u i)).

Makes box-constrained bid spaces interoperable with the Mathlib Set.Icc API (continuity, compactness, integration).

Ordered-bid utilities

The following definitions apply when bids are linearly ordered (e.g., scalar bids in ℝ). They are mathematical tools for computing bid maxima and argmaxes — they do not define any particular auction's winner or allocation rule.

Each concrete auction explicitly states whether it uses these utilities and how.

def Auction.maxBid {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) : V

The highest bid in a profile.

Equations

• Auction.maxBid b = Finset.univ.sup' ⋯ b

theorem Auction.exists_maxBid {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) : ∃ (i : I), b i = maxBid b

There exists a bidder whose bid equals the highest bid.

noncomputable def Auction.argmaxBid {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) : I

The bidder whose bid achieves the maximum.

This is a mathematical argmax, not a declaration that any auction's winner is the highest bidder. Concrete auctions define their own allocation/winner rules.

Equations

• Auction.argmaxBid b = Classical.choose ⋯

theorem Auction.argmaxBid_eq_maxBid {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) : b (argmaxBid b) = maxBid b

The argmax bidder's bid equals the highest bid.

theorem Auction.bid_le_maxBid {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) (j : I) : b j ≤ b (argmaxBid b)

Every bid is at most the argmax bidder's bid.

theorem Auction.eq_argmaxBid_of_strict_max {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) (i : I) (h : ∀ (j : I), j ≠ i → b j < b i) : i = argmaxBid b

If i strictly outbids all others, then i is the argmax bidder.

noncomputable def Auction.maxBidExcluding {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) [DecidableEq I] (i : I) : V

The highest bid excluding bidder i.

Equations

• Auction.maxBidExcluding b i = (Finset.univ.erase i).sup' ⋯ b

theorem Auction.maxBidExcluding_le_maxBid {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) [DecidableEq I] (i : I) : maxBidExcluding b i ≤ maxBid b

Excluding any bidder can only decrease the highest bid.

theorem Auction.maxBidExcluding_eq_maxBid_of_not_argmax {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) [DecidableEq I] {i : I} (h : i ≠ argmaxBid b) : maxBidExcluding b i = maxBid b

If i is not the argmax bidder, excluding i does not change the highest bid.

theorem Auction.maxBidExcluding_le_argmaxBid_bid {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) [DecidableEq I] : maxBidExcluding b (argmaxBid b) ≤ b (argmaxBid b)

The argmax bidder's bid is at least the highest bid among all others.

theorem Auction.maxBidExcluding_update_self {I : Type u_1} [Fintype I] [Nontrivial I] {V : Type u_2} [LinearOrder V] (b : I → V) [DecidableEq I] (i : I) (bi : V) : maxBidExcluding (Function.update b i bi) i = maxBidExcluding b i

Changing i's bid does not affect the highest bid among the others.