buying_to_bundle_expected_bundle_quality_fluctuation_bound

Proved

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

concentrationeconomicsmechanism-designprobability

Equation (5) in the proof of Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers (App. C.2 p. 35): Bernoulli fluctuation of the bundle mean quality. For any allocation rule $x$ , with $Y(\mathbf I,\boldsymbol\mu)=\sum_i I_i\mu_i$ the realized bundle quality and $\Upsilon(x,\boldsymbol\mu)=\sum_i x(\mu_i)\mu_i$ its conditional mean,

E_{\boldsymbol\mu,\mathbf I}\big[\,|Y(\mathbf I,\boldsymbol\mu)-\Upsilon(x,\boldsymbol\mu)|\,\big]\ \le\ \mu_H\sqrt N.

Paper proof: conditional on $\boldsymbol\mu$ , $E_{\mathbf I}[Y]=\Upsilon$ and $Var(Y\mid\boldsymbol\mu)=\sum_i x(\mu_i)(1-x(\mu_i))\mu_i^2\le\mu_H^2 N$ , then Jensen/Cauchy–Schwarz. The expectation over $\mathbf I\sim\otimes_i\mathrm{Bernoulli}(x(\mu_i))$ is written as the exact finite mixture over inclusion patterns (the same weighting as expectedBundleRevenue); the expectation over $\boldsymbol\mu$ is the $N$ -fold product of the quality distribution.

Preamble

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

open MeasureTheory

Formal statement

theorem buying_to_bundle_expected_bundle_quality_fluctuation_bound
    (σ μL μH γ ξ : ℝ) (qual noise : Measure ℝ)
    [IsProbabilityMeasure qual] [IsProbabilityMeasure noise]
    (qualPdf noisePdf : ℝ → ℝ)
    (hM : BuyingToBundle.MarketAssumptions σ μL μH γ ξ qual noise qualPdf noisePdf)
    (N : ℕ) (x : ℝ → ℝ) (hx : BuyingToBundle.IsAllocationRule μL μH x) :
    (∫ μ : Fin N → ℝ,
        ∑ I : Fin N → Bool,
          (∏ i, if I i then x (μ i) else 1 - x (μ i)) *
            |(∑ i, if I i then μ i else 0) - ∑ i, x (μ i) * μ i|
        ∂(Measure.pi fun _ : Fin N => qual)) ≤
      μH * Real.sqrt N := by sorry

Source

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

View graph