buying_to_bundle_bernoulli_product_sum_abs_mean_le

Proved

by ann · Jul 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

bernoulli-productbuying-to-bundleeq-5

Conditional finite-product Bernoulli fluctuation bound for Equation (5) of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers, Appendix C.2 p. 35. For fixed qualities $a_i \in [0,\mu_H]$ and independent inclusion probabilities $p_i \in [0,1]$ , the explicit finite mixture over inclusion patterns satisfies $E_I\,|\sum_i I_i a_i - \sum_i p_i a_i| \le \mu_H\sqrt N$ . The paper proves this by $E_I Y=\sum_i p_i a_i$ , $\operatorname{Var}(Y)=\sum_i p_i(1-p_i)a_i^2\le N\mu_H^2$ , and Cauchy-Schwarz/Jensen.

Preamble

import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Probability.Moments.Variance
import Mathlib.Probability.ProbabilityMassFunction.Constructions
import Mathlib.Probability.ProbabilityMassFunction.Integrals
import Mathlib.Tactic

open MeasureTheory
open scoped BigOperators

Formal statement

theorem buying_to_bundle_bernoulli_product_sum_abs_mean_le
    {N : ℕ} {μH : ℝ} (hμH0 : 0 ≤ μH)
    (p a : Fin N → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1)
    (ha0 : ∀ i, 0 ≤ a i) (haH : ∀ i, a i ≤ μH) :
    (∑ I : Fin N → Bool,
        (∏ i, if I i then p i else 1 - p i) *
          |(∑ i, if I i then a i else 0) - ∑ i, p i * a i|) ≤
      μH * Real.sqrt N := by sorry

Source

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

View graph