Eq. (1): $1-\prod_{i\le k}(1-X_i)\ge(1-(1-1/n)^n)\sum_{i\le k}X_i$

Proved

ComplementFreeCA.XOSRounding.eq1_product_bound

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

inequalitiesp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1probability

Let $1\le k\le n$ and let $X_1,\dots,X_k\in[0,1]$ satisfy $X_1+\dots+X_k\le 1$ . Then

1-\prod_{i=1}^k(1-X_i)\ \ge\ 1-\Big(1-\frac{\sum_{i=1}^kX_i}{k}\Big)^k\ \ge\ \Big(1-\Big(1-\frac1k\Big)^k\Big)\sum_{i=1}^kX_i\ \ge\ \Big(1-\Big(1-\frac1n\Big)^n\Big)\sum_{i=1}^kX_i .

This is the analytic core of Lemma 3.3: the probability that at least one of $k$ independent events with probabilities $X_i$ occurs is at least a $1-(1-1/n)^n\ (\ge 1-1/e)$ fraction of the sum of the probabilities.

Formalization Note The three inequalities of the chain are stated as a conjunction. In the paper the $X_i$ are the probabilities $X_i^j$ that bidder $i$ receives item $j$ in the preallocation, and $\sum_i X^j_i\le1$ comes from the item constraint of the LP.

Preamble

import Mathlib

Formal statement

namespace ComplementFreeCA.XOSRounding

theorem eq1_product_bound (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) (X : Fin k → ℝ)
    (hX0 : ∀ i, 0 ≤ X i) (hX1 : ∀ i, X i ≤ 1) (hsum : ∑ i, X i ≤ 1) :
    1 - (1 - (∑ i, X i) / (k : ℝ)) ^ k ≤ 1 - ∏ i, (1 - X i) ∧
    (1 - (1 - 1 / (k : ℝ)) ^ k) * ∑ i, X i ≤ 1 - (1 - (∑ i, X i) / (k : ℝ)) ^ k ∧
    (1 - (1 - 1 / (n : ℝ)) ^ n) * ∑ i, X i ≤ (1 - (1 - 1 / (k : ℝ)) ^ k) * ∑ i, X i := by sorry

end ComplementFreeCA.XOSRounding

Source

Dobzinski, Nisan, Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Math. Oper. Res. 35(1), 2010, pp. 7-8, §3.2, proof of Lemma 3.3, Eq. (1)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (1): 1−∏i≤k(1−Xi)≥(1−(1−1/n)n)∑i≤kXi1-\prod_{i\le k}(1-X_i)\ge(1-(1-1/n)^n)\sum_{i\le k}X_i1−∏i≤k​(1−Xi​)≥(1−(1−1/n)n)∑i≤k​Xi​

Eq. (1): $1-\prod_{i\le k}(1-X_i)\ge(1-(1-1/n)^n)\sum_{i\le k}X_i$