buying_to_bundle_profit_intermediate_surrogate_gap_bound
ProvedFirst gap bound in the proof of Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers (App. C.2 pp. 35–36). Define the intermediate surrogate profit — the profit with the random inclusion pattern replaced by deterministic inclusion weights inside the buyer valuation (the payment term is written , equal to by symmetry — the same shape as eq. (1) in the root statement). Then there exists depending only on such that for every IC allocation rule and every ,
Paper proof: for every realization , triangle inequality through the revenues at and ; the outer terms are by Lemma 4.5 (monopoly_revenue_subexponential_dispersion_bound, applied with and , using , ), and the middle term integrates to by eq. (5) (buying_to_bundle_expected_bundle_quality_fluctuation_bound).
import Mathlib.MeasureTheory.Constructions.Pi import Mathlib.Analysis.SpecialFunctions.Pow.Real import Definitions.Def_buying_to_bundle_market open MeasureTheory
theorem buying_to_bundle_profit_intermediate_surrogate_gap_bound
(σ μL μH γ ξ : ℝ) (qual noise : Measure ℝ)
[IsProbabilityMeasure qual] [IsProbabilityMeasure noise]
(qualPdf noisePdf : ℝ → ℝ)
(hM : BuyingToBundle.MarketAssumptions σ μL μH γ ξ qual noise qualPdf noisePdf) :
∃ K : ℝ, 0 < K ∧ ∀ N : ℕ, 1 ≤ N → ∀ x : ℝ → ℝ,
BuyingToBundle.IsAllocationRule μL μH x →
|BuyingToBundle.profit qual noise σ qualPdf N x -
((∫ μ : Fin N → ℝ,
BuyingToBundle.monopolyRevenue
((Measure.pi fun _ : Fin N => noise).map
fun z => ∑ i, x (μ i) * (μ i + σ * z i))
∂(Measure.pi fun _ : Fin N => qual)) -
N * ∫ m, BuyingToBundle.virtualCost qual noise σ qualPdf m * x m ∂qual)| ≤
K * (N : ℝ) ^ ((2 : ℝ) / 3) := by sorry