$E[ALG]\ge(1-(1-1/n)^n)\,OPT^*$ for every feasible LP solution

Proved

ComplementFreeCA.XOSRounding.expected_alg_ge_lp_value

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

approximation-algorithmscombinatorial-auctionsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1randomized-roundingxos-valuations

Let $n\ge1$ , let every bidder $i$ have an XOS valuation $v_i$ with admissible clause set $W_i$ and XOS oracle $\mathrm{cl}_i$ , and let $\mathrm{win}$ be a highest-clause assignment rule. Let $x$ be a feasible solution of the LP relaxation with value $\mathrm{OPT}^*(x)=\sum_{i,S}x_{i,S}v_i(S)$ . Run the algorithm of §3.2 on the preallocation drawn by randomized rounding from $x$ , and let $\mathrm{ALG}$ be the welfare of its allocation. Then

\mathbb E[\mathrm{ALG}]\ \ge\ \Big(1-\Big(1-\frac1n\Big)^n\Big)\,\mathrm{OPT}^*(x).

This is the bound the proof of Theorem 3.2 establishes against the fractional value, from which the guarantee against the integral optimum follows.

Formalization Note The statement holds for every feasible $x$ , every choice of maximizing clauses and every tie-breaking in step (iii).

Preamble

import Mathlib
import Definitions.Def_ComplementFreeCA_XOSRounding_Model
import Definitions.Def_ComplementFreeCA_XOSRounding_Rounding
import Definitions.Def_ComplementFreeCA_XOSRounding_Algorithm

Formal statement

namespace ComplementFreeCA.XOSRounding

theorem expected_alg_ge_lp_value {n m : ℕ} (hn : 0 < n)
    (W : Fin n → Finset (Fin m → ℝ)) (v : Fin n → Finset (Fin m) → ℝ)
    (hv : ∀ i, IsXOSWith (v i) (W i))
    (cl : Fin n → Finset (Fin m) → Fin m → ℝ) (hcl : ∀ i, IsXOSOracle (v i) (W i) (cl i))
    (win : (Fin n → Finset (Fin m)) → Fin m → Fin n) (hwin : IsHighestClauseRule cl win)
    (x : Fin n → Finset (Fin m) → ℝ) (hx : IsLPFeasible x) :
    (1 - (1 - 1 / (n : ℝ)) ^ n) * lpValue v x ≤
      roundingExpectation x (algWelfare v win) := by sorry

end ComplementFreeCA.XOSRounding

Source

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

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

E[ALG]≥(1−(1−1/n)n) OPT∗E[ALG]\ge(1-(1-1/n)^n)\,OPT^*E[ALG]≥(1−(1−1/n)n)OPT∗ for every feasible LP solution

$E[ALG]\ge(1-(1-1/n)^n)\,OPT^*$ for every feasible LP solution