EconCSLib.MechanismDesign.Auction.OptimalSingleItem

Regular Myerson optimal single-item auctions.

This file defines virtual values, the virtual-surplus-maximizing allocation rule, its Myerson payment rule, and the IC/IR revenue-optimality interface for MSZ 12.59. The main public result is virtualSurplusMaximizingAuction_regularMyersonOptimalICIR_of_isRegular.

Structure hierarchy

BayesianSingleItemAuction I                       -- direct Bayesian single-item layer
  ├─ virtualSurplusMaximizingMechanism            -- SingleParameterMechanism view
  └─ virtualSurplusMaximizingAuction              -- BayesianSingleItemAuction view

SingleParameterMechanism.withMyersonPayment       -- payment formula used by the optimizer

Main definitions

• virtualValue, IsRegular, IsReserveThreshold
• virtualSurplus, expectedVirtualSurplus
• IsSingleItemAllocationRule, IsVirtualSurplusOptimalAllocationRule
• IsFeasibleICIRIntegrable
• InterimFubiniAnalyticAssumptions
• RegularMyersonICIRAnalyticAssumptions
• IsRegularMyersonOptimalICIRAuction
• virtualSurplusMaximizingAllocationRule
• virtualSurplusMaximizingPaymentRule, virtualSurplusMaximizingMechanism, virtualSurplusMaximizingAuction

Main proofs

• reserve-threshold and sale/no-sale behavior
• feasibility and pointwise virtual-surplus optimality
• expected virtual-surplus monotonicity
• monotonicity and DSIC via MechanismDesign.Auction.Myerson
• bridge from ex-post DSIC to interim IC, plus conditional interim IR
• virtualSurplusMaximizingAuction_regularMyersonOptimalICIR_of_isRegular

References:

• Maschler, Solan, Zamir, Game Theory, Section 12.10.
• Nisan, Roughgarden, Tardos, Vazirani, Algorithmic Game Theory, Chapter 13.

Virtual values and regularity

noncomputable def BayesianSingleItemAuction.virtualValue {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (v : ℝ) : ℝ

Myerson virtual value v - (1 - F_i(v)) / f_i(v) for bidder i.

Equations

• A.virtualValue i v = v - (1 - (A.typeData.cdf i).cdf v) / A.typeDensity i v

def BayesianSingleItemAuction.IsRegular {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Regularity: every bidder's virtual value is monotone.

Equations

• A.IsRegular = ∀ (i : I), Monotone (A.virtualValue i)

theorem BayesianSingleItemAuction.measurable_virtualValue_of_isRegular {I : Type u_1} (A : BayesianSingleItemAuction I) (hA : A.IsRegular) (i : I) : Measurable (A.virtualValue i)

Regular virtual values are measurable by Mathlib's measurability theorem for monotone real functions.

def BayesianSingleItemAuction.IsReserveThreshold {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (reserve : ℝ) : Prop

A reserve threshold separating nonpositive and nonnegative virtual values.

Equations

• A.IsReserveThreshold i reserve = ((∀ v < reserve, A.virtualValue i v ≤ 0) ∧ ∀ (v : ℝ), reserve ≤ v → 0 ≤ A.virtualValue i v)

theorem BayesianSingleItemAuction.virtualValue_nonneg_of_isReserveThreshold {I : Type u_1} (A : BayesianSingleItemAuction I) {i : I} {reserve v : ℝ} (hreserve : A.IsReserveThreshold i reserve) (hv : reserve ≤ v) : 0 ≤ A.virtualValue i v

At a reserve threshold, the virtual value is nonnegative.

theorem BayesianSingleItemAuction.virtualValue_nonpos_of_lt_isReserveThreshold {I : Type u_1} (A : BayesianSingleItemAuction I) {i : I} {reserve v : ℝ} (hreserve : A.IsReserveThreshold i reserve) (hv : v < reserve) : A.virtualValue i v ≤ 0

Below a reserve threshold, the virtual value is nonpositive.

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

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

noncomputable def BayesianSingleItemAuction.virtualSurplus {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (x : (I → ℝ) → I → ℝ) (b : I → ℝ) : ℝ

Virtual surplus of an allocation rule at a reported type profile.

Equations

• A.virtualSurplus x b = ∑ i : I, x b i * A.virtualValue i (b i)

noncomputable def BayesianSingleItemAuction.expectedVirtualSurplus {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (x : (I → ℝ) → I → ℝ) : ℝ

Ex-ante expected virtual surplus under the auction prior.

Equations

• A.expectedVirtualSurplus x = ∫ (t : I → ℝ), A.virtualSurplus x t ∂A.prior

def BayesianSingleItemAuction.IntegrableVirtualSurplus {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (x : (I → ℝ) → I → ℝ) : Prop

Integrability condition for ex-ante virtual surplus under the auction prior.

Equations

• A.IntegrableVirtualSurplus x = MeasureTheory.Integrable (fun (t : I → ℝ) => A.virtualSurplus x t) A.prior

theorem BayesianSingleItemAuction.expectedVirtualSurplus_le_of_forall_virtualSurplus_le {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) {x y : (I → ℝ) → I → ℝ} (hx_int : A.IntegrableVirtualSurplus x) (hy_int : A.IntegrableVirtualSurplus y) (hxy : ∀ (t : I → ℝ), A.virtualSurplus x t ≤ A.virtualSurplus y t) : A.expectedVirtualSurplus x ≤ A.expectedVirtualSurplus y

Pointwise virtual-surplus dominance lifts to ex-ante dominance.

def BayesianSingleItemAuction.IsSingleItemAllocationRule {I : Type u_1} [Fintype I] (x : (I → ℝ) → I → ℝ) : Prop

A nonnegative fractional allocation rule with total mass at most 1.

Equations

• BayesianSingleItemAuction.IsSingleItemAllocationRule x = ((∀ (b : I → ℝ) (i : I), 0 ≤ x b i) ∧ ∀ (b : I → ℝ), ∑ i : I, x b i ≤ 1)

theorem BayesianSingleItemAuction.IsSingleItemAllocationRule.le_one {I : Type u_1} [Fintype I] [DecidableEq I] {x : (I → ℝ) → I → ℝ} (hx : IsSingleItemAllocationRule x) (b : I → ℝ) (i : I) : x b i ≤ 1

A feasible single-item allocation gives each bidder probability at most 1.

theorem BayesianSingleItemAuction.withPayment_isAllocFeasible_of_isSingleItemAllocationRule {I : Type u_1} [Fintype I] [DecidableEq I] {x p : (I → ℝ) → I → ℝ} (hx : IsSingleItemAllocationRule x) : { allocationRule := x, paymentRule := p }.IsAllocFeasible

A feasible single-item allocation rule satisfies IsAllocFeasible with any payment rule.

def BayesianSingleItemAuction.IsVirtualSurplusOptimalAllocationRule {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (x : (I → ℝ) → I → ℝ) : Prop

Feasible allocation rules that pointwise maximize virtual surplus.

Equations

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

Deterministic virtual-surplus maximization

noncomputable def BayesianSingleItemAuction.virtualScore {I : Type u_1} [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : Lex (ℝ × I)

Lexicographic score used to break ties among virtual values.

Equations

• A.virtualScore b i = toLex (A.virtualValue i (b i), i)

noncomputable def BayesianSingleItemAuction.virtualSurplusMaximizingWinner {I : Type u_1} [Fintype I] [Nontrivial I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) : I

The virtual-value winner with deterministic tie-breaking.

Equations

• A.virtualSurplusMaximizingWinner b = Auction.argmaxBid (A.virtualScore b)

theorem BayesianSingleItemAuction.virtualSurplusMaximizingWinner_eq_iff_forall_virtualScore_le {I : Type u_1} [Fintype I] [Nontrivial I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : A.virtualSurplusMaximizingWinner b = i ↔ ∀ (j : I), A.virtualScore b j ≤ A.virtualScore b i

The selected winner is exactly the bidder whose lexicographic virtual score dominates every other bidder's score.

noncomputable def BayesianSingleItemAuction.winningVirtualValue {I : Type u_1} [Fintype I] [Nontrivial I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) : ℝ

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

Equations

• A.winningVirtualValue b = A.virtualValue (A.virtualSurplusMaximizingWinner b) (b (A.virtualSurplusMaximizingWinner b))

noncomputable def BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : (I → ℝ) → I → ℝ

Allocates to the highest positive virtual value, otherwise withholds the item.

Equations

• A.virtualSurplusMaximizingAllocationRule b i = if 0 < A.winningVirtualValue b then if i = A.virtualSurplusMaximizingWinner b then 1 else 0 else 0

noncomputable def BayesianSingleItemAuction.virtualSurplusMaximizingPaymentRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : (I → ℝ) → I → ℝ

Myerson payment for virtualSurplusMaximizingAllocationRule.

Equations

• A.virtualSurplusMaximizingPaymentRule = SingleParameterMechanism.myersonPayment A.virtualSurplusMaximizingAllocationRule

noncomputable def BayesianSingleItemAuction.virtualSurplusMaximizingMechanism {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : SingleParameterMechanism I ℝ

The virtual-surplus allocation rule paired with its Myerson payment.

Equations

• A.virtualSurplusMaximizingMechanism = { allocationRule := A.virtualSurplusMaximizingAllocationRule, paymentRule := A.virtualSurplusMaximizingPaymentRule }

noncomputable def BayesianSingleItemAuction.virtualSurplusMaximizingAuction {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : BayesianSingleItemAuction I

The Bayesian auction using the virtual-surplus mechanism and the original priors.

Equations

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

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingMechanism_allocationRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingMechanism.allocationRule = A.virtualSurplusMaximizingAllocationRule

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingMechanism_paymentRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingMechanism.paymentRule = A.virtualSurplusMaximizingPaymentRule

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_allocationRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.allocationRule = A.virtualSurplusMaximizingAllocationRule

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_paymentRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.paymentRule = A.virtualSurplusMaximizingPaymentRule

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_prior {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.prior = A.prior

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_opponentPrior {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.opponentPrior = A.opponentPrior

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_typeData {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.typeData = A.typeData

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_toSingleParameterMechanism {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.toSingleParameterMechanism = A.virtualSurplusMaximizingMechanism

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_toDirectBayesianMechanismWithTransfers {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.toDirectBayesianMechanismWithTransfers = { prior := A.prior, prob_prior := ⋯, allocationRule := A.virtualSurplusMaximizingMechanism.allocationRule, paymentRule := A.virtualSurplusMaximizingMechanism.paymentRule }

Allocation-rule facts and virtual-surplus maximality

theorem BayesianSingleItemAuction.virtualSurplusMaximizingWinner_virtualValue_ge {I : Type u_1} [Fintype I] [Nontrivial I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : A.virtualValue i (b i) ≤ A.winningVirtualValue b

The selected winner has maximal virtual value.

theorem BayesianSingleItemAuction.virtualSurplus_le_virtualSurplusMaximizingAllocationRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {x : (I → ℝ) → I → ℝ} {b : I → ℝ} (hx_nonneg : ∀ (i : I), 0 ≤ x b i) (hx_capacity : ∑ i : I, x b i ≤ 1) : A.virtualSurplus x b ≤ A.virtualSurplus A.virtualSurplusMaximizingAllocationRule b

Pointwise virtual-surplus maximality.

Reserve-price interpretation of the allocation rule

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_eq_winnerIndicator_of_winningVirtualValue_pos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (hpos : 0 < A.winningVirtualValue b) : A.virtualSurplusMaximizingAllocationRule b = fun (i : I) => if i = A.virtualSurplusMaximizingWinner b then 1 else 0

If the winning virtual value is positive, allocate to the selected winner.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_winner_eq_one_of_winningVirtualValue_pos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (hpos : 0 < A.winningVirtualValue b) : A.virtualSurplusMaximizingAllocationRule b (A.virtualSurplusMaximizingWinner b) = 1

If the winning virtual value is positive, the selected winner receives 1.

theorem BayesianSingleItemAuction.winningVirtualValue_pos_iff_exists_virtualValue_pos {I : Type u_1} [Fintype I] [Nontrivial I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) : 0 < A.winningVirtualValue b ↔ ∃ (i : I), 0 < A.virtualValue i (b i)

The winning virtual value is positive iff some virtual value is positive.

theorem BayesianSingleItemAuction.winningVirtualValue_nonpos_iff_forall_virtualValue_nonpos {I : Type u_1} [Fintype I] [Nontrivial I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) : A.winningVirtualValue b ≤ 0 ↔ ∀ (i : I), A.virtualValue i (b i) ≤ 0

The winning virtual value is nonpositive iff all virtual values are.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_eq_one_iff {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : A.virtualSurplusMaximizingAllocationRule b i = 1 ↔ 0 < A.winningVirtualValue b ∧ i = A.virtualSurplusMaximizingWinner b

Allocation probability 1 characterizes the positive virtual-value winner.

theorem BayesianSingleItemAuction.virtualValue_pos_of_virtualSurplusMaximizingAllocationRule_eq_one {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {b : I → ℝ} {i : I} (hi : A.virtualSurplusMaximizingAllocationRule b i = 1) : 0 < A.virtualValue i (b i)

A bidder allocated probability 1 has positive virtual value.

theorem BayesianSingleItemAuction.reserveThreshold_le_bid_of_virtualSurplusMaximizingAllocationRule_eq_one {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {b : I → ℝ} {i : I} {reserve : ℝ} (hreserve : A.IsReserveThreshold i reserve) (hi : A.virtualSurplusMaximizingAllocationRule b i = 1) : reserve ≤ b i

An allocated bidder reports at least her reserve threshold.

theorem BayesianSingleItemAuction.exists_virtualSurplusMaximizingAllocationRule_eq_one_iff_exists_virtualValue_pos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) : (∃ (i : I), A.virtualSurplusMaximizingAllocationRule b i = 1) ↔ ∃ (i : I), 0 < A.virtualValue i (b i)

A sale occurs exactly when some bidder has positive virtual value.

theorem BayesianSingleItemAuction.exists_virtualSurplusMaximizingAllocationRule_eq_one_iff_winningVirtualValue_pos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) : (∃ (i : I), A.virtualSurplusMaximizingAllocationRule b i = 1) ↔ 0 < A.winningVirtualValue b

A sale occurs exactly when the selected virtual value is positive.

theorem BayesianSingleItemAuction.exists_reserveThreshold_le_bid_of_exists_virtualSurplusMaximizingAllocationRule_eq_one {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {reserve b : I → ℝ} (hreserve : ∀ (i : I), A.IsReserveThreshold i (reserve i)) (hsale : ∃ (i : I), A.virtualSurplusMaximizingAllocationRule b i = 1) : ∃ (i : I), reserve i ≤ b i

If a sale occurs, some bidder reaches her reserve threshold.

theorem BayesianSingleItemAuction.reserveThreshold_le_winner_bid_of_winningVirtualValue_pos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {reserve b : I → ℝ} (hreserve : ∀ (i : I), A.IsReserveThreshold i (reserve i)) (hpos : 0 < A.winningVirtualValue b) : reserve (A.virtualSurplusMaximizingWinner b) ≤ b (A.virtualSurplusMaximizingWinner b)

A positive virtual-value winner reaches her reserve threshold.

theorem BayesianSingleItemAuction.exists_reserveThreshold_le_bid_of_winningVirtualValue_pos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {reserve b : I → ℝ} (hreserve : ∀ (i : I), A.IsReserveThreshold i (reserve i)) (hpos : 0 < A.winningVirtualValue b) : ∃ (i : I), reserve i ≤ b i

Positive winning virtual value implies some report reaches reserve.

theorem BayesianSingleItemAuction.winningVirtualValue_nonpos_of_forall_lt_reserveThreshold {I : Type u_1} [Fintype I] [Nontrivial I] [LinearOrder I] (A : BayesianSingleItemAuction I) {reserve b : I → ℝ} (hreserve : ∀ (i : I), A.IsReserveThreshold i (reserve i)) (hb : ∀ (i : I), b i < reserve i) : A.winningVirtualValue b ≤ 0

If all reports are below reserve, the winning virtual value is nonpositive.

theorem BayesianSingleItemAuction.not_forall_lt_reserveThreshold_of_winningVirtualValue_pos {I : Type u_1} [Fintype I] [Nontrivial I] [LinearOrder I] (A : BayesianSingleItemAuction I) {reserve b : I → ℝ} (hreserve : ∀ (i : I), A.IsReserveThreshold i (reserve i)) (hpos : 0 < A.winningVirtualValue b) : ¬∀ (i : I), b i < reserve i

Positive winning virtual value rules out all reports below reserve.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_eq_zero_of_forall_virtualValue_nonpos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {b : I → ℝ} (hnonpos : ∀ (i : I), A.virtualValue i (b i) ≤ 0) : A.virtualSurplusMaximizingAllocationRule b = fun (x : I) => 0

If all virtual values are nonpositive, withhold the item.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_eq_zero_of_forall_lt_reserveThreshold {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {reserve b : I → ℝ} (hreserve : ∀ (i : I), A.IsReserveThreshold i (reserve i)) (hb : ∀ (i : I), b i < reserve i) : A.virtualSurplusMaximizingAllocationRule b = fun (x : I) => 0

If all reports are below reserve thresholds, withhold the item.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_eq_zero_iff_forall_virtualValue_nonpos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {b : I → ℝ} : (A.virtualSurplusMaximizingAllocationRule b = fun (x : I) => 0) ↔ ∀ (i : I), A.virtualValue i (b i) ≤ 0

Withholding is equivalent to all virtual values being nonpositive.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_eq_zero_iff_winningVirtualValue_nonpos {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {b : I → ℝ} : (A.virtualSurplusMaximizingAllocationRule b = fun (x : I) => 0) ↔ A.winningVirtualValue b ≤ 0

Withholding is equivalent to nonpositive winning virtual value.

theorem BayesianSingleItemAuction.virtualSurplus_virtualSurplusMaximizingAllocationRule_eq_max_winningVirtualValue_zero {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) : A.virtualSurplus A.virtualSurplusMaximizingAllocationRule b = max (A.winningVirtualValue b) 0

The constructed virtual surplus is the positive part of the winning virtual value.

Feasibility

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_nonneg {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : 0 ≤ A.virtualSurplusMaximizingAllocationRule b i

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_le_one {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : A.virtualSurplusMaximizingAllocationRule b i ≤ 1

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_respectsSingleItemCapacity {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) : ∑ i : I, A.virtualSurplusMaximizingAllocationRule b i ≤ 1

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

The virtual-surplus-maximizing allocation rule is feasible.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingMechanism_isAllocFeasible {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingMechanism.IsAllocFeasible

The virtual-surplus-maximizing mechanism is allocation-feasible.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isFeasible {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.IsFeasible

The constructed auction is feasible.

theorem BayesianSingleItemAuction.IsFeasible.isSingleItemAllocationRule {I : Type u_1} [Fintype I] {B : BayesianSingleItemAuction I} (hB : B.IsFeasible) : IsSingleItemAllocationRule B.allocationRule

Auction feasibility gives allocation-rule feasibility.

Measurability helpers

Allocation-rule optimality

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

The deterministic virtual-surplus-maximizing allocation rule is feasible and pointwise maximizes virtual surplus among all feasible fractional single-item allocation rules.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingMechanism_allocationRule_isVirtualSurplusOptimal {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.IsVirtualSurplusOptimalAllocationRule A.virtualSurplusMaximizingMechanism.allocationRule

The allocation rule of the Myerson-payment mechanism is virtual-surplus optimal. This exposes the optimal-allocation content at the mechanism layer, while payments continue to be supplied by MechanismDesign.Auction.Myerson.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_allocationRule_isVirtualSurplusOptimal {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.IsVirtualSurplusOptimalAllocationRule A.virtualSurplusMaximizingAuction.allocationRule

The allocation rule of the constructed Bayesian single-item auction is virtual-surplus optimal.

theorem BayesianSingleItemAuction.expectedVirtualSurplus_le_virtualSurplusMaximizingAllocationRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {x : (I → ℝ) → I → ℝ} (hx : IsSingleItemAllocationRule x) (hx_int : A.IntegrableVirtualSurplus x) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAllocationRule) : A.expectedVirtualSurplus x ≤ A.expectedVirtualSurplus A.virtualSurplusMaximizingAllocationRule

Ex-ante virtual-surplus optimality of the deterministic rule, conditional on the explicit integrability assumptions needed by the Bochner integral.

theorem BayesianSingleItemAuction.expectedVirtualSurplus_le_virtualSurplusMaximizingAuction_allocationRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {x : (I → ℝ) → I → ℝ} (hx : IsSingleItemAllocationRule x) (hx_int : A.IntegrableVirtualSurplus x) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule) : A.expectedVirtualSurplus x ≤ A.expectedVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule

The allocation rule of the constructed Bayesian auction is ex-ante virtual-surplus optimal under the same explicit integrability assumptions.

theorem BayesianSingleItemAuction.expectedVirtualSurplus_le_virtualSurplusMaximizingAuction_of_isFeasible {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A B : BayesianSingleItemAuction I) (hB : B.IsFeasible) (hB_int : A.IntegrableVirtualSurplus B.allocationRule) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule) : A.expectedVirtualSurplus B.allocationRule ≤ A.expectedVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule

def BayesianSingleItemAuction.IsZeroNormalized {I : Type u_1} [DecidableEq I] (B : BayesianSingleItemAuction I) : Prop

Zero normalization for a Bayesian single-item auction's payment rule: reporting 0 gives payment 0, holding the other reports fixed.

Equations

• B.IsZeroNormalized = SingleParameterMechanism.ZeroNormalized B.paymentRule

theorem BayesianSingleItemAuction.interimExpectedPayment_zero_of_isZeroNormalized {I : Type u_1} [DecidableEq I] (B : BayesianSingleItemAuction I) (hzero : B.IsZeroNormalized) (i : I) : B.interimExpectedPayment i 0 = 0

A zero-normalized payment rule has zero interim expected payment at type 0.

theorem BayesianSingleItemAuction.isIndividuallyRationalOnSupport_of_isZeroNormalized_of_hasInterimEnvelopeFormula {I : Type u_1} [DecidableEq I] (B : BayesianSingleItemAuction I) (hzero : B.IsZeroNormalized) (henv : B.HasInterimEnvelopeFormula) (hint_nonneg : B.HasNonnegativeInterimAllocationIntegralOnSupport) : B.IsIndividuallyRationalOnSupport

Under the interim envelope formula and nonnegative envelope increments, zero normalization implies support-restricted interim IR.

Monotonicity and Myerson implementation

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_isMonotone_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : { allocationRule := A.virtualSurplusMaximizingAllocationRule, paymentRule := A.virtualSurplusMaximizingPaymentRule }.IsMonotone

Under regularity, the deterministic virtual-surplus-maximizing allocation rule is monotone in the sense required by SingleParameterMechanism.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingMechanism_isDSIC_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : A.virtualSurplusMaximizingMechanism.IsDSIC

The regular deterministic virtual-surplus-maximizing mechanism is DSIC by the existing Myerson payment theorem.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isDSIC_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : A.virtualSurplusMaximizingAuction.IsDSIC

The constructed Bayesian single-item auction is DSIC after forgetting to the underlying single-parameter mechanism.

Myerson payment formula and uniqueness

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingMechanism_eq_withMyersonPayment {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingMechanism = SingleParameterMechanism.withMyersonPayment A.virtualSurplusMaximizingAllocationRule

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingPaymentRule_eq {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : A.virtualSurplusMaximizingPaymentRule b i = b i * A.virtualSurplusMaximizingAllocationRule b i - ∫ (z : ℝ) in 0..b i, A.virtualSurplusMaximizingAllocationRule (Function.update b i z) i

theorem BayesianSingleItemAuction.norm_virtualSurplusMaximizingPaymentRule_le {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (b : I → ℝ) (i : I) : ‖A.virtualSurplusMaximizingPaymentRule b i‖ ≤ 2 * ‖b i‖

The constructed Myerson payment is bounded by twice the absolute report.

This uses only the pointwise allocation bounds 0 ≤ x ≤ 1; it is the boundedness half of the interim-integrability proof route.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_interimPaymentIntegrand_bound {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (i : I) (z_i : ℝ) : ∀ᵐ (t : OpponentTypeProfile I i) ∂A.opponentPrior i, ‖A.virtualSurplusMaximizingAuction.interimPaymentIntegrand i z_i t‖ ≤ 2 * ‖z_i‖

For each fixed report, the constructed Myerson payment integrand is bounded uniformly over opponent profiles.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_hasIntegrableInterimObjects_of_aestronglyMeasurable {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (halloc_meas : ∀ (i : I) (z_i : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : OpponentTypeProfile I i) => A.virtualSurplusMaximizingAuction.interimAllocationIntegrand i z_i t) (A.opponentPrior i)) (hpay_meas : ∀ (i : I) (z_i : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : OpponentTypeProfile I i) => A.virtualSurplusMaximizingAuction.interimPaymentIntegrand i z_i t) (A.opponentPrior i)) : A.virtualSurplusMaximizingAuction.HasIntegrableInterimObjects

Once the constructed allocation and payment integrands are measurable, boundedness gives interim integrability for the constructed auction.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_hasIntegrableInterimObjects_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : A.virtualSurplusMaximizingAuction.HasIntegrableInterimObjects

theorem BayesianSingleItemAuction.virtualSurplusMaximizingPaymentRule_zeroNormalized {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : SingleParameterMechanism.ZeroNormalized A.virtualSurplusMaximizingPaymentRule

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isZeroNormalized {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.virtualSurplusMaximizingAuction.IsZeroNormalized

theorem BayesianSingleItemAuction.virtualSurplusMaximizingMechanism_quasiLinearUtility_eq {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (v b : I → ℝ) (i : I) : A.virtualSurplusMaximizingMechanism.quasiLinearUtility b v i = (v i - b i) * A.virtualSurplusMaximizingAllocationRule b i + ∫ (z : ℝ) in 0..b i, A.virtualSurplusMaximizingAllocationRule (Function.update b i z) i

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAllocationRule_isImplementable_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : SingleParameterMechanism.IsImplementable A.virtualSurplusMaximizingAllocationRule

theorem BayesianSingleItemAuction.paymentRule_eq_virtualSurplusMaximizingPaymentRule_of_isDSIC_of_zeroNormalized {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) {p : (I → ℝ) → I → ℝ} (hdsic : { allocationRule := A.virtualSurplusMaximizingAllocationRule, paymentRule := p }.IsDSIC) (hzero : SingleParameterMechanism.ZeroNormalized p) : p = A.virtualSurplusMaximizingPaymentRule

theorem BayesianSingleItemAuction.existsUnique_zeroNormalized_paymentRule_for_virtualSurplusMaximizingAllocationRule {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : ∃! p : (I → ℝ) → I → ℝ, SingleParameterMechanism.ZeroNormalized p ∧ { allocationRule := A.virtualSurplusMaximizingAllocationRule, paymentRule := p }.IsDSIC

theorem BayesianSingleItemAuction.virtualSurplusMaximizingMechanism_isVirtualSurplusOptimal_and_isDSIC_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : A.IsVirtualSurplusOptimalAllocationRule A.virtualSurplusMaximizingMechanism.allocationRule ∧ A.virtualSurplusMaximizingMechanism.IsDSIC

Main mechanism-level package theorem for the regular case: the virtual-surplus-maximizing mechanism uses a virtual-surplus-optimal allocation rule and is DSIC with the canonical Myerson payment rule.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isVirtualSurplusOptimal_and_isFeasible_and_isDSIC_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : A.IsVirtualSurplusOptimalAllocationRule A.virtualSurplusMaximizingAuction.allocationRule ∧ A.virtualSurplusMaximizingAuction.IsFeasible ∧ A.virtualSurplusMaximizingAuction.IsDSIC

Main auction-level package theorem for the regular case: the constructed Bayesian single-item auction has a virtual-surplus-optimal allocation rule, is feasible, and is DSIC after forgetting to the underlying single-parameter mechanism.

Support and density assumptions for the analytic identity layer

def BayesianSingleItemAuction.IsOnTypeSupport {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (v : ℝ) : Prop

Agent i's type lies in [0, ωᵢ].

Equations

• A.IsOnTypeSupport i v = (0 ≤ v ∧ v ≤ A.typeData.omega i)

def BayesianSingleItemAuction.IsOnTypeProfileSupport {I : Type u_1} (A : BayesianSingleItemAuction I) (t : I → ℝ) : Prop

A type profile lies in the product support.

Equations

• A.IsOnTypeProfileSupport t = ∀ (i : I), A.IsOnTypeSupport i (t i)

def BayesianSingleItemAuction.HasPositiveDensityOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Densities are positive on support interiors.

Equations

• A.HasPositiveDensityOnSupport = ∀ (i : I) (v : ℝ), 0 < v → v < A.typeData.omega i → 0 < A.typeDensity i v

def BayesianSingleItemAuction.HasNonnegativeDensityOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Densities are nonnegative on supports.

Equations

• A.HasNonnegativeDensityOnSupport = ∀ (i : I) (v : ℝ), 0 ≤ v → v ≤ A.typeData.omega i → 0 ≤ A.typeDensity i v

def BayesianSingleItemAuction.HasPositiveJointDensityAt {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (t : I → ℝ) : Prop

The joint density is positive at a profile.

Equations

• A.HasPositiveJointDensityAt t = (0 < A.jointDensity t)

def BayesianSingleItemAuction.IsOnTypeProfileInterior {I : Type u_1} (A : BayesianSingleItemAuction I) (t : I → ℝ) : Prop

A profile lies in the interior of the product support.

Equations

• A.IsOnTypeProfileInterior t = ∀ (i : I), 0 < t i ∧ t i < A.typeData.omega i

theorem BayesianSingleItemAuction.isOnTypeSupport_left {I : Type u_1} (A : BayesianSingleItemAuction I) {i : I} {v : ℝ} (hv : A.IsOnTypeSupport i v) : 0 ≤ v

theorem BayesianSingleItemAuction.isOnTypeSupport_right {I : Type u_1} (A : BayesianSingleItemAuction I) {i : I} {v : ℝ} (hv : A.IsOnTypeSupport i v) : v ≤ A.typeData.omega i

theorem BayesianSingleItemAuction.isOnTypeProfileSupport_apply {I : Type u_1} (A : BayesianSingleItemAuction I) {t : I → ℝ} (ht : A.IsOnTypeProfileSupport t) (i : I) : A.IsOnTypeSupport i (t i)

theorem BayesianSingleItemAuction.isOnTypeProfileInterior_isOnTypeProfileSupport {I : Type u_1} (A : BayesianSingleItemAuction I) {t : I → ℝ} (ht : A.IsOnTypeProfileInterior t) : A.IsOnTypeProfileSupport t

theorem BayesianSingleItemAuction.typeDensity_pos_of_hasPositiveDensityOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) (hA : A.HasPositiveDensityOnSupport) {i : I} {v : ℝ} (h0 : 0 < v) (homega : v < A.typeData.omega i) : 0 < A.typeDensity i v

theorem BayesianSingleItemAuction.typeDensity_nonneg_of_hasNonnegativeDensityOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) (hA : A.HasNonnegativeDensityOnSupport) {i : I} {v : ℝ} (h0 : 0 ≤ v) (homega : v ≤ A.typeData.omega i) : 0 ≤ A.typeDensity i v

theorem BayesianSingleItemAuction.typeDensity_measurable {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) : Measurable (A.typeDensity i)

theorem BayesianSingleItemAuction.typeDensity_ennreal_ofReal_aemeasurable {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) : AEMeasurable (fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)) (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)))

theorem BayesianSingleItemAuction.typeDensity_nonnegative_ae_of_hasPositiveDensityOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) (hA : A.HasPositiveDensityOnSupport) (i : I) : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v

theorem BayesianSingleItemAuction.typeMeasure_isProbabilityMeasure_of_cdf_absolutelyContinuous_of_density_nonnegative_ae {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (hAC : AbsolutelyContinuousOnInterval (A.typeData.cdf i).cdf 0 (A.typeData.omega i)) (hdens_ae : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) : MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)

theorem BayesianSingleItemAuction.typeMeasure_isProbabilityMeasure_of_cdf_absolutelyContinuous_of_positiveDensity {I : Type u_1} (A : BayesianSingleItemAuction I) (hdens : A.HasPositiveDensityOnSupport) (i : I) (hAC : AbsolutelyContinuousOnInterval (A.typeData.cdf i).cdf 0 (A.typeData.omega i)) : MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)

theorem BayesianSingleItemAuction.typeDensity_pos_of_hasPositiveDensityOnSupport_of_profileInterior {I : Type u_1} (A : BayesianSingleItemAuction I) (hA : A.HasPositiveDensityOnSupport) {t : I → ℝ} (ht : A.IsOnTypeProfileInterior t) (i : I) : 0 < A.typeDensity i (t i)

theorem BayesianSingleItemAuction.jointDensity_pos_of_hasPositiveDensityOnSupport_of_profileInterior {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (hA : A.HasPositiveDensityOnSupport) {t : I → ℝ} (ht : A.IsOnTypeProfileInterior t) : A.HasPositiveJointDensityAt t

theorem BayesianSingleItemAuction.survivalIntegral_eq_intervalIntegral_mul_deriv {F Q : ℝ → ℝ} {ω : ℝ} (hω : 0 ≤ ω) (hF : AbsolutelyContinuousOnInterval F 0 ω) (hF0 : F 0 = 0) (hFω : F ω = 1) (hQ : IntervalIntegrable Q MeasureTheory.volume 0 ω) : ∫ (v : ℝ) in 0..ω, Q v * (1 - F v) = ∫ (v : ℝ) in 0..ω, (∫ (z : ℝ) in 0..v, Q z) * deriv F v

Integration by parts for the survival term.

structure BayesianSingleItemAuction.EnvelopeVirtualSurplusAnalyticAssumptions {I : Type u_1} (A B : BayesianSingleItemAuction I) : Prop

CDF assumptions for the interim virtual-surplus comparison.

• cdf_absolutelyContinuous (i : I) : AbsolutelyContinuousOnInterval (A.typeData.cdf i).cdf 0 (A.typeData.omega i)
• positive_density_on_support : A.HasPositiveDensityOnSupport
• interim_allocation_intervalIntegrable (i : I) : IntervalIntegrable (B.interimAllocProb i) MeasureTheory.volume 0 (A.typeData.omega i)
• interim_allocation_survival_integrable (i : I) : IntervalIntegrable (fun (v : ℝ) => B.interimAllocProb i v * (1 - (A.typeData.cdf i).cdf v)) MeasureTheory.volume 0 (A.typeData.omega i)
• interim_virtual_surplus_integrable (i : I) : IntervalIntegrable (fun (v : ℝ) => B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)

structure BayesianSingleItemAuction.EnvelopeVirtualSurplusEnvironmentAssumptions {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Environment-level analytic assumptions for the envelope/virtual-surplus comparison.

• cdf_absolutelyContinuous (i : I) : AbsolutelyContinuousOnInterval (A.typeData.cdf i).cdf 0 (A.typeData.omega i)
• positive_density_on_support : A.HasPositiveDensityOnSupport

theorem BayesianSingleItemAuction.EnvelopeVirtualSurplusEnvironmentAssumptions.typeDensity_nonnegative_ae {I : Type u_1} {A : BayesianSingleItemAuction I} (h : A.EnvelopeVirtualSurplusEnvironmentAssumptions) (i : I) : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v

theorem BayesianSingleItemAuction.EnvelopeVirtualSurplusEnvironmentAssumptions.typeMeasure_isProbabilityMeasure {I : Type u_1} {A : BayesianSingleItemAuction I} (h : A.EnvelopeVirtualSurplusEnvironmentAssumptions) (i : I) : MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)

theorem BayesianSingleItemAuction.envelopeVirtualSurplusAnalyticAssumptions_of_environment {I : Type u_1} {A B : BayesianSingleItemAuction I} (henv : A.EnvelopeVirtualSurplusEnvironmentAssumptions) (hQ : ∀ (i : I), IntervalIntegrable (B.interimAllocProb i) MeasureTheory.volume 0 (A.typeData.omega i)) (hQsurv : ∀ (i : I), IntervalIntegrable (fun (v : ℝ) => B.interimAllocProb i v * (1 - (A.typeData.cdf i).cdf v)) MeasureTheory.volume 0 (A.typeData.omega i)) (hvirt : ∀ (i : I), IntervalIntegrable (fun (v : ℝ) => B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)) : A.EnvelopeVirtualSurplusAnalyticAssumptions B

theorem BayesianSingleItemAuction.HasPositiveDensityOnSupport.nonzero_on_support {I : Type u_1} (A : BayesianSingleItemAuction I) (hA : A.HasPositiveDensityOnSupport) {i : I} {v : ℝ} (h0 : 0 < v) (homega : v < A.typeData.omega i) : A.typeDensity i v ≠ 0

theorem BayesianSingleItemAuction.EnvelopeVirtualSurplusAnalyticAssumptions.interim_allocation_intervalIntegrableOnSupport {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.EnvelopeVirtualSurplusAnalyticAssumptions B) (i : I) : IntervalIntegrable (B.interimAllocProb i) MeasureTheory.volume 0 (A.typeData.omega i)

theorem BayesianSingleItemAuction.EnvelopeVirtualSurplusAnalyticAssumptions.envelopeIntegrand_eq_onSupport {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.EnvelopeVirtualSurplusAnalyticAssumptions B) (i : I) : Set.EqOn (fun (v : ℝ) => (B.interimAllocProb i v * v - ∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v) (fun (v : ℝ) => B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v + B.interimAllocProb i v * (1 - (A.typeData.cdf i).cdf v) - (∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v) (Set.uIoc 0 (A.typeData.omega i))

theorem BayesianSingleItemAuction.EnvelopeVirtualSurplusAnalyticAssumptions.accumulatedAllocation_density_integrable {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.EnvelopeVirtualSurplusAnalyticAssumptions B) (i : I) : IntervalIntegrable (fun (v : ℝ) => (∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)

theorem BayesianSingleItemAuction.EnvelopeVirtualSurplusAnalyticAssumptions.survivalIntegral_eq_accumulatedDensity {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.EnvelopeVirtualSurplusAnalyticAssumptions B) (i : I) : ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimAllocProb i v * (1 - (A.typeData.cdf i).cdf v) = ∫ (v : ℝ) in 0..A.typeData.omega i, (∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v

theorem BayesianSingleItemAuction.EnvelopeVirtualSurplusAnalyticAssumptions.envelope_density_integrable {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.EnvelopeVirtualSurplusAnalyticAssumptions B) (i : I) : IntervalIntegrable (fun (v : ℝ) => (B.interimAllocProb i v * v - ∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)

Abstract expected-revenue optimality interface

noncomputable def BayesianSingleItemAuction.myersonPaymentRevenueInEnvironment {I : Type u_1} [Fintype I] [DecidableEq I] (A B : BayesianSingleItemAuction I) : ℝ

Myerson-payment revenue of B, evaluated in environment A.

Equations

• A.myersonPaymentRevenueInEnvironment B = A.expectedPaymentRevenueInEnvironment (SingleParameterMechanism.myersonPayment B.allocationRule)

noncomputable def BayesianSingleItemAuction.expectedInterimVirtualSurplus {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : ℝ

Ex-ante virtual surplus through interim allocation probabilities.

Equations

• A.expectedInterimVirtualSurplus B = ∑ i : I, ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v

def BayesianSingleItemAuction.HasExpectedRevenueVirtualSurplusIdentity {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Expected revenue equals expected virtual surplus.

Equations

• A.HasExpectedRevenueVirtualSurplusIdentity B = (A.expectedSellerRevenueInEnvironment B = A.expectedVirtualSurplus B.allocationRule)

def BayesianSingleItemAuction.HasExpectedRevenueVirtualSurplusUpperBound {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Expected revenue is bounded above by expected virtual surplus.

Equations

• A.HasExpectedRevenueVirtualSurplusUpperBound B = (A.expectedSellerRevenueInEnvironment B ≤ A.expectedVirtualSurplus B.allocationRule)

def BayesianSingleItemAuction.HasMyersonPaymentRevenueVirtualSurplusIdentity {I : Type u_1} [Fintype I] [DecidableEq I] (A B : BayesianSingleItemAuction I) : Prop

Myerson-payment revenue equals expected virtual surplus.

Equations

• A.HasMyersonPaymentRevenueVirtualSurplusIdentity B = (A.myersonPaymentRevenueInEnvironment B = A.expectedVirtualSurplus B.allocationRule)

def BayesianSingleItemAuction.HasExpectedVirtualSurplusInterimIdentity {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Ex-ante virtual surplus agrees with the interim expression.

Equations

• A.HasExpectedVirtualSurplusInterimIdentity B = (A.expectedVirtualSurplus B.allocationRule = A.expectedInterimVirtualSurplus B)

structure BayesianSingleItemAuction.InterimFubiniAnalyticAssumptions {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Fubini hypotheses connecting ex-ante and interim expressions.

• payment_integrable (i : I) : MeasureTheory.Integrable (fun (t : I → ℝ) => B.paymentRule t i) A.prior
• virtual_surplus_integrable (i : I) : MeasureTheory.Integrable (fun (t : I → ℝ) => B.allocationRule t i * A.virtualValue i (t i)) A.prior
• payment_interim_fubini (i : I) : ∫ (t : I → ℝ), B.paymentRule t i ∂A.prior = ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimExpectedPayment i v * A.typeDensity i v
• virtual_surplus_interim_fubini (i : I) : ∫ (t : I → ℝ), B.allocationRule t i * A.virtualValue i (t i) ∂A.prior = ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v

theorem BayesianSingleItemAuction.InterimFubiniAnalyticAssumptions.toPaymentInterimFubini {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (h : A.InterimFubiniAnalyticAssumptions B) : A.PaymentInterimFubiniAssumptions B

theorem BayesianSingleItemAuction.InterimFubiniAnalyticAssumptions.expectedPaymentRevenueIntegrable {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (h : A.InterimFubiniAnalyticAssumptions B) : MeasureTheory.Integrable (fun (t : I → ℝ) => ∑ i : I, B.paymentRule t i) A.prior

theorem BayesianSingleItemAuction.InterimFubiniAnalyticAssumptions.integrableVirtualSurplus {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (h : A.InterimFubiniAnalyticAssumptions B) : A.IntegrableVirtualSurplus B.allocationRule

theorem BayesianSingleItemAuction.InterimFubiniAnalyticAssumptions.hasExpectedRevenueInterimPaymentIdentity {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (h : A.InterimFubiniAnalyticAssumptions B) : A.HasExpectedRevenueInterimPaymentIdentity B

theorem BayesianSingleItemAuction.InterimFubiniAnalyticAssumptions.hasExpectedVirtualSurplusInterimIdentity {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (h : A.InterimFubiniAnalyticAssumptions B) : A.HasExpectedVirtualSurplusInterimIdentity B

structure BayesianSingleItemAuction.TypeMeasureInterimFubiniAnalyticAssumptions {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Type-measure Fubini hypotheses.

• payment_integrable (i : I) : MeasureTheory.Integrable (fun (t : I → ℝ) => B.paymentRule t i) A.prior
• virtual_surplus_integrable (i : I) : MeasureTheory.Integrable (fun (t : I → ℝ) => B.allocationRule t i * A.virtualValue i (t i)) A.prior
• type_density_measurable (i : I) : AEMeasurable (fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)) (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)))
• type_density_nonnegative_ae (i : I) : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v
• payment_typeMeasure_fubini (i : I) : ∫ (t : I → ℝ), B.paymentRule t i ∂A.prior = ∫ (v : ℝ), B.interimExpectedPayment i v ∂A.typeMeasure i
• virtual_surplus_typeMeasure_fubini (i : I) : ∫ (t : I → ℝ), B.allocationRule t i * A.virtualValue i (t i) ∂A.prior = ∫ (v : ℝ), B.interimAllocProb i v * A.virtualValue i v ∂A.typeMeasure i

theorem BayesianSingleItemAuction.typeMeasureInterimFubiniAnalyticAssumptions_of_typeMeasure_fubini {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (hdens_ae : ∀ (i : I), ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hpay_int : ∀ (i : I), MeasureTheory.Integrable (fun (t : I → ℝ) => B.paymentRule t i) A.prior) (hvs_int : ∀ (i : I), MeasureTheory.Integrable (fun (t : I → ℝ) => B.allocationRule t i * A.virtualValue i (t i)) A.prior) (hpay_fubini : ∀ (i : I), ∫ (t : I → ℝ), B.paymentRule t i ∂A.prior = ∫ (v : ℝ), B.interimExpectedPayment i v ∂A.typeMeasure i) (hvs_fubini : ∀ (i : I), ∫ (t : I → ℝ), B.allocationRule t i * A.virtualValue i (t i) ∂A.prior = ∫ (v : ℝ), B.interimAllocProb i v * A.virtualValue i v ∂A.typeMeasure i) : A.TypeMeasureInterimFubiniAnalyticAssumptions B

theorem BayesianSingleItemAuction.TypeMeasureInterimFubiniAnalyticAssumptions.toInterimFubini {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (h : A.TypeMeasureInterimFubiniAnalyticAssumptions B) : A.InterimFubiniAnalyticAssumptions B

def BayesianSingleItemAuction.HasInterimPaymentVirtualSurplusUpperBound {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Interim-payment revenue is bounded by interim virtual surplus.

Equations

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

def BayesianSingleItemAuction.HasInterimPaymentEnvelopeUpperBound {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

The envelope-term upper bound for interim expected payments.

Equations

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

def BayesianSingleItemAuction.HasEnvelopeVirtualSurplusUpperBound {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Envelope-term revenue is bounded by interim virtual surplus.

Equations

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

theorem BayesianSingleItemAuction.EnvelopeVirtualSurplusAnalyticAssumptions.envelopeIntegral_eq_virtualSurplusIntegral {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.EnvelopeVirtualSurplusAnalyticAssumptions B) (i : I) : ∫ (v : ℝ) in 0..A.typeData.omega i, (B.interimAllocProb i v * v - ∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v = ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v

theorem BayesianSingleItemAuction.hasEnvelopeVirtualSurplusUpperBound_of_analyticAssumptions {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (h : A.EnvelopeVirtualSurplusAnalyticAssumptions B) : A.HasEnvelopeVirtualSurplusUpperBound B

theorem BayesianSingleItemAuction.intervalIntegrable_interimAllocProb_mul_virtualValue_mul_typeDensity_of_profileSplit_integrable {I : Type u_1} {A B : BayesianSingleItemAuction I} (i : I) (hmeas : AEMeasurable (fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)) (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)))) (hnonneg : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hvs : MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.allocationRule (reportProfile i p.1 p.2) i * A.virtualValue i p.1) ((A.typeMeasure i).prod (B.opponentPrior i))) : IntervalIntegrable (fun (v : ℝ) => B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)

Product-side virtual-surplus integrability gives interval integrability of the density-weighted interim virtual surplus.

@[simp]

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_hasSameSellingEnvironment {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : A.HasSameSellingEnvironment A.virtualSurplusMaximizingAuction

theorem BayesianSingleItemAuction.integrableVirtualSurplus_of_profileSplit_integrable_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] {A B : BayesianSingleItemAuction I} [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (hind : A.HasIndependentTypePriors) (henv : A.HasSameSellingEnvironment B) (hvs_prod_int : ∀ (i : I), MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.allocationRule (reportProfile i p.1 p.2) i * A.virtualValue i p.1) ((A.typeMeasure i).prod (B.opponentPrior i))) : A.IntegrableVirtualSurplus B.allocationRule

Product-side virtual-surplus integrability gives ex-ante virtual-surplus integrability under independent priors.

theorem BayesianSingleItemAuction.typeMeasureInterimFubiniAnalyticAssumptions_of_independentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] {A B : BayesianSingleItemAuction I} [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (hdens_ae : ∀ (i : I), ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hind : A.HasIndependentTypePriors) (henv : A.HasSameSellingEnvironment B) (hpay_prod_int : ∀ (i : I), MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.paymentRule (reportProfile i p.1 p.2) i) ((A.typeMeasure i).prod (B.opponentPrior i))) (hvs_prod_int : ∀ (i : I), MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.allocationRule (reportProfile i p.1 p.2) i * A.virtualValue i p.1) ((A.typeMeasure i).prod (B.opponentPrior i))) : A.TypeMeasureInterimFubiniAnalyticAssumptions B

Build type-measure Fubini hypotheses from independent priors and product-side integrability. This is the main bridge from the full prior to interim one-dimensional expressions.

theorem BayesianSingleItemAuction.interimFubiniAnalyticAssumptions_of_independentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] {A B : BayesianSingleItemAuction I} [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (hdens_ae : ∀ (i : I), ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hind : A.HasIndependentTypePriors) (henv : A.HasSameSellingEnvironment B) (hpay_prod_int : ∀ (i : I), MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.paymentRule (reportProfile i p.1 p.2) i) ((A.typeMeasure i).prod (B.opponentPrior i))) (hvs_prod_int : ∀ (i : I), MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.allocationRule (reportProfile i p.1 p.2) i * A.virtualValue i p.1) ((A.typeMeasure i).prod (B.opponentPrior i))) : A.InterimFubiniAnalyticAssumptions B

def BayesianSingleItemAuction.IsRevenueComparable {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Feasible candidates with revenue equal to virtual surplus.

Equations

• A.IsRevenueComparable B = (A.HasSameSellingEnvironment B ∧ B.IsFeasible ∧ A.IntegrableVirtualSurplus B.allocationRule ∧ A.HasExpectedRevenueVirtualSurplusIdentity B)

def BayesianSingleItemAuction.IsRevenueUpperBounded {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Feasible candidates with revenue bounded by virtual surplus.

Equations

• A.IsRevenueUpperBounded B = (A.HasSameSellingEnvironment B ∧ B.IsFeasible ∧ A.IntegrableVirtualSurplus B.allocationRule ∧ A.HasExpectedRevenueVirtualSurplusUpperBound B)

def BayesianSingleItemAuction.IsFeasibleICIRIntegrable {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Feasible IC/IR candidates with integrable virtual surplus.

Equations

• A.IsFeasibleICIRIntegrable B = (A.HasSameSellingEnvironment B ∧ B.IsFeasible ∧ B.IsIncentiveCompatible ∧ B.IsIndividuallyRationalOnSupport ∧ A.IntegrableVirtualSurplus B.allocationRule)

structure BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) : Prop

Analytic assumptions for MSZ 12.59.

• independent_type_priors : A.HasIndependentTypePriors
• envelope_environment : A.EnvelopeVirtualSurplusEnvironmentAssumptions
• candidate_payment_profileSplit_integrable (B : BayesianSingleItemAuction I) : B.IsFeasible → B.IsIncentiveCompatible → B.IsIndividuallyRationalOnSupport → ∀ (i : I), MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.paymentRule (reportProfile i p.1 p.2) i) ((A.typeMeasure i).prod (B.opponentPrior i))
• candidate_virtual_surplus_profileSplit_integrable (B : BayesianSingleItemAuction I) : B.IsFeasible → B.IsIncentiveCompatible → B.IsIndividuallyRationalOnSupport → ∀ (i : I), MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.allocationRule (reportProfile i p.1 p.2) i * A.virtualValue i p.1) ((A.typeMeasure i).prod (B.opponentPrior i))

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.typeMeasure_isProbabilityMeasure {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (i : I) : MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.typeDensity_nonnegative_ae {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (i : I) : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_payment_density_integrable {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (B : BayesianSingleItemAuction I) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) (i : I) : IntervalIntegrable (fun (v : ℝ) => B.interimExpectedPayment i v * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_interim_virtual_surplus_density_integrable {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (B : BayesianSingleItemAuction I) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) (i : I) : IntervalIntegrable (fun (v : ℝ) => B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_allocation_survival_integrable {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (B : BayesianSingleItemAuction I) (_hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (_hIR : B.IsIndividuallyRationalOnSupport) (i : I) : IntervalIntegrable (fun (v : ℝ) => B.interimAllocProb i v * (1 - (A.typeData.cdf i).cdf v)) MeasureTheory.volume 0 (A.typeData.omega i)

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_envelope_analytic {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (B : BayesianSingleItemAuction I) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) : A.EnvelopeVirtualSurplusAnalyticAssumptions B

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_typeMeasure_interim_fubini {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (B : BayesianSingleItemAuction I) (henv : A.HasSameSellingEnvironment B) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) : A.TypeMeasureInterimFubiniAnalyticAssumptions B

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_interim_fubini {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (B : BayesianSingleItemAuction I) (henv : A.HasSameSellingEnvironment B) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) : A.InterimFubiniAnalyticAssumptions B

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_integrableVirtualSurplus {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (B : BayesianSingleItemAuction I) (henv : A.HasSameSellingEnvironment B) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) : A.IntegrableVirtualSurplus B.allocationRule

def BayesianSingleItemAuction.IsExpectedSellerRevenueOptimalInEnvironmentAmong {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (Candidate : BayesianSingleItemAuction I → Prop) : Prop

Expected seller-revenue optimality among candidates.

Equations

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

def BayesianSingleItemAuction.IsRegularMyersonOptimalICIRAuction {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Regular Myerson optimality among feasible IC/IR mechanisms.

Equations

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

theorem BayesianSingleItemAuction.IsRegularMyersonOptimalICIRAuction.isVirtualSurplusOptimalAllocationRule {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (hB : A.IsRegularMyersonOptimalICIRAuction B) : A.IsVirtualSurplusOptimalAllocationRule B.allocationRule

theorem BayesianSingleItemAuction.IsRegularMyersonOptimalICIRAuction.isFeasible {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (hB : A.IsRegularMyersonOptimalICIRAuction B) : B.IsFeasible

theorem BayesianSingleItemAuction.IsRegularMyersonOptimalICIRAuction.isIncentiveCompatible {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (hB : A.IsRegularMyersonOptimalICIRAuction B) : B.IsIncentiveCompatible

theorem BayesianSingleItemAuction.IsRegularMyersonOptimalICIRAuction.isIndividuallyRationalOnSupport {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (hB : A.IsRegularMyersonOptimalICIRAuction B) : B.IsIndividuallyRationalOnSupport

theorem BayesianSingleItemAuction.IsRegularMyersonOptimalICIRAuction.isExpectedSellerRevenueOptimal {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (hB : A.IsRegularMyersonOptimalICIRAuction B) : A.IsExpectedSellerRevenueOptimalInEnvironmentAmong B fun (C : BayesianSingleItemAuction I) => A.IsFeasibleICIRIntegrable C

theorem BayesianSingleItemAuction.expectedSellerRevenueInEnvironment_le_of_expectedVirtualSurplus_le {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) {B C : BayesianSingleItemAuction I} (hB : A.HasExpectedRevenueVirtualSurplusIdentity B) (hC : A.HasExpectedRevenueVirtualSurplusIdentity C) (hvs : A.expectedVirtualSurplus B.allocationRule ≤ A.expectedVirtualSurplus C.allocationRule) : A.expectedSellerRevenueInEnvironment B ≤ A.expectedSellerRevenueInEnvironment C

Virtual-surplus comparison gives revenue comparison under identity.

theorem BayesianSingleItemAuction.hasExpectedRevenueVirtualSurplusUpperBound_of_identity {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (hB : A.HasExpectedRevenueVirtualSurplusIdentity B) : A.HasExpectedRevenueVirtualSurplusUpperBound B

theorem BayesianSingleItemAuction.paymentRule_eq_myersonPayment_of_isDSIC_of_isZeroNormalized {I : Type u_1} [Fintype I] [DecidableEq I] (B : BayesianSingleItemAuction I) (hdsic : B.IsDSIC) (hzero : B.IsZeroNormalized) : B.paymentRule = SingleParameterMechanism.myersonPayment B.allocationRule

theorem BayesianSingleItemAuction.expectedSellerRevenueInEnvironment_eq_myersonPaymentRevenueInEnvironment_of_isDSIC_of_isZeroNormalized {I : Type u_1} [Fintype I] [DecidableEq I] (A B : BayesianSingleItemAuction I) (hdsic : B.IsDSIC) (hzero : B.IsZeroNormalized) : A.expectedSellerRevenueInEnvironment B = A.myersonPaymentRevenueInEnvironment B

theorem BayesianSingleItemAuction.hasExpectedRevenueVirtualSurplusIdentity_of_myersonPaymentIdentity_of_isDSIC_of_isZeroNormalized {I : Type u_1} [Fintype I] [DecidableEq I] (A B : BayesianSingleItemAuction I) (hmyerson : A.HasMyersonPaymentRevenueVirtualSurplusIdentity B) (hdsic : B.IsDSIC) (hzero : B.IsZeroNormalized) : A.HasExpectedRevenueVirtualSurplusIdentity B

theorem BayesianSingleItemAuction.hasExpectedRevenueVirtualSurplusUpperBound_of_interim_identities {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (hrev : A.HasExpectedRevenueInterimPaymentIdentity B) (hvs : A.HasExpectedVirtualSurplusInterimIdentity B) (hupper : A.HasInterimPaymentVirtualSurplusUpperBound B) : A.HasExpectedRevenueVirtualSurplusUpperBound B

theorem BayesianSingleItemAuction.hasExpectedRevenueVirtualSurplusIdentity_of_interim_identities {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (hrev : A.HasExpectedRevenueInterimPaymentIdentity B) (hvs : A.HasExpectedVirtualSurplusInterimIdentity B) (hid : ∀ (i : I), ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimExpectedPayment i v * A.typeDensity i v = ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v) : A.HasExpectedRevenueVirtualSurplusIdentity B

theorem BayesianSingleItemAuction.hasInterimPaymentVirtualSurplusUpperBound_of_envelope_upper {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (hpay : A.HasInterimPaymentEnvelopeUpperBound B) (henv : A.HasEnvelopeVirtualSurplusUpperBound B) : A.HasInterimPaymentVirtualSurplusUpperBound B

theorem BayesianSingleItemAuction.hasInterimPaymentEnvelopeIdentity_of_zeroNormalized_of_interimPaymentFormula {I : Type u_1} [Fintype I] [DecidableEq I] (A B : BayesianSingleItemAuction I) (hzero : B.IsZeroNormalized) (hpay_formula : B.HasInterimPaymentFormula) (i : I) : ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimExpectedPayment i v * A.typeDensity i v = ∫ (v : ℝ) in 0..A.typeData.omega i, (B.interimAllocProb i v * v - ∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v

theorem BayesianSingleItemAuction.hasInterimPaymentVirtualSurplusIdentity_of_zeroNormalized_of_interimPaymentFormula {I : Type u_1} [Fintype I] [DecidableEq I] (A B : BayesianSingleItemAuction I) (hzero : B.IsZeroNormalized) (hpay_formula : B.HasInterimPaymentFormula) (henv : A.EnvelopeVirtualSurplusAnalyticAssumptions B) (i : I) : ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimExpectedPayment i v * A.typeDensity i v = ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimAllocProb i v * A.virtualValue i v * A.typeDensity i v

theorem BayesianSingleItemAuction.hasInterimPaymentEnvelopeUpperBound_of_pointwise {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (hdens_ae : ∀ (i : I), ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hint_pay : ∀ (i : I), IntervalIntegrable (fun (v : ℝ) => B.interimExpectedPayment i v * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)) (hint_env : ∀ (i : I), IntervalIntegrable (fun (v : ℝ) => (B.interimAllocProb i v * v - ∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)) (hpoint : ∀ (i : I) (v : ℝ), 0 ≤ v → v ≤ A.typeData.omega i → B.interimExpectedPayment i v ≤ B.interimAllocProb i v * v - ∫ (z : ℝ) in 0..v, B.interimAllocProb i z) : A.HasInterimPaymentEnvelopeUpperBound B

theorem BayesianSingleItemAuction.hasInterimPaymentEnvelopeUpperBound_of_isIncentiveCompatible_of_isIndividuallyRationalOnSupport {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (hdens_ae : ∀ (i : I), ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hint_pay : ∀ (i : I), IntervalIntegrable (fun (v : ℝ) => B.interimExpectedPayment i v * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)) (hint_env : ∀ (i : I), IntervalIntegrable (fun (v : ℝ) => (B.interimAllocProb i v * v - ∫ (z : ℝ) in 0..v, B.interimAllocProb i z) * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) : A.HasInterimPaymentEnvelopeUpperBound B

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_payment_envelope_upper {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A B : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) : A.HasInterimPaymentEnvelopeUpperBound B

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_revenue_interim_identity {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A B : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (henv : A.HasSameSellingEnvironment B) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) : A.HasExpectedRevenueInterimPaymentIdentity B

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.candidate_virtual_surplus_interim_identity {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A B : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (henv : A.HasSameSellingEnvironment B) (hfeas : B.IsFeasible) (hIC : B.IsIncentiveCompatible) (hIR : B.IsIndividuallyRationalOnSupport) : A.HasExpectedVirtualSurplusInterimIdentity B

theorem BayesianSingleItemAuction.isRevenueUpperBounded_of_isRevenueComparable {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) (hB : A.IsRevenueComparable B) : A.IsRevenueUpperBounded B

theorem BayesianSingleItemAuction.isRevenueUpperBounded_of_ic_ir_upper {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A B : BayesianSingleItemAuction I) (h : A.RegularMyersonICIRAnalyticAssumptions) (hB : A.IsFeasibleICIRIntegrable B) : A.IsRevenueUpperBounded B

theorem BayesianSingleItemAuction.isRevenueComparable_of_myersonPaymentIdentity_of_isDSIC_of_isZeroNormalized {I : Type u_1} [Fintype I] [DecidableEq I] (A B : BayesianSingleItemAuction I) (henv : A.HasSameSellingEnvironment B) (hfeas : B.IsFeasible) (hint : A.IntegrableVirtualSurplus B.allocationRule) (hmyerson : A.HasMyersonPaymentRevenueVirtualSurplusIdentity B) (hdsic : B.IsDSIC) (hzero : B.IsZeroNormalized) : A.IsRevenueComparable B

theorem BayesianSingleItemAuction.expectedSellerRevenueInEnvironment_le_virtualSurplusMaximizingAuction {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A B : BayesianSingleItemAuction I) (hB : A.IsRevenueComparable B) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule) (hopt_id : A.HasExpectedRevenueVirtualSurplusIdentity A.virtualSurplusMaximizingAuction) : A.expectedSellerRevenueInEnvironment B ≤ A.expectedSellerRevenueInEnvironment A.virtualSurplusMaximizingAuction

theorem BayesianSingleItemAuction.expectedSellerRevenueInEnvironment_le_virtualSurplusMaximizingAuction_of_revenueUpperBounded {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A B : BayesianSingleItemAuction I) (hB : A.IsRevenueUpperBounded B) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule) (hopt_id : A.HasExpectedRevenueVirtualSurplusIdentity A.virtualSurplusMaximizingAuction) : A.expectedSellerRevenueInEnvironment B ≤ A.expectedSellerRevenueInEnvironment A.virtualSurplusMaximizingAuction

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isRevenueComparable {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule) (hopt_id : A.HasExpectedRevenueVirtualSurplusIdentity A.virtualSurplusMaximizingAuction) : A.IsRevenueComparable A.virtualSurplusMaximizingAuction

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isRevenueUpperBounded {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule) (hopt_id : A.HasExpectedRevenueVirtualSurplusIdentity A.virtualSurplusMaximizingAuction) : A.IsRevenueUpperBounded A.virtualSurplusMaximizingAuction

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isIncentiveCompatible_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : A.virtualSurplusMaximizingAuction.IsIncentiveCompatible

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isIndividuallyRationalOnSupport {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (henv : A.virtualSurplusMaximizingAuction.HasInterimEnvelopeFormula) (hint_nonneg : A.virtualSurplusMaximizingAuction.HasNonnegativeInterimAllocationIntegralOnSupport) : A.virtualSurplusMaximizingAuction.IsIndividuallyRationalOnSupport

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isIncentiveCompatible_and_individuallyRationalOnSupport_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : A.virtualSurplusMaximizingAuction.IsIncentiveCompatible ∧ A.virtualSurplusMaximizingAuction.IsIndividuallyRationalOnSupport

MSZ 12.58: regular Myerson is IC and IR.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isIndividuallyRationalOnSupport_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) : A.virtualSurplusMaximizingAuction.IsIndividuallyRationalOnSupport

IR half of MSZ 12.58.

theorem BayesianSingleItemAuction.RegularMyersonICIRAnalyticAssumptions.opt_identity {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] {A : BayesianSingleItemAuction I} (h : A.RegularMyersonICIRAnalyticAssumptions) (hA : A.IsRegular) : A.HasExpectedRevenueVirtualSurplusIdentity A.virtualSurplusMaximizingAuction

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isFeasibleICIRIntegrable_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) (h : A.RegularMyersonICIRAnalyticAssumptions) : A.IsFeasibleICIRIntegrable A.virtualSurplusMaximizingAuction

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isExpectedSellerRevenueOptimalInEnvironmentAmongRevenueComparable {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule) (hopt_id : A.HasExpectedRevenueVirtualSurplusIdentity A.virtualSurplusMaximizingAuction) : A.IsExpectedSellerRevenueOptimalInEnvironmentAmong A.virtualSurplusMaximizingAuction fun (B : BayesianSingleItemAuction I) => A.IsRevenueComparable B

Revenue optimality among revenue-comparable candidates.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isExpectedSellerRevenueOptimalInEnvironmentAmongRevenueUpperBounded {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hopt_int : A.IntegrableVirtualSurplus A.virtualSurplusMaximizingAuction.allocationRule) (hopt_id : A.HasExpectedRevenueVirtualSurplusIdentity A.virtualSurplusMaximizingAuction) : A.IsExpectedSellerRevenueOptimalInEnvironmentAmong A.virtualSurplusMaximizingAuction fun (B : BayesianSingleItemAuction I) => A.IsRevenueUpperBounded B

Revenue optimality under the one-sided revenue upper bound.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_isExpectedSellerRevenueOptimalInEnvironmentAmongFeasibleICIRIntegrable_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) (h : A.RegularMyersonICIRAnalyticAssumptions) : A.IsExpectedSellerRevenueOptimalInEnvironmentAmong A.virtualSurplusMaximizingAuction fun (B : BayesianSingleItemAuction I) => A.IsFeasibleICIRIntegrable B

MSZ 12.59: revenue optimality among IC/IR candidates.

theorem BayesianSingleItemAuction.virtualSurplusMaximizingAuction_regularMyersonOptimalICIR_of_isRegular {I : Type u_1} [Fintype I] [Nontrivial I] [DecidableEq I] [LinearOrder I] (A : BayesianSingleItemAuction I) (hA : A.IsRegular) (h : A.RegularMyersonICIRAnalyticAssumptions) : A.IsRegularMyersonOptimalICIRAuction A.virtualSurplusMaximizingAuction

MSZ 12.59 compact theorem.