buying_to_bundle_asymptotic_surrogate_optimality
ProvedTheorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers (asymptotic optimality of the surrogate-profit mechanism in large markets). Buyers value seller 's item at , where is a strictly regular, sub-exponential random variable with mean zero and unit variance, and the private qualities are i.i.d. with positive density on . Let be an incentive-compatible allocation rule (measurable, monotone non-increasing into ) maximizing the expected surrogate profit , where is the Myerson virtual cost — by Theorem 4.4 of the paper the maximizer is a threshold rule. If , then the profit-maximizing IC mechanism improves on by at most a factor : there exist and such that for every market size , the expected profit satisfies and every IC allocation rule has
Hence for any profit-maximizing rule : bundling via the simple surrogate threshold mechanism is asymptotically profit-optimal.
import Mathlib.Analysis.SpecialFunctions.Pow.Real import Definitions.Def_buying_to_bundle_market open MeasureTheory
theorem buying_to_bundle_asymptotic_surrogate_optimality
(σ μL μH γ ξ : ℝ) (qual noise : Measure ℝ)
[IsProbabilityMeasure qual] [IsProbabilityMeasure noise]
(qualPdf noisePdf : ℝ → ℝ)
(hM : BuyingToBundle.MarketAssumptions σ μL μH γ ξ qual noise qualPdf noisePdf)
(xbar : ℝ → ℝ) (hxbar : BuyingToBundle.IsAllocationRule μL μH xbar)
(hmax : ∀ y : ℝ → ℝ, BuyingToBundle.IsAllocationRule μL μH y →
BuyingToBundle.surrogatePerSeller qual noise σ qualPdf y ≤
BuyingToBundle.surrogatePerSeller qual noise σ qualPdf xbar)
(hpos : 0 < BuyingToBundle.surrogatePerSeller qual noise σ qualPdf xbar) :
∃ C : ℝ, 0 < C ∧ ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N →
0 < BuyingToBundle.profit qual noise σ qualPdf N xbar ∧
∀ x : ℝ → ℝ, BuyingToBundle.IsAllocationRule μL μH x →
BuyingToBundle.profit qual noise σ qualPdf N x ≤
(1 + C / (N : ℝ) ^ ((1 : ℝ) / 3)) *
BuyingToBundle.profit qual noise σ qualPdf N xbar := by sorry