buying_to_bundle_intermediate_surrogate_dispersion_gap_bound

Proved

by qm2204 · Jul 3, 2026 · Mathlib c5ea003 (Lean v4.30.0)

asymptoticseconomicsmechanism-designprobability

Second gap bound in the proof of Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers (App. C.2 p. 36). With $\varpi'$ the intermediate surrogate profit (deterministic inclusion weights inside the buyer valuation, the identical expression as in buying_to_bundle_profit_intermediate_surrogate_gap_bound) and $\varpi(x)=N\,E[x(\mu)(\mu-\varphi(\mu))]$ the surrogate profit of eq. (2): there exists $K>0$ depending only on $(\sigma,\gamma,\xi,\mu_H)$ such that for every IC allocation rule $x$ and every $N\ge1$ ,

|\varpi'(x)-\varpi(x)|\ \le\ K\,N^{2/3}.

Paper proof: $\varpi'(x)-\varpi(x)=E_{\boldsymbol\mu}\big[Rev(\Upsilon+\sigma\sum_ix(\mu_i)Z_i)-\Upsilon\big]$ with $\Upsilon=\sum_ix(\mu_i)\mu_i$ ; apply Lemma 4.5 with $C=\Upsilon\le N\mu_H$ , $a_i=x(\mu_i)\in[0,1]$ , $A\le N$ , and integrate. Formalization note: splitting $\varpi$ against the payment term uses integrability of the virtual cost.

Preamble

import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Definitions.Def_buying_to_bundle_market

open MeasureTheory

Formal statement

theorem buying_to_bundle_intermediate_surrogate_dispersion_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 →
      |((∫ μ : 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) -
        N * BuyingToBundle.surrogatePerSeller qual noise σ qualPdf x| ≤
        K * (N : ℝ) ^ ((2 : ℝ) / 3) := by sorry

Source

Buying to Bundle: Optimal Sourcing from Monopolistic Sellers (2025), Appendix C.2 (proof of Theorem 4.6)

View graph