monopoly_revenue_subexponential_dispersion_bound

Proved

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

concentrationeconomicsmechanism-designprobability

Lemma 4.5 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers (p. 15; proof App. C.2 pp. 33–35). Assume $Z$ is a sub-exponential random variable $Z\in SE(\gamma^2,\xi)$ with parameters $\gamma,\xi>0$ , i.e. $E[e^{\lambda Z}]\le e^{\lambda^2\gamma^2/2}$ for all $|\lambda|<1/\xi$ , and (standing Section-4 assumptions, used in the paper's own proof) $Z$ has mean zero and variance one. Let $Z_1,\dots,Z_N$ be i.i.d. copies of $Z$ . For any buyer valuation $v=C+\sigma\sum_{i\in[N]}a_iZ_i$ where $C\ge 0$ , $\sigma>0$ are constants and $a_i\in[0,1]$ , let $A=\sum_{i\in[N]}a_i^2$ . Then

\Big|Rev\big(C+\sigma\sum_i a_iZ_i\big)-C\Big|\le\max\Big\{\sigma\gamma e^{-1/2}A^{1/2},\ \frac{8\sigma\xi}{3e},\ \sqrt{2}\,\sigma A^{1/2},\ 2\sigma^{2/3}(CA)^{1/3}\Big\}.

Upper direction: Chernoff via the product MGF bound (sub-Gaussian regime for $\eta<\gamma^2\sqrt A/\xi$ , sub-exponential regime beyond). Lower direction: price at $C-\sigma\sqrt A\,\eta$ and control the lost demand by Chebyshev/Cantelli (this is where mean 0/variance 1 enter); optimizing $\eta^*=(2C/(\sigma\sqrt A))^{1/3}$ gives the last two terms. $C\ge0$ is implicit in the paper ( $C$ is a bundle mean quality) and is used in the lower-bound pricing step.

Preamble

import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Definitions.Def_monopoly_pricing

open MeasureTheory

Formal statement

theorem monopoly_revenue_subexponential_dispersion_bound
    (N : ℕ) (noise : Measure ℝ) [IsProbabilityMeasure noise]
    (γ ξ σ C : ℝ) (a : Fin N → ℝ)
    (hσ : 0 < σ) (hγ : 0 < γ) (hξ : 0 < ξ) (hC : 0 ≤ C)
    (ha : ∀ i, a i ∈ Set.Icc (0 : ℝ) 1)
    (hmean : ∫ z, z ∂noise = 0)
    (hvar : ∫ z, z ^ 2 ∂noise = 1)
    (hse : ∀ l : ℝ, |l| < 1 / ξ →
      ∫⁻ z, ENNReal.ofReal (Real.exp (l * z)) ∂noise ≤
        ENNReal.ofReal (Real.exp (l ^ 2 * γ ^ 2 / 2))) :
    |BuyingToBundle.monopolyRevenue
        ((Measure.pi fun _ : Fin N => noise).map
          fun z => C + σ * ∑ i, a i * z i) - C| ≤
      max
        (max (σ * γ * Real.exp (-(1 : ℝ) / 2) * Real.sqrt (∑ i, a i ^ 2))
          (8 * σ * ξ / (3 * Real.exp 1)))
        (max (Real.sqrt 2 * σ * Real.sqrt (∑ i, a i ^ 2))
          (2 * σ ^ ((2 : ℝ) / 3) * (C * ∑ i, a i ^ 2) ^ ((1 : ℝ) / 3))) := by sorry

Source

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

View graph